Skip to content

Conversation

@protz
Copy link
Contributor

@protz protz commented Nov 7, 2025

@ssyram this is a WIP -- I tried to extract more code from the str module

I think in the long run, we will want a mechanism to encode some type equations for when things have the same representation, like you have done on your branch -- this is one case where we have to know that str is a slice of u8, and it looks based on your branch that there are more such cases

@ssyram
Copy link
Contributor

ssyram commented Nov 7, 2025

Ah, yes, there are many such cases, e.g., in tmp-checker branch, I added a function essentially_slice in the MonoState module, which is:

let essentially_slice lid =
  let (|>) x f = f x in
  [
    [ "std"; "path" ], "Path";
    [ "std"; "ffi"; "os_str" ], "OsStr";
  ]
  |> List.mem lid

But I don't think we should handle them by hand by ourselves, ultimately, after the mono migration, we will be able to know their metadata and translate as Eurydice::dst_ref -- this is what is happening now.

The problem now is just that in the generic case like fn by_ref<T>(t: &T) { ... } or so, the type checker cannot recognise these types (e.g., std::path::Path) as DST. But they will not appear in mono mode.

This is how I understand it, but might be wrong, would you have a deeper explanation to your intention if this is not what you mean?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants