#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"6746549772c5cc0ac66c0fce562f297f4d4b80a2/ghc" 67465497/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6746549772c5cc0ac66c0fce562f297f4d4b80a2" Add kind equalities to GHC. This implements the ideas originally put forward in "System FC with Explicit Kind Equality" (ICFP'13). There are several noteworthy changes with this patch: * We now have casts in types. These change the kind of a type. See new constructor `CastTy`. * All types and all constructors can be promoted. This includes GADT constructors. GADT pattern matches take place in type family equations. In Core, types can now be applied to coercions via the `CoercionTy` constructor. * Coercions can now be heterogeneous, relating types of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2` proves both that `t1` and `t2` are the same and also that `k1` and `k2` are the same. * The `Coercion` type has been significantly enhanced. The documentation in `docs/core-spec/core-spec.pdf` reflects the new reality. * The type of `*` is now `*`. No more `BOX`. * Users can write explicit kind variables in their code, anywhere they can write type variables. For backward compatibility, automatic inference of kind-variable binding is still permitted. * The new extension `TypeInType` turns on the new user-facing features. * Type families and synonyms are now promoted to kinds. This causes trouble with parsing `*`, leading to the somewhat awkward new `HsAppsTy` constructor for `HsType`. This is dispatched with in the renamer, where the kind `*` can be told apart from a type-level multiplication operator. Without `-XTypeInType` the old behavior persists. With `-XTypeInType`, you need to import `Data.Kind` to get `*`, also known as `Type`. * The kind-checking algorithms in TcHsType have been significantly rewritten to allow for enhanced kinds. * The new features are still quite experimental and may be in flux. * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203. * TODO: Update user manual. Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142. Updates Haddock submodule. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | ErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11672 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * keywords: TypeInType => TypeInType, ErrorMessages * related: => #11672 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.2 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | ErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11672 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): See also #12373, which looks quite similar to this bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | ErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11672 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: => goldfire Comment: Has there been any motion on this Richard? If not is it safe to say that this won't be fixed for 8.2? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeInType, Resolution: | ErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11672 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See #13530 for a concrete and very simple test case -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 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: Blocked By: | Blocking: Related Tickets: #11672 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeInType, ErrorMessages => TypeInType, TypeErrorMessages -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 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: Blocked By: | Blocking: Related Tickets: #11672 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"8e15e3d370e9c253ae0dbb330e25b72cb00cdb76/ghc" 8e15e3d3/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8e15e3d370e9c253ae0dbb330e25b72cb00cdb76" Improve error messages around kind mismatches. Previously, when canonicalizing (or unifying, in uType) a heterogeneous equality, we emitted a kind equality and used the resulting coercion to cast one side of the heterogeneous equality. While sound, this led to terrible error messages. (See the bugs listed below.) The problem is that using the coercion built from the emitted kind equality is a bit like a wanted rewriting a wanted. The solution is to keep heterogeneous equalities as irreducible. See Note [Equalities with incompatible kinds] in TcCanonical. This commit also removes a highly suspicious switch to FM_SubstOnly when flattening in the kinds of a type variable. I have no idea why this was there, other than as a holdover from pre-TypeInType. I've not left a Note because there is simply no reason I can conceive of that the FM_SubstOnly should be there. One challenge with this patch is that the emitted derived equalities might get emitted several times: when a heterogeneous equality is in an implication and then gets floated out from the implication, the Derived is present both in and out of the implication. This causes a duplicate error message. (Test case: typecheck/should_fail/T7368) Solution: track the provenance of Derived constraints and refuse to float out a constraint that has an insoluble Derived. Lastly, this labels one test (dependent/should_fail/RAE_T32a) as expect_broken, because the problem is really #12919. The different handling of constraints in this patch exposes the error. This fixes bugs #11198, #12373, #13530, and #13610. test cases: typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610} }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11198: TypeInType error message regressions -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: merge 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 goldfire): * testcase: => typecheck/should_fail/{T8262,T8603,tcfail122} * status: new => merge * milestone: 8.4.1 => 8.2.2 Comment: I'm going to label this merge, as it would really be nice to get this into 8.2.2. But I don't really mean it, because it's a sizeable change. Judge for yourself. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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: | -------------------------------------+------------------------------------- Comment (by simonpj):

What test program inspired comment:18?

The one in #13910, with HEAD. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11198#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler