Opened 22 months ago

Last modified 8 days ago

#11198 new bug

TypeInType error message regressions

Reported by: goldfire Owned by:
Priority: high Milestone: 8.2.2
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: typecheck/should_fail/{T8262,T8603,tcfail122}
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 (20)

comment:1 Changed 22 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 21 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 20 months ago by thomie

Component: CompilerCompiler (Type checker)

comment:4 Changed 19 months ago by adamgundry

Keywords: ErrorMessages added

comment:5 Changed 18 months ago by bgamari

Milestone: 8.0.18.0.2

comment:6 Changed 15 months ago by goldfire

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

comment:7 Changed 12 months ago by bgamari

Milestone: 8.0.28.2.1

This won't be happening for 8.0.2.

comment:8 Changed 9 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 9 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 6 months ago by simonpj

See #13530 for a concrete and very simple test case

comment:11 Changed 5 months ago by goldfire

Another case (possibly): #13610.

comment:12 Changed 5 months ago by simonpj

Keywords: TypeErrorMessages added; ErrorMessages removed

comment:13 Changed 5 months ago by bgamari

Milestone: 8.2.18.4.1

comment:14 Changed 2 months ago by Richard Eisenberg <rae@…>

In 8e15e3d3/ghc:

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}

comment:15 Changed 2 months ago by Richard Eisenberg <rae@…>

In 9a54975/ghc:

Test #11672 in typecheck/should_fail/T11672.

I believe this was fixed with the fix for #11198.

comment:16 Changed 2 months ago by goldfire

Milestone: 8.4.18.2.2
Status: newmerge
Test Case: typecheck/should_fail/{T8262,T8603,tcfail122}

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.

comment:17 Changed 3 weeks ago by bgamari

I'll admit I've been very much on the fence about this. We have said that we would aim to tighten up the release schedule and one piece of this is to reduce the quantity of non-regression (relative to the last major release, 8.2.1 in this case) bugfixes merged. As alluded to in comment:16, the patch in question is rather large and, while there is nothing particularly challenging about merging it, I do worry that we will lose some amount of moral authority to deny merging other non-critical bugfixes.

On the other hand, the patch does significantly improve the clarity of kind errors which I think users will appreciate. I'm going to continue to reflect on this but at the moment I'm leaning towards merging.

comment:18 Changed 8 days ago by simonpj

Owner: goldfire deleted
Status: mergenew

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?

comment:19 Changed 8 days ago by goldfire

What test program inspired comment:18? I don't agree with some of your conclusions and want to examine this myself. In particular, both problems (the already-unified kappa and the F Int example) would seem to be solved as long as we flatten kinds sufficiently. I have reworked some of the code around this in Phab:D3848 (my big flattener patch), which is currently (with much progress made today) undergoing revisions as suggested last week. This new version explicitly flattens kinds before emitting the derived, and so I wonder if your test program behaves differently on my end.

comment:20 Changed 8 days ago by simonpj

What test program inspired comment:18?

The one in #13910, with HEAD.

I wonder if your test program behaves differently on my end

Might well. The ALAS part was that we were not "seeing" earlier unifications that affected kinds. Nothing to do with type functions.

Hmm. Maybe you are right that that would be enough. To replay my reasoning, if we had

[W] (alpha :: F beta) ~ (gamma :: *)

Then if we flatten the kinds we'd get

[W] F beta ~ fuv
Inert irred   (alpha :: fuv) ~ (gamma :: *)

Now if we end up reducing that F beta we'll unify the fuv and hence (I hope) kick out the inert irred.

Even if we had

[G] a ~ *    -- skolems
[W] (alpha :: a) ~ (Int :: *)

then we'll rewrite that (alpha :: a) to (alpha :: *) when we flatten the kind (I hope), and all will be well.

So yes, provided we flatten the kinds before parking the equality as an Irred, I think it'll be fine. Sing ho for the Big Flattener Patch.

Last edited 8 days ago by simonpj (previous) (diff)
Note: See TracTickets for help on using tickets.