[GHC] #13083: Constraint solving failure with Coercible + type family + newtype

[GHC]

#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