Tighten up the treatment of loose types in the solver
Note [Use loose types in inert set] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly solvable from the other. So, we do lookup in the inert set using loose types, which omits the kind-check. We must be careful when using the result of a lookup because it may not match the requested info exactly!
There are several problems.
We aren't always careful. For example,
lookupInertDict, both of which use this "loose" lookup. Yet the result of
lookupInInertsjust uses the result, without any special handling to take the fact that the types might not match exactly.
The Note doesn't actually make sense. The only difference between
Eq (a |> c1)and
Eq (a |> c2)is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type
Eq (a |> c1)where GHC is expecting
Eq (a |> c2)(assuming
c2have the same type), all will be well.
What I think the Note is trying to say will never happen. That is, the actual implementation of the inert-set lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing
Eq (a :: k1)with
Eq (a :: k2). But that's impossible, even with casts: all type families and classes have closed kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have well-typed
T blah1 (... :: kind1)and
T blah2 (... :: kind2), then either
blah2must differ. We use this logic elsewhere -- in particular, in the pure unifier.
Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
We should update the Note with my argument above.
No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in
I'm pretty confident about this all, but I'd like a double-check before I commit a fix.