`tcMatchTy` is terribly broken
Suppose (T :: forall k. k -> Type)
and we are matching
tcMatchTy (T k (a::k)) (T j (b::j))
Then we'll match k :-> j
, as expected. But then in TcUnify.unify_tys
we invoke
unify_tys env (a::k) (b::j) (Refl k)
Despite Note [Kind coercions in Unify]
it's not clear to
me why we need that Refl coercion.
But, assuming we need it, very very bad things now happen.
In uUnrefined
we end up adding the binding a :-> (b |> Refl k)
.
Alas! Alack! k
is one of the template variables, which we are
substituting away, so it's terrible if k
appears in the
range of the substitution -- it belongs only in the range.
A one-line (actually one-character) fix is this:
- = do { unify_ty env x y (mkNomReflCo $ typeKind x)
+ = do { unify_ty env x y (mkNomReflCo $ typeKind y)
But I am hard-pressed to explain exactly why this is the correct fix.
@rae, help?
This actually bit me when working on mkCastTy
in #17323.