#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