[GHC] #11198: TypeInType error message regressions

[GHC]

#11198: TypeInType error message regressions
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  7.11
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 `TypeInType` causes error messages around certain kind errors to degrade.

 Here is the case:

 {{{
 [W] (alpha :: k) ~ (Int :: *)
 }}}

 where `alpha` is a unification variable, `k` is a skolem, and there is no
 witness that `k ~ *`. The solver will simplify to

 {{{
 [W] kco :: k ~ *
 [W] (alpha :: k) ~ (Int |> sym kco)
 }}}

 and then the latter, now homogeneous equality is solved by unification

 {{{
 alpha := Int |> sym kco
 }}}

 This is all sound. But when reporting a kind error around `k` not
 equalling `*`, GHC likes to report the type error that the kind error came
 from. But, after zonking, the type error looks like `Int ~ Int`, when we
 drop coercions (as we tend to do in error messages).

 That's unfortunate. It affects test cases
   * T9196
   * T8262
   * T8603
   * tcfail122

 Simon has proposed a rule that should avoid this: never, ever use a wanted
 as a kind cast. That might work, but an attempt at implementing caused a
 loop when kind families were involved. I will keep pushing on this.

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