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

8 files changed, 56 insertions, 3 deletions

diff --git a/testsuite/tests/gadt/gadtSyntaxFail003.stderr b/testsuite/tests/gadt/gadtSyntaxFail003.stderr
index bb2b6a2fff..a66d135c3a 100644
--- a/testsuite/tests/gadt/gadtSyntaxFail003.stderr
+++ b/testsuite/tests/gadt/gadtSyntaxFail003.stderr
@@ -1,7 +1,7 @@
 
 gadtSyntaxFail003.hs:7:5: error:
     • Data constructor ‘C1’ has existential type variables, a context, or a specialised result type
-        C1 :: forall b a c. a -> Int -> c -> Foo b a
+        C1 :: forall a c b. a -> Int -> c -> Foo b a
         (Use ExistentialQuantification or GADTs to allow this)
     • In the definition of data constructor ‘C1’
       In the data type declaration for ‘Foo’
diff --git a/testsuite/tests/ghci/scripts/T11721.script b/testsuite/tests/ghci/scripts/T11721.script
new file mode 100644
index 0000000000..11fa313e3c
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T11721.script
@@ -0,0 +1,7 @@
+:set -XGADTs -XPolyKinds -XTypeApplications
+:set -fprint-explicit-foralls
+import Data.Proxy
+data X a where { MkX :: b -> Proxy a -> X a }
+:type +v MkX
+:type +v MkX @Int
+:type +v MkX @Int @Maybe
diff --git a/testsuite/tests/ghci/scripts/T11721.stdout b/testsuite/tests/ghci/scripts/T11721.stdout
new file mode 100644
index 0000000000..145a5894dc
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T11721.stdout
@@ -0,0 +1,3 @@
+MkX :: forall {k} b (a :: k). b -> Proxy a -> X a
+MkX @Int :: forall {k} (a :: k). Int -> Proxy a -> X a
+MkX @Int @Maybe :: Int -> Proxy Maybe -> X Maybe
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index 6d1d0f1172..4eed55b812 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -239,6 +239,7 @@ test('T12007', normal, ghci_script, ['T12007.script'])
 test('T11975', normal, ghci_script, ['T11975.script'])
 test('T10963', normal, ghci_script, ['T10963.script'])
 test('T11547', normal, ghci_script, ['T11547.script'])
+test('T11721', normal, ghci_script, ['T11721.script'])
 test('T12520', normal, ghci_script, ['T12520.script'])
 test('T12091', [extra_run_opts('-fobject-code')], ghci_script,
      ['T12091.script'])
diff --git a/testsuite/tests/patsyn/should_fail/T11010.stderr b/testsuite/tests/patsyn/should_fail/T11010.stderr
index b09140c0a5..6e3aae58f5 100644
--- a/testsuite/tests/patsyn/should_fail/T11010.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11010.stderr
@@ -3,7 +3,7 @@ T11010.hs:9:36: error:
     • Couldn't match type ‘a1’ with ‘Int’
       ‘a1’ is a rigid type variable bound by
         a pattern with constructor:
-          Fun :: forall b a. String -> (a -> b) -> Expr a -> Expr b,
+          Fun :: forall a b. String -> (a -> b) -> Expr a -> Expr b,
         in a pattern synonym declaration
         at T11010.hs:9:26-36
       Expected type: a -> b
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 0794442edc..3e14ab4594 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -6,7 +6,7 @@ T8566.hs:32:9: error:
         bound by the instance declaration at T8566.hs:30:10-67
       or from: 'AA t (a : as) ~ 'AA t1 as1
         bound by a pattern with constructor:
-                   A :: forall (r :: [*]) v (t :: v) (as :: [U *]). I ('AA t as) r,
+                   A :: forall v (t :: v) (as :: [U *]) (r :: [*]). I ('AA t as) r,
                  in an equation for ‘c’
         at T8566.hs:32:5
       The type variable ‘fs0’ is ambiguous
diff --git a/testsuite/tests/typecheck/should_compile/T13848.hs b/testsuite/tests/typecheck/should_compile/T13848.hs
new file mode 100644
index 0000000000..36c45b49fc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13848.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module T13848 where
+
+data N = Z | S N
+
+data Vec1 (n :: N) a where
+  VNil1  :: forall a. Vec1 Z a
+  VCons1 :: forall n a. a -> Vec1 n a -> Vec1 (S n) a
+
+data Vec2 (n :: N) a where
+  VNil2  :: Vec2 Z a
+  VCons2 :: a -> Vec2 n a -> Vec2 (S n) a
+
+data Vec3 (n :: N) a
+  = (n ~ Z) => VNil3
+  | forall (n' :: N). (n ~ S n') => VCons3 a (Vec3 n' a)
+
+vcons1 :: Vec1 (S Z) Int
+vcons1 = VCons1 @Z @Int 1 (VNil1 @Int)
+
+vcons2 :: Vec2 (S Z) Int
+vcons2 = VCons2 @Int @Z 1 (VNil2 @Int)
+
+vcons3 :: Vec3 (S Z) Int
+vcons3 = VCons3 @(S Z) @Int @Z 1 (VNil3 @Z @Int)
+
+newtype Result1 a s = Ok1 s
+
+newtype Result2 a s where
+  Ok2 :: s -> Result2 a s
+
+result1 :: Result1 Int Char
+result1 = Ok1 @Int @Char 'a'
+
+result2 :: Result2 Int Char
+result2 = Ok2 @Char @Int 'a'
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a1062a229e..6f855df8bb 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -565,6 +565,7 @@ test('T13680', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])
 test('T13822', normal, compile, [''])
+test('T13848', normal, compile, [''])
 test('T13871', normal, compile, [''])
 test('T13879', normal, compile, [''])
 test('T13881', normal, compile, [''])