#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