Opened 18 months ago

Last modified 9 days ago

#11721 patch bug

GADT-syntax data constructors don't work well with TypeApplications

Reported by: goldfire Owned by: RyanGlScott
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.1
Keywords: TypeApplications Cc: RyanGlScott, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #13848, #12025 Differential Rev(s): Phab:D3687
Wiki Page:

Description

Consider

data X a where
  MkX :: b -> Proxy a -> X a

According to the rules around specified vs. generalized variables around TypeApplications, the type of MkX should be

MkX :: forall {k} (b :: *) (a :: k). b -> Proxy a -> X a

A few things to note:

  • The k isn't available for TypeApplications (that's why it's in braces), because it is not user-written.
  • The b is quantified before the a, because b comes before a in the user-written type signature for MkX.

Both of these bullets are currently violated. GHCi reports MkX's type as

MkX :: forall k (a :: k) b. b -> Proxy a -> X a

It turns out that this is a hard to fix. The problem is that GHC expects data constructors to have their universal variables followed by their existential variables, always. And yet that's violated in the desired type for MkX. Furthermore, given the way that GHC deals with GADT return types ("rejigging", in technical parlance), it's inconvenient to get the specified/generalized distinction correct.

Given time constraints, I'm afraid fixing this all won't make it for 8.0.

Happily, there is are easy-to-articulate rules governing GHC's current (wrong) behavior. In a GADT-syntax data constructor:

  • All kind and type variables are considered specified and available for visible type application.
  • Universal variables always come first, in precisely the order they appear in the tycon. Note that universals that are constrained by a GADT return type are missing from the datacon.
  • Existential variables come next. Their order is determined by a user-written forall; or, if there is none, by taking the left-to-right order in the datacon's type and doing a stable topological sort. (This stable topological sort step is the same as for other user-written type signatures.)

Despite the existence of these rules, it would still be better not to have special rules for GADT-syntax data constructors. This ticket is intended to capture that eventual goal.

Change History (11)

comment:1 Changed 18 months ago by simonpj

Could we avoid having the special rules by embodying the type the user wrote in the wrapper for MkX?

comment:2 Changed 18 months ago by goldfire

Yes, we could. Then the wrapper implementation would just match up the tyvars. I don't think it would be that hard. But I've grown increasingly worried about my ability to graduate before my new job starts, and I've just had to draw the line somewhere. I am currently validating my last round of patches and hope very much to focus primarily on my dissertation immediately thereafter.

comment:3 Changed 18 months ago by simonpj

That's fine. I just wanted to lay out a design alternative.

comment:4 Changed 18 months ago by Richard Eisenberg <eir@…>

In 35e93797/ghc:

Track specified/invisible more carefully.

In particular, this allows correct tracking of specified/invisible
for variables in Haskell98 data constructors and in pattern synonyms.
GADT-syntax constructors are harder, and are left until #11721.

This was all inspired by Simon's comments to my fix for #11512,
which this subsumes.

Test case: ghci/scripts/TypeAppData

[skip ci]  (The test case fails because of an unrelated problem
fixed in the next commit.)

comment:5 Changed 6 months ago by bgamari

Milestone: 8.2.18.4.1

Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4

comment:6 Changed 3 months ago by RyanGlScott

Cc: RyanGlScott added

comment:7 Changed 3 months ago by RyanGlScott

Owner: changed from goldfire to RyanGlScott

I'm working on this at the moment. A very rough attempt at this is located at Phab:D3687, but it's nowhere near ready to be merged (the changes I've introduced bring out many inscrutable Core Lint errors, which I'll need to puzzle over).

comment:8 Changed 3 months ago by simonpj

See discussion in #13848 (only closed because duplicate)

comment:9 Changed 2 weeks ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 2 weeks ago by Iceland_jack

comment:11 Changed 9 days ago by RyanGlScott

Differential Rev(s): Phab:D3687
Status: newpatch

Phab:D3687 is now ready for review.

Note: See TracTickets for help on using tickets.