Track the order of user-written tyvars in DataCon
authorRyan Scott <ryan.gl.scott@gmail.com>
Tue, 3 Oct 2017 18:58:27 +0000 (14:58 -0400)
committerBen Gamari <ben@smart-cactus.org>
Tue, 3 Oct 2017 20:25:15 +0000 (16:25 -0400)
commitef26182e2014b0a2a029ae466a4b121bf235e4e4
tree8896c54392be17515b457770a43667264cab93fe
parent8d647450655713e035091349d5163a1a28be18f4
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
23 files changed:
compiler/backpack/RnModIface.hs
compiler/basicTypes/DataCon.hs
compiler/basicTypes/DataCon.hs-boot
compiler/basicTypes/MkId.hs
compiler/iface/BuildTyCl.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/iface/MkIface.hs
compiler/iface/TcIface.hs
compiler/prelude/TysWiredIn.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/types/TyCoRep.hs
compiler/vectorise/Vectorise/Generic/PData.hs
compiler/vectorise/Vectorise/Type/TyConDecl.hs
docs/users_guide/8.4.1-notes.rst
testsuite/tests/gadt/gadtSyntaxFail003.stderr
testsuite/tests/ghci/scripts/T11721.script [new file with mode: 0644]
testsuite/tests/ghci/scripts/T11721.stdout [new file with mode: 0644]
testsuite/tests/ghci/scripts/all.T
testsuite/tests/patsyn/should_fail/T11010.stderr
testsuite/tests/polykinds/T8566.stderr
testsuite/tests/typecheck/should_compile/T13848.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T