Opened 20 months ago

Closed 7 weeks ago

Last modified 6 weeks ago

#11721 closed bug (fixed)

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: ghci/scripts/T11721, th/T11721_TH, typecheck/should_compile/T13848
Blocked By: Blocking:
Related Tickets: #13848, #12025 Differential Rev(s): Phab:D3687, Phab:D4070
Wiki Page:

Description (last modified by bgamari)

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 (16)

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

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

comment:4 Changed 20 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 8 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 5 months ago by RyanGlScott

Cc: RyanGlScott added

comment:7 Changed 5 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 5 months ago by simonpj

See discussion in #13848 (only closed because duplicate)

comment:9 Changed 2 months ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 2 months ago by Iceland_jack

comment:11 Changed 2 months ago by RyanGlScott

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

Phab:D3687 is now ready for review.

comment:12 Changed 7 weeks ago by Ben Gamari <ben@…>

In ef26182/ghc:

Track the order of user-written tyvars in DataCon

After typechecking a data constructor's type signature, its type
variables are partitioned into two distinct groups: the universally
quantified type variables and the existentially quantified type
variables. Then, when prompted for the type of the data constructor,
GHC gives this:

```lang=haskell
MkT :: forall <univs> <exis>. (...)
```

For H98-style datatypes, this is a fine thing to do. But for GADTs,
this can sometimes produce undesired results with respect to
`TypeApplications`. For instance, consider this datatype:

```lang=haskell
data T a where
  MkT :: forall b a. b -> T a
```

Here, the user clearly intended to have `b` be available for visible
type application before `a`. That is, the user would expect
`MkT @Int @Char` to be of type `Int -> T Char`, //not//
`Char -> T Int`. But alas, up until now that was not how GHC
operated—regardless of the order in which the user actually wrote
the tyvars, GHC would give `MkT` the type:

```lang=haskell
MkT :: forall a b. b -> T a
```

Since `a` is universal and `b` is existential. This makes predicting
what order to use for `TypeApplications` quite annoying, as
demonstrated in #11721 and #13848.

This patch cures the problem by tracking more carefully the order in
which a user writes type variables in data constructor type
signatures, either explicitly (with a `forall`) or implicitly
(without a `forall`, in which case the order is inferred). This is
accomplished by adding a new field `dcUserTyVars` to `DataCon`, which
is a subset of `dcUnivTyVars` and `dcExTyVars` that is permuted to
the order in which the user wrote them. For more details, refer to
`Note [DataCon user type variables]` in `DataCon.hs`.

An interesting consequence of this design is that more data
constructors require wrappers. This is because the workers always
expect the first arguments to be the universal tyvars followed by the
existential tyvars, so when the user writes the tyvars in a different
order, a wrapper type is needed to swizzle the tyvars around to match
the order that the worker expects. For more details, refer to
`Note [Data con wrappers and GADT syntax]` in `MkId.hs`.

Test Plan: ./validate

Reviewers: austin, goldfire, bgamari, simonpj

Reviewed By: goldfire, simonpj

Subscribers: ezyang, goldfire, rwbarton, thomie

GHC Trac Issues: #11721, #13848

Differential Revision: https://phabricator.haskell.org/D3687

comment:13 Changed 7 weeks ago by bgamari

Description: modified (diff)
Resolution: fixed
Status: patchclosed

comment:14 Changed 7 weeks ago by RyanGlScott

Differential Rev(s): Phab:D3687Phab:D3687, Phab:D4070

Phab:D4070 updates Template Haskell accordingly.

comment:15 Changed 6 weeks ago by Ryan Scott <ryan.gl.scott@…>

In 341d3a78/ghc:

Incorporate changes from #11721 into Template Haskell

Summary:
#11721 changed the order of type variables in GADT
constructor type signatures, but these changes weren't reflected in
Template Haskell reification of GADTs. Let's do that.

Along the way, I:

* noticed that the `T13885` test was claiming to test TH reification
  of GADTs, but the reified data type wasn't actually a GADT! Since
  this patch touches that part of the codebase, I decided to fix
  this.
* incorporated some feedback from @simonpj in
  https://phabricator.haskell.org/D3687#113566. (These changes alone
  don't account for any different in behavior.)

Test Plan: make test TEST=T11721_TH

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: goldfire, bgamari, simonpj

Subscribers: rwbarton, thomie, simonpj

GHC Trac Issues: #11721

Differential Revision: https://phabricator.haskell.org/D4070

comment:16 Changed 6 weeks ago by RyanGlScott

Test Case: ghci/scripts/T11721, th/T11721_TH, typecheck/should_compile/T13848
Note: See TracTickets for help on using tickets.