Niko Matsakis

Probably we want some kind of "well-formed decls" check analogous to [well-formed-mir](https://github.com/nikomatsakis/a-mir-formality/blob/main/src/mir/well-formed-mir.rkt)? It could also check that e.g. all `TraitId` are defined somewhere (which current results in assertion failures).

In other words, I would just define these rules using redex type judgments, not try to make logical predicates.

Started on this in the user-ty branch. I'm currently just adding a `(user-ty ...)` function that converts types "in place", might be nicer eventually to move into the grammar.

Now that #56 added user-ty, I think the next step would be to modify the decl layer and the `WhereClause` to actually just use `UserTy` instead of `Ty`, and then...

My proposed grammar would be that `AdtDecl` remains unchanged, but we have ```diff - (CrateItemDecl ::= FeatureDecl AdtDecl TraitDecl TraitImplDecl ConstDecl FnDecl) + (CrateItemDecl ::= FeatureDecl StructDecl EnumDecl UnionDecl TraitDecl...

We probably want to add a `(not-provable Goal)` goal into the solver so that we can express this -- but I wouldn't want that exposed as a where-clause.

hmm, I am getting a messed up `make serve` locally....  ...could be user error :)

Thanks

Heh, yes! I'm not sure if that example is even valid, actually, I have to double check.

Interesting. This does seem like a case where SSA-style rewriting would help; I wonder if there is another solution. The constraints that arise are roughly like this: ``` 'b1: 'list...