The pure unifier (in types/Unify.hs) is used to match up instances with actual types. Since GHC 8, it matches up the kinds with the types in a separate pass. But this is often wasteful, and sometimes downright wrong.

It's wasteful because most invocations of the unifier on a list of types pass in well-kinded arguments to some type constructor. Because the kinds of type constructors are closed, if we process the list left-to-right, we will always unify the kinds of later arguments before we get to them. So we shouldn't take another pass on the kinds.

It's wrong because it's conceivable for the kind to include a type family application, and using a type family application as a template in the pure unifier is very silly, indeed.

I cam across this while trying to translate Idris's algebraic effects library to Haskell. My reduced test case is attached.

Patch on the way.