Simon Peyton Jones authored Jul 03, 2019 and Marge Bot committed Jul 04, 2019

In the eager unifier, when unifying (tv1 ~ tv2),
when we decide to swap them over, to unify (tv2 ~ tv1),
I'd forgotten to ensure that tv1's kind was fully zonked,
which is an invariant of uUnfilledTyVar2.

That could lead us to build an infinite kind, or (in the
case of #16902) update the same unification variable twice.

Yikes.

Now we get an error message rather than non-termination,
which is much better.  The error message is not great,
but it's a very strange program, and I can't see an easy way
to improve it, so for now I'm just committing this fix.

Here's the decl
 data F (a :: k) :: (a ~~ k) => Type where
    MkF :: F a

and the rather error message of which I am not proud

  T16902.hs:11:10: error:
    • Expected a type, but found something with kind ‘a1’
    • In the type ‘F a’