a-mir-formality
a-mir-formality copied to clipboard
rust-lang
a model of MIR and the Rust type/trait system
Similar to #100, when we reify a fn-def into a fn-ptr, we need to do a vaguely similar process. One option would be to take a `for (P => F)`...
https://github.com/nikomatsakis/a-mir-formality/pull/97 adds in a fn-def type that unifies early/late bound parameters into a single list. It also includes a better approach to implied bounds. But there's lots of work to...
Type-checking calls: when there is a CALL in the MIR, we need to "unpack" the fn type to get to something callable. e.g. if the type of the thing-to-be-called is...
We need tests that fn-def types are well-formed (and maybe code?). To be well-formed, the where-clauses on the fn must be met. (That said, in the MIR type checker, I...
This code might be unused: https://github.com/nikomatsakis/a-mir-formality/blob/4a47eb8d97a374a953d50a94acab55d4c98ac552/racket-src/logic/test/cosld-solve-ambiguity.rkt#L3 That's what racket-mode is telling me, at least. 😇
If you have a grammar like this... ``` Expr = Expr . `await` | Place Place = Id $*Projections Projections = `.` FieldId ``` ...then `a.await` will be parsed as...
In the hope of progressing https://github.com/rust-lang/rust/issues/20400, I stumbled across https://github.com/rust-lang/rfcs/pull/1672. Given [this comment](https://github.com/rust-lang/rfcs/pull/1672#issuecomment-1748505018), I decided to properly investigate a-mir-formality. As it turns out, the current overlap checks are very generous....
Both use `:` in Rust, but the colon is always parsed as outlives in formality. This was confusing when @jackh726 wrote his projection PR, since it looked like trait goals...
In https://github.com/rust-lang/a-mir-formality/pull/145, @jackh726 added basic WF rules for ADTs: https://github.com/rust-lang/a-mir-formality/blob/c0e069180dc28639fa5b2bf351e72e657bf8a5b4/crates/formality-prove/src/prove/prove_wf.rs#L42-L46 These rules effectively say that `Foo` is WF if `T0..Tn` are WF. That's necessary but not sufficient. They should also...
In particular with https://github.com/rust-lang/trait-system-refactor-initiative/issues/8