[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:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:  fixed             |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  dependent/should_compile/T12442
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D2433
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Richard there are no comments to explain what is going on here.

 The brief comments that are there suggest that it's just an efficiency
 thing: when unifying `t1 :: k1` with `t2 :: k2`, if you happen to know
 that `t1 = t2` (in the `eqType`, defnitional equality sense) then no need
 to match them.  Saves work.

 But there is much more to it than that!   You say, cryptically, that
 "sometimes it is downright wrong".  But you need to say that in the code,
 and support it with a few examples that demonstrate how wrong it is, and
 justify the cases where you use the laxer matching.

 Could you do that?  This is subtle stuff, and I'm anxious about making it
 robust to future modification.

 Also, all the remaining calls to `tcMatchTy` now have to guarantee an
 invariant, that the kinds are `eqType`.  I see nothing at the calls sites
 drawing attention to that claim, and justifying why, at that call site, it
 holds.

 Simon

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