Currently we use the types::Context object to hold type bounds. We provide an accessor to BoundRefs which index these bounds, but which internally hold a value uniquely tied to the Context it came from. We check consistency at runtime: if you try to use a boundref with a context it didn't come from, you'll get a types::InferenceContextMismatch error.
However, in Rust it is possible to do this check at compile time, by abusing invariant lifetimes to local variables to create types with unique lifetimes that cannot be unified.
Basically, instead of users calling
let ctx = Context::new();
...
they would write
let _unused = ();
// SAFETY: we are calling `unsafe fn new` with a unique lifetime, and `Context` has an invariant-lifetime PhantomData preventing this unique lifetime from being unified with any other lifetime
let ctx = unsafe { Context::new(&_unused) }(where ofc we would wrap this up in a macro so the user doesn't need to write the dummy variable or the unsafe marker themselves).
A consequence of this construction is that Context (and anything else containing a Context) will be unable to escape the scope in which it is defined. I think this is fine for this type; the "standard usage" is for users to create a context, build a program, then throw away the context, all within some function.
See https://arhan.sh/blog/the-generativity-pattern-in-rust/ for a long blog post which expands this issue into a self-contained blog post which can be understood without having memorized tons of Rust arcana.
The blog post argues that the "Context cannot escape its scope" limitation is inherent to Rust because otherwise you could create a runtime-sized Vec containing a runtime-determined number of unique types, which (almost by definition) requires dependent types. I'm not totally convinced by this argument. It seems like you should be able to create an arbitrary number of generative types and the compiler shouldn't need to care "how many" of them there are. If they don't unify they can't be used together without giving them all distinct names.
Currently we use the
types::Contextobject to hold type bounds. We provide an accessor toBoundRefs which index these bounds, but which internally hold a value uniquely tied to theContextit came from. We check consistency at runtime: if you try to use a boundref with a context it didn't come from, you'll get atypes::InferenceContextMismatcherror.However, in Rust it is possible to do this check at compile time, by abusing invariant lifetimes to local variables to create types with unique lifetimes that cannot be unified.
Basically, instead of users calling
they would write
(where ofc we would wrap this up in a macro so the user doesn't need to write the dummy variable or the
unsafemarker themselves).A consequence of this construction is that
Context(and anything else containing aContext) will be unable to escape the scope in which it is defined. I think this is fine for this type; the "standard usage" is for users to create a context, build a program, then throw away the context, all within some function.See https://arhan.sh/blog/the-generativity-pattern-in-rust/ for a long blog post which expands this issue into a self-contained blog post which can be understood without having memorized tons of Rust arcana.
The blog post argues that the "
Contextcannot escape its scope" limitation is inherent to Rust because otherwise you could create a runtime-sizedVeccontaining a runtime-determined number of unique types, which (almost by definition) requires dependent types. I'm not totally convinced by this argument. It seems like you should be able to create an arbitrary number of generative types and the compiler shouldn't need to care "how many" of them there are. If they don't unify they can't be used together without giving them all distinct names.