[GHC] #11198: TypeInType error message regressions

[GHC]

#11198: TypeInType error message regressions
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.2
       Component:  Compiler (Type    |              Version:  7.11
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeErrorMessages
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  typecheck/should_fail/{T8262,T8603,tcfail122}
      Blocked By:                    |             Blocking:
 Related Tickets:  #11672            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * owner:  goldfire => (none)
 * status:  merge => new


Comment:

 I now think that the patch in comment:14 is bogus.

 I tripped over this when debugging #13910, following
 the patch in comment:7 of that ticket.  We had
 {{{
 [W] alpha |> co  ~  t
 }}}
 where `co :: <blah> ~ kappa`, `alpha` and `kappa` are unification
 variables, `t :: tk` is a skolem.

 We can't unify `alpha := t |> sym co` because the kinds don't match, so,
 according to `Note [Equalities with incompatible kinds]` (introduced in
 comment:14) we emit a derived equality
 {{{
 [D] kappa ~ tk
 }}}
 and park the original Wanted as an Irred.

 ALAS!  It turns out that `kappa` was ''already'' unified with `tk`, so the
 new Derived is instantly solved, but since no unifications happen we don't
 kick out the Wanted from the inert set, so it (utterly bogusly) stays
 unsolved.

 Possible solution: in the kind check in `canEqTyVar` use `zonk_eq_types`.
 That would make this program work, I think, but a deeper bug is lurking.

 The process described in `Note [Equalities with incompatible kinds]`
 relies on the kind-equality being solved by unification.  But what if we
 have
 {{{
 [W] (alpha :: F Int) ~ (beta :: *)
 }}}
 Now we may indeed be able solve the kind equality `F Int ~ *`, if `F` is a
 type function, with a suitable instance.  But there is no unification
 happening, and we really do need ultimately to unify `alpha` to `beta |>
 co` where `co :: * ~ F Int`.  I conclude that the patch in comment:14 is
 utterly wrong.

 Richard do you agree?

 Given `[W] co :: (alpha :: k1) ~ (ty :: k2)`, kind-heterogeneous, I think
 we probably ''do'' want to generate a wanted kind-equality
 {{{
 [W] co_k :: k1 ~ k2
 }}}
 Then rewrite the original equality to
 {{{
 [W] co' :: (alpha :: k1) ~ (ty :: k2) |> sym co_k
 }}}
 '''But we want to somehow refrain from actually carrying out the
 unificationn unti we have discharged `co_k`.'''  One way to do that might
 be to park it in Irreds and kick it out when unifying `co_k`.  But that
 would fail if we end up iterating the entire implication in which this
 constraint lives.  Maybe we should refrain from unify `alpha := ty` if
 there are any coercion holes in `ty`?

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