Tighten up the treatment of loose types in the solver
GHC.Tc.Solver.Monad
includes
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,
lookupInInerts
trieslookupSolvedDict
and thenlookupInertDict
, both of which use this "loose" lookup. Yet the result oflookupInInerts
just 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)
andEq (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 typeEq (a |> c1)
where GHC is expectingEq (a |> c2)
(assumingc1
andc2
have 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)
withEq (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-typedT blah1 (... :: kind1)
andT blah2 (... :: kind2)
, then eitherkind1
equalskind2
orblah1
andblah2
must differ. We use this logic elsewhere -- in particular, in the pure unifier.
Conclusions:
-
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
lookupFlatCache
).
I'm pretty confident about this all, but I'd like a double-check before I commit a fix.