Provide a better error message for unpromotable data constructor contexts
ClosedPublic

Authored by RyanGlScott on May 24 2018, 5:13 AM.

Details

Summary

Trac #14845 brought to light a corner case where a data
constructor could not be promoted (even with -XTypeInType) due to
an unpromotable constraint in its context. However, the error message
was less than helpful, so this patch adds an additional check to
tcTyVar catch unpromotable data constructors like these before
they're promoted, and to give a sensible error message in such cases.

Test Plan

make test TEST="T13895 T14845"

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
RyanGlScott created this revision.May 24 2018, 5:13 AM
RyanGlScott added inline comments.May 24 2018, 5:20 AM
compiler/typecheck/TcHsType.hs
1385

I'm not sure I did a particularly good job of explaining here why certain constraints are off-limits and why others aren't (I'm not too sure of the reasons myself), so suggestions for better wording are welcome here.

docs/users_guide/glasgow_exts.rst
8580

Similarly, do you think we should bother explaining why certain constraints can be promoted and others can't in the users' guide? Or do you think the phrasing I've chosen here suffices?

Let's sort out whether we allow these term level dictionaries in kinds (I think not) first.

compiler/typecheck/TcHsType.hs
1213

use not . eqPred

1399

I don't think so. I think we allow only ~# and ~R#, the primitive equalities. All others are represented by term-level dictionaries that we have to pattern-match on to extract the equality evidence.

Hence isEqPred

Right, Richard?

RyanGlScott added inline comments.May 25 2018, 7:27 AM
compiler/typecheck/TcHsType.hs
1213

isEqPred (I'm assuming that's what you meant) wouldn't work here, as that tests for the wrong set of classes.

1399

No. I definitely meant (~), (~~), and Coercible, as those are exactly the classes checked for in tcInstBinder.

simonpj added inline comments.May 25 2018, 10:15 AM
compiler/typecheck/TcHsType.hs
1399

Maybe so, but first Richard has to explain the impenetrable comment in tcInstBinder

-- handle boxed equality constraints, because it's so easy

I have literally no idea what is going on here.

At the moment I believe that we should have only ~# and ~R# in kinds. Let's see what Richard has to say

goldfire added inline comments.May 30 2018, 3:27 PM
compiler/typecheck/TcHsType.hs
1399

The equality constraints are easy. (And supporting at least nominal equality is necessary to support promoted GADT constructors.) These are easy because we can create type-level dictionaries, even for the lifted constraints. Is there a particular spot of difficulty?

simonpj added inline comments.May 31 2018, 2:55 AM
compiler/typecheck/TcHsType.hs
1399

Is there a particular spot of difficulty?

Yes! At the type level we don't have facilities for building and taking apart dictionaries. Especially taking apart: no case expressions. Can you give a concrete example?

(I'm guessing that you may say something like: it's possible for newtype dictionaries because they are only casts -- but that is vulnerable to us changing our minds about the implementation strategy for singleton dictionaries.)

Moreover, is any of this necessary at all? GADTs are implemented with primitive, unlifted equality constraints.

Finally, when we promote a GADT data con, I think we promote the wrapper don't we? E.g MkT :: forall a. T a a, not MkT :: forall a b. (a ~# b) => T a b. And we have no facilities at the type level for binding local constraints (case at the term level).

So, because of "finally" maybe we don't need ANY of this stuff. Just promote only GADT data cons, but not data cons with any explicit constraints.

goldfire added inline comments.May 31 2018, 6:53 PM
compiler/typecheck/TcHsType.hs
1399

You're right about promoting wrappers. But it shouldn't matter whether the user writes

data G a where
  MkG :: G Bool

or

data G a = (a ~ Bool) => MkG

We want to promote both. And we need this to be able to do so.

We don't have case at the type level, but we do have type families. Matching on a constructor in a type family works just fine even if the constraint is boxed, as it will unify the types related in the equality constraint.

I agree that we could drop Coercible here, but I think we need the others for consistency with GADT promotion.

simonpj added inline comments.Jun 1 2018, 2:34 AM
compiler/typecheck/TcHsType.hs
1399

You're right about promoting wrappers.

Can you be more specific? That is, we promote MkG :: G Bool not MkG :: (a~Bool) => MkG a? Let's say so in a Note somewhere.

We want to promote both.

Why? Can you given an example of *using* even the GADT form? And rather than having some ad-hoc restrictions on constraints wouldn't it be simpler to say "we don't promote data cons with explicit constraints" period.

Finally, can you give me a concrete example of a program that uses the boxed equality constraints, including how they get unboxed at the type level. I have no idea how this happens.

At the moment all this still feels like an unforced complication -- and one that I still do not understand.

RyanGlScott planned changes to this revision.Jun 2 2018, 10:06 AM

As far as I can tell, the plan of attack here should be:

  1. Remove Coercible as a promotable constraint.
  2. Keep the rest of the patch as-is.
  3. Have someone (Richard?) update the relevant Notes about how this desugars into coercions.

Does that sound right?

As far as I can tell, the plan of attack here should be:

  1. Remove Coercible as a promotable constraint.
  2. Keep the rest of the patch as-is.
  3. Have someone (Richard?) update the relevant Notes about how this desugars into coercions.

    Does that sound right?

That sounds right to me, yes.

RyanGlScott updated this revision to Diff 16651.Jun 2 2018, 6:00 PM
  • Don't special-case Coercible

Alright, this should be good to go now.

RyanGlScott updated this revision to Diff 16675.Jun 3 2018, 7:37 AM
  • Remove unused function

Have someone (Richard?) update the relevant Notes about how this desugars into coercions.

I'm keen on this happening. As you could tell during the call I was super-confused. Especially, the treatment of GADTs at the type level is utterly different to that at the term level. (Which I now understand, although it seems unsettling to me.)

It'd be good to close the loop on this.

Agreed. Should I just land this, then?

The discussion we had on this Phab, and indeed on the FC call, should turn into a Note. Otherwise we'll lose it entirely. It's highly non-obvious how very differently GADTs are handled at the term and type level

...did you read the discussion earlier on this Diff? We had agreed that Richard should do this separately, since I haven't the slightest clue how to write up such a Note. As it stands, this ticket will remain in limbo forever if I'm required to write it.

Fine with me -- but perhaps open a ticket with relevant pointers, and assign it to Richard.

Rebase on top of master

  • Accept new test output

Rebase yet again

bgamari accepted this revision.Jun 17 2018, 11:28 AM

Looks quite reasonable to me.

This revision is now accepted and ready to land.Jun 17 2018, 11:28 AM
This revision was automatically updated to reflect the committed changes.