GitLab

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.