Right now, GHC Core doesn't obey the substitution lemma. Specifically, given `a :: TYPE (TupleRep '[])` in scope, `\ (x :: a). x` is a fine expression. However, if we substitute `[a |-> Int ~# Int]` (which is well-kinded), then that expression will not pass Core Lint. The problem is that we need to keep coercions (always of type `ty1 ~#r ty2` for some types `ty1` and `ty2` and role `r`) separate from expressions. This is sometimes done today by looking at types: things that have a coercion type are generally assumed to be coercions, and things without coercion types are not. The problem is that this notion doesn't obey the substitution lemma. A great example is `mkLocalIdOrCoVar`, which either makes a regular variable (an `Id`) or a `CoVar` depending on the type. Another example is in the definition of `~`, which looks kind of like this: ```hs class (a ~# b) => (a ~ b) instance (a ~# b) => (a ~ b) ``` I say "kind of like" because we cannot have an unlifted superclass. But it's a good model. That class definition would get compiled into this datatype definition: ```hs data D~ :: forall k. k -> k -> Constraint where MkD~ :: forall k (a :: k) (b :: k). { eq_sel :: a ~# b } -> D~ a b ``` Notice that this is a record with a record selector. (This is how all classes are compiled.) But now we have a problem, because `eq_sel` actually has a definition: ```hs eq_sel :: D~ a b -> a ~# b eq_sel (MkD~ co) = co ``` This is a function that returns a coercion. But that's not possible in the theory: there is simply no evaluation allowed in coercions. Why do we have this at all? Because when the solver has a Given equality, it needs to get its evidence from somewhere. Specifically, if the solver has `g1 :: a ~ b` as a Given, it will look at `~`'s superclass and extract a Given `a ~# b`. That Given is given a name, say `co1`, and it needs a definition. This will be `co1 = eq_sel g1`. This binding is tracked in the `Bag EvBind` carried around in the solver. In the desugarer, it becomes `let co1 = eq_sel g1`. Well -- almost. Because `co1`'s type is unlifted, we hit the let/app invariant and use a `case` binding. This is good, because it means the `eq_sel g1` will be sure to be evaluated. All will be OK. Except in #17267, all is *not* OK: the binding for the coercion ends up in a recursive group, and then it's let-bound, unevaluated, and an agent of chaos. The fix for #17267 is about fixing the constraint solver not to do that, but it's frightening how far GHC got with a recursive binding for a coercion. The bottom line here is that we must be better in keeping coercions and expressions separate. Specifically: * `lintCoreExpr` aborts on `Type`. This is because all types should be arguments to functions; they are handled by `lintCoreArgs`. The same should be true for coercions. * `CoVar`s should be born separately from `Id`s. That is, remove `mkLocalIdOrCoVar`. * Invent a new form of `EvTerm` that binds a coercion. This will *not* be a `let`-binding. * The desugarer must do SCC analysis to figure out how to desugar the evidence bindings. Currently, this analysis is done after desugaring. But now that we need to desugar equality bindings differently than other ones, it's better to do the SCC analysis first. * The desugarer should produce `FloatBind`s, not `CoreBind`s as it does today. (`FloatBind` allows for `case` bindings.) * Knock-on effect: `DataCon` will have to be more scrupulous about keeping GADT equalities (which are unlifted) apart from other constraints. This means some work in `dataConTheta` and `dataConSig` (the latter should just be removed, as it's essentially never used). None of this is required, and I don't think we have a bug beyond #17267. But it's really a gaping hole in our type system, and it's a matter of good hygiene to sort it out.