You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Right now, when a function or impl is supposed to get "implied bounds" from a type Foo, we add (well-formed (type Foo)) to the environment. In the "expanded implied bounds" proposal this made sense, but it doesn't work well for modeling the more limited version of implied bounds that rust uses. For example, this function is not well-formed in rustc today:
Compiling it gives an error because T: Ord is required (playground).
But in a-mir-formality, we would have trouble producing this error: we would try to prove (well-formed (type (user-ty (WantsOrd T)))) but that is also in the environment, so it would be true.
To solve this, I think we should add a new predicate, (in-scope (ParameterKind Parameter)). This would be added to the environment for a function and it would also have to be proven when invoking a function (these are basically implied where-clauses, though we have no where-clause syntax for it). We would have a built-in rule that says:
and we would create the invariants based on in-scope (so, with expanded implied bounds, we would say that, for all T, (in-scope (type (user-ty (WantsOrd T)))) => (is-implemented (Ord T)), for example).
The text was updated successfully, but these errors were encountered:
Right now, when a function or impl is supposed to get "implied bounds" from a type
Foo
, we add(well-formed (type Foo))
to the environment. In the "expanded implied bounds" proposal this made sense, but it doesn't work well for modeling the more limited version of implied bounds that rust uses. For example, this function is not well-formed in rustc today:Compiling it gives an error because
T: Ord
is required (playground).But in a-mir-formality, we would have trouble producing this error: we would try to prove
(well-formed (type (user-ty (WantsOrd T))))
but that is also in the environment, so it would be true.To solve this, I think we should add a new predicate,
(in-scope (ParameterKind Parameter))
. This would be added to the environment for a function and it would also have to be proven when invoking a function (these are basically implied where-clauses, though we have no where-clause syntax for it). We would have a built-in rule that says:and we would create the invariants based on
in-scope
(so, with expanded implied bounds, we would say that, for allT
,(in-scope (type (user-ty (WantsOrd T))))
=>(is-implemented (Ord T))
, for example).The text was updated successfully, but these errors were encountered: