
#13083: Constraint solving failure with Coercible + type family + newtype -------------------------------------+------------------------------------- Reporter: conal | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Coercible Operating System: MacOS X | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => goldfire Comment: Richard, `TcCanonical.zonk_eq_types` is completely broken. I don't quite know why it's there but it's utterly wrong. Consider the call `zonkEqTypes (T Par1) (S (Par1 b))`. Even though the head type constructors are utterly different you still use `tcRepSplitAppTy_maybe` to make recursive calls to {{{ go T S and go Par1 (Par1 b) }}} Notice these two arguments have different kinds. Incidentally it seems terribly inefficient to break into binary applications when both types are manifestly `TyConApp`s. Now the `tc1 == tc2` case of `go` kicks in, and we call `tycon`. Alas this calls `zipWithM` which simply discards the `b` argument to `Par1`. Eek. This mis-match kind stuff could occur, I guess, if you had {{{ go (T k1 t1) (T k2 t2) }}} where `T` is polykinded and `k1` differs from `k2`. So fixing the efficiency bug would not be enough to fix the mis-matched kind bug. I have a fix validating Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13083#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler