[GHC] #12442: Pure unifier usually doesn't need to unify kinds

[GHC]

#12442: Pure unifier usually doesn't need to unify kinds
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12442>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler