Opened 20 months ago

Last modified 3 months ago

#11198 new bug

TypeInType error message regressions

Reported by: goldfire Owned by: goldfire
Priority: high Milestone: 8.4.1
Component: Compiler (Type checker) Version: 7.11
Keywords: TypeInType, TypeErrorMessages Cc:
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:

Description

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.

Change History (13)

comment:1 Changed 20 months ago by Richard Eisenberg <eir@…>

In 67465497/ghc:

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.

comment:2 Changed 19 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 18 months ago by thomie

Component: CompilerCompiler (Type checker)

comment:4 Changed 17 months ago by adamgundry

Keywords: ErrorMessages added

comment:5 Changed 16 months ago by bgamari

Milestone: 8.0.18.0.2

comment:6 Changed 13 months ago by goldfire

See also #12373, which looks quite similar to this bug.

comment:7 Changed 10 months ago by bgamari

Milestone: 8.0.28.2.1

This won't be happening for 8.0.2.

comment:8 Changed 7 months ago by bgamari

Owner: set to goldfire

Has there been any motion on this Richard? If not is it safe to say that this won't be fixed for 8.2?

comment:9 Changed 7 months ago by goldfire

No motion on this, I'm afraid. I'd love to get to this by 8.2, believe me. Can't swear to it, as I'm prioritizing the levity polymorphism stuff. I've left my work here. There's a chance that rebasing that patch might just work, given the changes to the solver in the meantime. (I gave up because of a solver loop, and my memory just barely tells me that I thought at the time that the loop wasn't my fault.) I'll at least check this possibility soon.

comment:10 Changed 4 months ago by simonpj

See #13530 for a concrete and very simple test case

comment:11 Changed 3 months ago by goldfire

Another case (possibly): #13610.

comment:12 Changed 3 months ago by simonpj

Keywords: TypeErrorMessages added; ErrorMessages removed

comment:13 Changed 3 months ago by bgamari

Milestone: 8.2.18.4.1
Note: See TracTickets for help on using tickets.