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, 493 insertions, 203 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index 1691706ad0..296b4e2f3c 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -523,7 +523,8 @@ rnIfaceConDecls IfAbstractTyCon = pure IfAbstractTyCon
 rnIfaceConDecl :: Rename IfaceConDecl
 rnIfaceConDecl d = do
     con_name <- rnIfaceGlobal (ifConName d)
-    con_ex_tvs <- mapM rnIfaceForAllBndr (ifConExTvs d)
+    con_ex_tvs <- mapM rnIfaceTvBndr (ifConExTvs d)
+    con_user_tvbs <- mapM rnIfaceForAllBndr (ifConUserTvBinders d)
     let rnIfConEqSpec (n,t) = (,) n <$> rnIfaceType t
     con_eq_spec <- mapM rnIfConEqSpec (ifConEqSpec d)
     con_ctxt <- mapM rnIfaceType (ifConCtxt d)
@@ -534,6 +535,7 @@ rnIfaceConDecl d = do
     con_stricts <- mapM rnIfaceBang (ifConStricts d)
     return d { ifConName = con_name
              , ifConExTvs = con_ex_tvs
+             , ifConUserTvBinders = con_user_tvbs
              , ifConEqSpec = con_eq_spec
              , ifConCtxt = con_ctxt
              , ifConArgTys = con_arg_tys
diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index 9b8c527b97..82298f7bfc 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -31,9 +31,8 @@ module DataCon (
         dataConName, dataConIdentity, dataConTag, dataConTagZ,
         dataConTyCon, dataConOrigTyCon,
         dataConUserType,
-        dataConUnivTyVars, dataConUnivTyVarBinders,
-        dataConExTyVars, dataConExTyVarBinders,
-        dataConAllTyVars,
+        dataConUnivTyVars, dataConExTyVars, dataConUnivAndExTyVars,
+        dataConUserTyVars, dataConUserTyVarBinders,
         dataConEqSpec, dataConTheta,
         dataConStupidTheta,
         dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
@@ -52,6 +51,7 @@ module DataCon (
         isNullarySrcDataCon, isNullaryRepDataCon, isTupleDataCon, isUnboxedTupleCon,
         isUnboxedSumCon,
         isVanillaDataCon, classDataCon, dataConCannotMatch,
+        dataConUserTyVarsArePermuted,
         isBanged, isMarkedStrict, eqHsBang, isSrcStrict, isSrcUnpacked,
         specialPromotedDc, isLegacyPromotableDataCon, isLegacyPromotableTyCon,
 
@@ -88,6 +88,7 @@ import qualified Data.Data as Data
 import Data.Char
 import Data.Word
 import Data.List( mapAccumL, find )
+import qualified Data.Set as Set
 
 {-
 Data constructor representation
@@ -278,7 +279,7 @@ data DataCon
         --
         --      *** As declared by the user
         --  data T a where
-        --    MkT :: forall x y. (x~y,Ord x) => x -> y -> T (x,y)
+        --    MkT :: forall y x. (x~y,Ord x) => x -> y -> T (x,y)
 
         --      *** As represented internally
         --  data T a where
@@ -287,17 +288,26 @@ data DataCon
         -- The next six fields express the type of the constructor, in pieces
         -- e.g.
         --
-        --      dcUnivTyVars  = [a]
-        --      dcExTyVars    = [x,y]
-        --      dcEqSpec      = [a~(x,y)]
-        --      dcOtherTheta  = [x~y, Ord x]
-        --      dcOrigArgTys  = [x,y]
-        --      dcRepTyCon       = T
+        --      dcUnivTyVars       = [a]
+        --      dcExTyVars         = [x,y]
+        --      dcUserTyVarBinders = [y,x]
+        --      dcEqSpec           = [a~(x,y)]
+        --      dcOtherTheta       = [x~y, Ord x]
+        --      dcOrigArgTys       = [x,y]
+        --      dcRepTyCon         = T
 
         -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
         -- FOR THE PARENT TyCon. (This is a change (Oct05): previously, vanilla
         -- datacons guaranteed to have the same type variables as their parent TyCon,
-        -- but that seems ugly.)
+        -- but that seems ugly.) They can be different in the case where a GADT
+        -- constructor uses different names for the universal tyvars than does
+        -- the tycon. For example:
+        --
+        --   data H a where
+        --     MkH :: b -> H b
+        --
+        -- Here, the tyConTyVars of H will be [a], but the dcUnivTyVars of MkH
+        -- will be [b].
 
         dcVanilla :: Bool,      -- True <=> This is a vanilla Haskell 98 data constructor
                                 --          Its type is of form
@@ -314,14 +324,21 @@ data DataCon
         -- INVARIANT: result type of data con worker is exactly (T a b c)
         -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
         --            the tyConTyVars of the parent TyCon
-        dcUnivTyVars    :: [TyVarBinder],
+        dcUnivTyVars    :: [TyVar],
 
         -- Existentially-quantified type vars [x,y]
-        dcExTyVars     :: [TyVarBinder],
+        dcExTyVars     :: [TyVar],
 
         -- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
         -- Reason: less confusing, and easier to generate IfaceSyn
 
+        -- The type vars in the order the user wrote them [y,x]
+        -- INVARIANT: the set of tyvars in dcUserTyVarBinders is exactly the
+        --            set of dcExTyVars unioned with the set of dcUnivTyVars
+        --            whose tyvars do not appear in dcEqSpec
+        -- See Note [DataCon user type variable binders]
+        dcUserTyVarBinders :: [TyVarBinder],
+
         dcEqSpec :: [EqSpec],   -- Equalities derived from the result type,
                                 -- _as written by the programmer_
 
@@ -432,6 +449,9 @@ we can construct the right type for the DataCon with its foralls
 attributed the correct visibility.  That in turn governs whether you
 can use visible type application at a call of the data constructor.
 
+See also [DataCon user type variable binders] for an extended discussion on the
+order in which TyVarBinders appear in a DataCon.
+
 Note [DataCon arities]
 ~~~~~~~~~~~~~~~~~~~~~~
 dcSourceArity does not take constraints into account,
@@ -439,6 +459,83 @@ but dcRepArity does.  For example:
    MkT :: Ord a => a -> T a
     dcSourceArity = 1
     dcRepArity    = 2
+
+Note [DataCon user type variable binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In System FC, data constructor type signatures always quantify over all of
+their universal type variables, followed by their existential type variables.
+Normally, this isn't a problem, as most datatypes naturally quantify their type
+variables in this order anyway. For example:
+
+  data T a b = forall c. MkT b c
+
+Here, we have `MkT :: forall {k} (a :: k) (b :: *) (c :: *). b -> c -> T a b`,
+where k, a, and b are universal and c is existential. (The inferred variable k
+isn't available for TypeApplications, hence why it's in braces.) This is a
+perfectly reasonable order to use, as the syntax of H98-style datatypes
+(+ ExistentialQuantification) suggests it.
+
+Things become more complicated when GADT syntax enters the picture. Consider
+this example:
+
+  data X a where
+    MkX :: forall b a. b -> Proxy a -> X a
+
+If we adopt the earlier approach of quantifying all the universal variables
+followed by all the existential ones, GHC would come up with this type
+signature for MkX:
+
+  MkX :: forall {k} (a :: k) (b :: *). b -> Proxy a -> X a
+
+But this is not what we want at all! After all, if a user were to use
+TypeApplications on MkX, they would expect to instantiate `b` before `a`,
+as that's the order in which they were written in the `forall`. (See #11721.)
+Instead, we'd like GHC to come up with this type signature:
+
+  MkX :: forall {k} (b :: *) (a :: k). b -> Proxy a -> X a
+
+In fact, even if we left off the explicit forall:
+
+  data X a where
+    MkX :: b -> Proxy a -> X a
+
+Then a user should still expect `b` to be quantified before `a`, since
+according to the rules of TypeApplications, in the absence of `forall` GHC
+performs a stable topological sort on the type variables in the user-written
+type signature, which would place `b` before `a`.
+
+But as noted above, enacting this behavior is not entirely trivial, as System
+FC demands the variables go in universal-then-existential order under the hood.
+Our solution is thus to equip DataCon with two different sets of type
+variables:
+
+* dcUnivTyVars and dcExTyVars, for the universal and existential type
+  variables, respectively. Their order is irrelevant for the purposes of
+  TypeApplications, and as a consequence, they do not come equipped with
+  visibilities (that is, they are TyVars instead of TyVarBinders).
+* dcUserTyVarBinders, for the type variables binders in the order in which they
+  originally arose in the user-written type signature. Their order *does*
+  matter for TypeApplications, so they are full TyVarBinders, complete
+  with visibilities.
+
+This encoding has some redundancy. The set of tyvars in dcUserTyVarBinders
+consists precisely of:
+
+* The set of tyvars in dcUnivTyVars whose type variables do not appear in
+  dcEqSpec, unioned with:
+* The set of tyvars in dcExTyVars
+
+The word "set" is used above because the order in which the tyvars
+appear in dcUserTyVarBinders can be completely different from the order in
+dcUnivTyVars or dcExTyVars. That is, the tyvars in dcUserTyVarBinders are a
+permutation of (dcExTyVars + a subset of dcUnivTyVars). But aside from the
+ordering, they in fact share the same type variables (with the same Uniques).
+We sometimes refer to this as "the dcUserTyVarBinders invariant".
+
+dcUserTyVarBinders, as the name suggests, is the one that users will see most
+of the time. It's used when computing the type signature of a data constructor
+(see dataConUserType), and as a result, it's what matters from a
+TypeApplications perspective.
 -}
 
 -- | Data Constructor Representation
@@ -570,13 +667,12 @@ substEqSpec subst (EqSpec tv ty)
   where
     tv' = getTyVar "substEqSpec" (substTyVar subst tv)
 
--- | Filter out any TyBinders mentioned in an EqSpec
-filterEqSpec :: [EqSpec] -> [TyVarBinder] -> [TyVarBinder]
+-- | Filter out any 'TyVar's mentioned in an 'EqSpec'.
+filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
 filterEqSpec eq_spec
   = filter not_in_eq_spec
   where
-    not_in_eq_spec bndr = let var = binderVar bndr in
-                          all (not . (== var) . eqSpecTyVar) eq_spec
+    not_in_eq_spec var = all (not . (== var) . eqSpecTyVar) eq_spec
 
 instance Outputable EqSpec where
   ppr (EqSpec tv ty) = ppr (tv, ty)
@@ -754,9 +850,11 @@ mkDataCon :: Name
           -> [HsSrcBang]    -- ^ Strictness/unpack annotations, from user
           -> [FieldLabel]   -- ^ Field labels for the constructor,
                             -- if it is a record, otherwise empty
-          -> [TyVarBinder]  -- ^ Universals. See Note [TyVarBinders in DataCons]
-          -> [TyVarBinder]  -- ^ Existentials.
-                            -- (These last two must be Named and Inferred/Specified)
+          -> [TyVar]        -- ^ Universals.
+          -> [TyVar]        -- ^ Existentials.
+          -> [TyVarBinder]  -- ^ User-written 'TyVarBinder's.
+                            --   These must be Inferred/Specified.
+                            --   See @Note [TyVarBinders in DataCons]@
           -> [EqSpec]       -- ^ GADT equalities
           -> ThetaType      -- ^ Theta-type occuring before the arguments proper
           -> [Type]         -- ^ Original argument types
@@ -773,11 +871,11 @@ mkDataCon :: Name
 mkDataCon name declared_infix prom_info
           arg_stricts   -- Must match orig_arg_tys 1-1
           fields
-          univ_tvs ex_tvs
+          univ_tvs ex_tvs user_tvbs
           eq_spec theta
           orig_arg_tys orig_res_ty rep_info rep_tycon
           stupid_theta work_id rep
--- Warning: mkDataCon is not a good place to check invariants.
+-- Warning: mkDataCon is not a good place to check certain invariants.
 -- If the programmer writes the wrong result type in the decl, thus:
 --      data T a where { MkT :: S }
 -- then it's possible that the univ_tvs may hit an assertion failure
@@ -788,10 +886,20 @@ mkDataCon name declared_infix prom_info
   = con
   where
     is_vanilla = null ex_tvs && null eq_spec && null theta
+    -- Check the dcUserTyVarBinders invariant
+    -- (see Note [DataCon user type variable binders])
+    user_tvbs_invariant =
+         Set.fromList (filterEqSpec eq_spec univ_tvs ++ ex_tvs)
+      == Set.fromList (binderVars user_tvbs)
+    user_tvbs' =
+      ASSERT2( user_tvbs_invariant
+             , ppr univ_tvs $$ ppr ex_tvs $$ ppr user_tvbs )
+      user_tvbs
     con = MkData {dcName = name, dcUnique = nameUnique name,
                   dcVanilla = is_vanilla, dcInfix = declared_infix,
                   dcUnivTyVars = univ_tvs,
                   dcExTyVars = ex_tvs,
+                  dcUserTyVarBinders = user_tvbs',
                   dcEqSpec = eq_spec,
                   dcOtherTheta = theta,
                   dcStupidTheta = stupid_theta,
@@ -812,13 +920,20 @@ mkDataCon name declared_infix prom_info
     tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con
     rep_arg_tys = dataConRepArgTys con
 
-    rep_ty = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $
-             mkFunTys rep_arg_tys $
-             mkTyConApp rep_tycon (mkTyVarTys (binderVars univ_tvs))
+    mk_rep_for_all_tys =
+      case rep of
+        -- If the DataCon has no wrapper, then the worker's type *is* the
+        -- user-facing type, so we can simply use user_tvbs.
+        NoDataConRep -> mkForAllTys user_tvbs'
+        -- If the DataCon has a wrapper, then the worker's type is never seen
+        -- by the user. The visibilities we pick do not matter here.
+        DCR{} -> mkInvForAllTys univ_tvs . mkInvForAllTys ex_tvs
+    rep_ty = mk_rep_for_all_tys $ mkFunTys rep_arg_tys $
+             mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
 
       -- See Note [Promoted data constructors] in TyCon
     prom_tv_bndrs = [ mkNamedTyConBinder vis tv
-                    | TvBndr tv vis <- filterEqSpec eq_spec univ_tvs ++ ex_tvs ]
+                    | TvBndr tv vis <- user_tvbs' ]
 
     prom_arg_bndrs = mkCleanAnonTyConBinders prom_tv_bndrs (theta ++ orig_arg_tys)
     prom_res_kind  = orig_res_ty
@@ -892,24 +1007,27 @@ dataConIsInfix = dcInfix
 
 -- | The universally-quantified type variables of the constructor
 dataConUnivTyVars :: DataCon -> [TyVar]
-dataConUnivTyVars (MkData { dcUnivTyVars = tvbs }) = binderVars tvbs
-
--- | 'TyBinder's for the universally-quantified type variables
-dataConUnivTyVarBinders :: DataCon -> [TyVarBinder]
-dataConUnivTyVarBinders = dcUnivTyVars
+dataConUnivTyVars (MkData { dcUnivTyVars = tvbs }) = tvbs
 
 -- | The existentially-quantified type variables of the constructor
 dataConExTyVars :: DataCon -> [TyVar]
-dataConExTyVars (MkData { dcExTyVars = tvbs }) = binderVars tvbs
-
--- | 'TyBinder's for the existentially-quantified type variables
-dataConExTyVarBinders :: DataCon -> [TyVarBinder]
-dataConExTyVarBinders = dcExTyVars
+dataConExTyVars (MkData { dcExTyVars = tvbs }) = tvbs
 
 -- | Both the universal and existential type variables of the constructor
-dataConAllTyVars :: DataCon -> [TyVar]
-dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
-  = binderVars (univ_tvs ++ ex_tvs)
+dataConUnivAndExTyVars :: DataCon -> [TyVar]
+dataConUnivAndExTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
+  = univ_tvs ++ ex_tvs
+
+-- See Note [DataCon user type variable binders]
+-- | The type variables of the constructor, in the order the user wrote them
+dataConUserTyVars :: DataCon -> [TyVar]
+dataConUserTyVars (MkData { dcUserTyVarBinders = tvbs }) = binderVars tvbs
+
+-- See Note [DataCon user type variable binders]
+-- | 'TyVarBinder's for the type variables of the constructor, in the order the
+-- user wrote them
+dataConUserTyVarBinders :: DataCon -> [TyVarBinder]
+dataConUserTyVarBinders = dcUserTyVarBinders
 
 -- | Equalities derived from the result type of the data constructor, as written
 -- by the programmer in any GADT declaration. This includes *all* GADT-like
@@ -1039,7 +1157,7 @@ dataConBoxer _ = Nothing
 
 -- | The \"signature\" of the 'DataCon' returns, in order:
 --
--- 1) The result of 'dataConAllTyVars',
+-- 1) The result of 'dataConUnivAndExTyVars',
 --
 -- 2) All the 'ThetaType's relating to the 'DataCon' (coercion, dictionary, implicit
 --    parameter - whatever)
@@ -1049,7 +1167,7 @@ dataConBoxer _ = Nothing
 -- 4) The /original/ result type of the 'DataCon'
 dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
 dataConSig con@(MkData {dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
-  = (dataConAllTyVars con, dataConTheta con, arg_tys, res_ty)
+  = (dataConUnivAndExTyVars con, dataConTheta con, arg_tys, res_ty)
 
 dataConInstSig
   :: DataCon
@@ -1066,9 +1184,8 @@ dataConInstSig (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs
     , substTheta subst (eqSpecPreds eq_spec ++ theta)
     , substTys   subst arg_tys)
   where
-    univ_subst = zipTvSubst (binderVars univ_tvs) univ_tys
-    (subst, ex_tvs') = mapAccumL Type.substTyVarBndr univ_subst $
-                       binderVars ex_tvs
+    univ_subst = zipTvSubst univ_tvs univ_tys
+    (subst, ex_tvs') = mapAccumL Type.substTyVarBndr univ_subst ex_tvs
 
 
 -- | The \"full signature\" of the 'DataCon' returns, in order:
@@ -1090,7 +1207,7 @@ dataConFullSig :: DataCon
 dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
                         dcEqSpec = eq_spec, dcOtherTheta = theta,
                         dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
-  = (binderVars univ_tvs, binderVars ex_tvs, eq_spec, theta, arg_tys, res_ty)
+  = (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
 
 dataConOrigResTy :: DataCon -> Type
 dataConOrigResTy dc = dcOrigResTy dc
@@ -1111,14 +1228,15 @@ dataConUserType :: DataCon -> Type
 --
 -- > T :: forall a c. forall b. (c~[a]) => a -> b -> T c
 --
+-- The type variables are quantified in the order that the user wrote them.
+-- See @Note [DataCon user type variable binders]@.
+--
 -- NB: If the constructor is part of a data instance, the result type
 -- mentions the family tycon, not the internal one.
-dataConUserType (MkData { dcUnivTyVars = univ_tvs,
-                          dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
+dataConUserType (MkData { dcUserTyVarBinders = user_tvbs,
                           dcOtherTheta = theta, dcOrigArgTys = arg_tys,
                           dcOrigResTy = res_ty })
-  = mkForAllTys (filterEqSpec eq_spec univ_tvs) $
-    mkForAllTys ex_tvs $
+  = mkForAllTys user_tvbs $
     mkFunTys theta $
     mkFunTys arg_tys $
     res_ty
@@ -1137,7 +1255,7 @@ dataConInstArgTys dc@(MkData {dcUnivTyVars = univ_tvs,
  = ASSERT2( univ_tvs `equalLength` inst_tys
           , text "dataConInstArgTys" <+> ppr dc $$ ppr univ_tvs $$ ppr inst_tys)
    ASSERT2( null ex_tvs, ppr dc )
-   map (substTyWith (binderVars univ_tvs) inst_tys) (dataConRepArgTys dc)
+   map (substTyWith univ_tvs inst_tys) (dataConRepArgTys dc)
 
 -- | Returns just the instantiated /value/ argument types of a 'DataCon',
 -- (excluding dictionary args)
@@ -1155,7 +1273,7 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
           , text "dataConInstOrigArgTys" <+> ppr dc $$ ppr tyvars $$ ppr inst_tys )
     map (substTyWith tyvars inst_tys) arg_tys
   where
-    tyvars = binderVars (univ_tvs ++ ex_tvs)
+    tyvars = univ_tvs ++ ex_tvs
 
 -- | Returns the argument types of the wrapper, excluding all dictionary arguments
 -- and without substituting for any type variables
@@ -1245,6 +1363,23 @@ dataConCannotMatch tys con
                        | eq `hasKey` eqTyConKey -> [(ty1, ty2)]
                      _                          -> []
 
+-- | Were the type variables of the data con written in a different order
+-- than the regular order (universal tyvars followed by existential tyvars)?
+--
+-- This is not a cheap test, so we minimize its use in GHC as much as possible.
+-- Currently, its only call site in the GHC codebase is in 'mkDataConRep' in
+-- "MkId", and so 'dataConUserTyVarsArePermuted' is only called at most once
+-- during a data constructor's lifetime.
+
+-- See Note [DataCon user type variable binders], as well as
+-- Note [Data con wrappers and GADT syntax] for an explanation of what
+-- mkDataConRep is doing with this function.
+dataConUserTyVarsArePermuted :: DataCon -> Bool
+dataConUserTyVarsArePermuted (MkData { dcUnivTyVars = univ_tvs,
+                                       dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
+                                       dcUserTyVarBinders = user_tvbs }) =
+  (filterEqSpec eq_spec univ_tvs ++ ex_tvs) /= binderVars user_tvbs
+
 {-
 %************************************************************************
 %*                                                                      *
diff --git a/compiler/basicTypes/DataCon.hs-boot b/compiler/basicTypes/DataCon.hs-boot
index 95216b063c..a223c4f306 100644
--- a/compiler/basicTypes/DataCon.hs-boot
+++ b/compiler/basicTypes/DataCon.hs-boot
@@ -13,13 +13,13 @@ import {-# SOURCE #-} TyCoRep ( Type, ThetaType )
 data DataCon
 data DataConRep
 data EqSpec
-filterEqSpec :: [EqSpec] -> [TyVarBinder] -> [TyVarBinder]
+filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
 
 dataConName      :: DataCon -> Name
 dataConTyCon     :: DataCon -> TyCon
-dataConUnivTyVarBinders :: DataCon -> [TyVarBinder]
 dataConExTyVars  :: DataCon -> [TyVar]
-dataConExTyVarBinders :: DataCon -> [TyVarBinder]
+dataConUserTyVars :: DataCon -> [TyVar]
+dataConUserTyVarBinders :: DataCon -> [TyVarBinder]
 dataConSourceArity  :: DataCon -> Arity
 dataConFieldLabels :: DataCon -> [FieldLabel]
 dataConInstOrigArgTys  :: DataCon -> [Type] -> [Type]
diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index b1161ee13c..18be9c9657 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -278,7 +278,7 @@ mkDictSelId name clas
     sel_names      = map idName (classAllSelIds clas)
     new_tycon      = isNewTyCon tycon
     [data_con]     = tyConDataCons tycon
-    tyvars         = dataConUnivTyVarBinders data_con
+    tyvars         = dataConUserTyVarBinders data_con
     n_ty_args      = length tyvars
     arg_tys        = dataConRepArgTys data_con  -- Includes the dictionary superclasses
     val_index      = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
@@ -553,7 +553,6 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
              -- Passing Nothing here allows the wrapper to inline when
              -- unsaturated.
              wrap_unf = mkInlineUnfolding wrap_rhs
-             wrap_tvs = (univ_tvs `minusList` map eqSpecTyVar eq_spec) ++ ex_tvs
              wrap_rhs = mkLams wrap_tvs $
                         mkLams wrap_args $
                         wrapFamInstBody tycon res_ty_args $
@@ -568,6 +567,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
   where
     (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, _orig_res_ty)
       = dataConFullSig data_con
+    wrap_tvs     = dataConUserTyVars data_con
     res_ty_args  = substTyVars (mkTvSubstPrs (map eqSpecPair eq_spec)) univ_tvs
 
     tycon        = dataConTyCon data_con       -- The representation TyCon (not family)
@@ -595,11 +595,20 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
     (unboxers, boxers) = unzip wrappers
     (rep_tys, rep_strs) = unzip (concat rep_tys_w_strs)
 
-    wrapper_reqd = not (isNewTyCon tycon)  -- Newtypes have only a worker
-                && (any isBanged (ev_ibangs ++ arg_ibangs)
-                      -- Some forcing/unboxing (includes eq_spec)
-                    || isFamInstTyCon tycon  -- Cast result
-                    || (not $ null eq_spec)) -- GADT
+    wrapper_reqd =
+        (not (isNewTyCon tycon)
+                     -- (Most) newtypes have only a worker, with the exception
+                     -- of some newtypes written with GADT syntax. See below.
+         && (any isBanged (ev_ibangs ++ arg_ibangs)
+                     -- Some forcing/unboxing (includes eq_spec)
+             || isFamInstTyCon tycon  -- Cast result
+             || (not $ null eq_spec))) -- GADT
+      || dataConUserTyVarsArePermuted data_con
+                     -- If the data type was written with GADT syntax and
+                     -- orders the type variables differently from what the
+                     -- worker expects, it needs a data con wrapper to reorder
+                     -- the type variables.
+                     -- See Note [Data con wrappers and GADT syntax].
 
     initial_wrap_app = Var (dataConWorkId data_con)
                        `mkTyApps`  res_ty_args
@@ -677,6 +686,40 @@ For a start, it's still to generate a no-op.  But worse, since wrappers
 are currently injected at TidyCore, we don't even optimise it away!
 So the stupid case expression stays there.  This actually happened for
 the Integer data type (see Trac #1600 comment:66)!
+
+Note [Data con wrappers and GADT syntax]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider these two very similar data types:
+
+  data T1 a b = MkT1 b
+
+  data T2 a b where
+    MkT2 :: forall b a. b -> T2 a b
+
+Despite their similar appearance, T2 will have a data con wrapper but T1 will
+not. What sets them apart? The types of their constructors, which are:
+
+  MkT1 :: forall a b. b -> T1 a b
+  MkT2 :: forall b a. b -> T2 a b
+
+MkT2's use of GADT syntax allows it to permute the order in which `a` and `b`
+would normally appear. See Note [DataCon user type variable binders] in DataCon
+for further discussion on this topic.
+
+The worker data cons for T1 and T2, however, both have types such that `a` is
+expected to come before `b` as arguments. Because MkT2 permutes this order, it
+needs a data con wrapper to swizzle around the type variables to be in the
+order the worker expects.
+
+A somewhat surprising consequence of this is that *newtypes* can have data con
+wrappers! After all, a newtype can also be written with GADT syntax:
+
+  newtype T3 a b where
+    MkT3 :: forall b a. b -> T3 a b
+
+Again, this needs a wrapper data con to reorder the type variables. It does
+mean that this newtype constructor requires another level of indirection when
+being called, but the inliner should make swift work of that.
 -}
 
 -------------------------
diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index 4eb8271477..3d34e6f5fd 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -72,9 +72,12 @@ mkNewTyConRhs tycon_name tycon con
   where
     tvs    = tyConTyVars tycon
     roles  = tyConRoles tycon
-    inst_con_ty = piResultTys (dataConUserType con) (mkTyVarTys tvs)
-    rhs_ty = ASSERT( isFunTy inst_con_ty ) funArgTy inst_con_ty
-        -- Instantiate the data con with the
+    con_arg_ty = case dataConRepArgTys con of
+                   [arg_ty] -> arg_ty
+                   tys -> pprPanic "mkNewTyConRhs" (ppr con <+> ppr tys)
+    rhs_ty = substTyWith (dataConUnivTyVars con)
+                         (mkTyVarTys tvs) con_arg_ty
+        -- Instantiate the newtype's RHS with the
         -- type variables from the tycon
         -- NB: a newtype DataCon has a type that must look like
         --        forall tvs.  <arg-ty> -> T tvs
@@ -109,8 +112,9 @@ buildDataCon :: FamInstEnvs
             -> Maybe [HsImplBang]
                 -- See Note [Bangs on imported data constructors] in MkId
            -> [FieldLabel]             -- Field labels
-           -> [TyVarBinder]            -- Universals
-           -> [TyVarBinder]            -- Existentials
+           -> [TyVar]                  -- Universals
+           -> [TyVar]                  -- Existentials
+           -> [TyVarBinder]            -- User-written 'TyVarBinder's
            -> [EqSpec]                 -- Equality spec
            -> ThetaType                -- Does not include the "stupid theta"
                                        -- or the GADT equalities
@@ -122,7 +126,7 @@ buildDataCon :: FamInstEnvs
 --   b) makes the wrapper Id if necessary, including
 --      allocating its unique (hence monadic)
 buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs field_lbls
-             univ_tvs ex_tvs eq_spec ctxt arg_tys res_ty rep_tycon
+             univ_tvs ex_tvs user_tvbs eq_spec ctxt arg_tys res_ty rep_tycon
   = do  { wrap_name <- newImplicitBinder src_name mkDataConWrapperOcc
         ; work_name <- newImplicitBinder src_name mkDataConWorkerOcc
         -- This last one takes the name of the data constructor in the source
@@ -135,7 +139,7 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs fie
         ; let stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs
               data_con = mkDataCon src_name declared_infix prom_info
                                    src_bangs field_lbls
-                                   univ_tvs ex_tvs eq_spec ctxt
+                                   univ_tvs ex_tvs user_tvbs eq_spec ctxt
                                    arg_tys res_ty NoRRI rep_tycon
                                    stupid_ctxt dc_wrk dc_rep
               dc_wrk = mkDataConWorkId work_name data_con
@@ -150,13 +154,13 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs fie
 -- the type variables mentioned in the arg_tys
 -- ToDo: Or functionally dependent on?
 --       This whole stupid theta thing is, well, stupid.
-mkDataConStupidTheta :: TyCon -> [Type] -> [TyVarBinder] -> [PredType]
+mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType]
 mkDataConStupidTheta tycon arg_tys univ_tvs
   | null stupid_theta = []      -- The common case
   | otherwise         = filter in_arg_tys stupid_theta
   where
     tc_subst     = zipTvSubst (tyConTyVars tycon)
-                              (mkTyVarTys (binderVars univ_tvs))
+                              (mkTyVarTys univ_tvs)
     stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
         -- Start by instantiating the master copy of the
         -- stupid theta, taken from the TyCon
@@ -308,8 +312,9 @@ buildClass tycon_name binders roles fds
                                    (map (const no_bang) args)
                                    (Just (map (const HsLazy) args))
                                    [{- No fields -}]
-                                   univ_bndrs
+                                   univ_tvs
                                    [{- no existentials -}]
+                                   univ_bndrs
                                    [{- No GADT equalities -}]
                                    [{- No theta -}]
                                    arg_tys
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index c047343c2d..885e119abc 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -66,7 +66,7 @@ import Binary
 import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
 import Var( TyVarBndr(..) )
 import TyCon ( Role (..), Injectivity(..) )
-import Util( filterOut, filterByList )
+import Util( dropList, filterByList )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
 import Lexeme (isLexSym)
 import DynFlags
@@ -240,7 +240,14 @@ data IfaceConDecl
         -- but it's not so easy for the original TyCon/DataCon
         -- So this guarantee holds for IfaceConDecl, but *not* for DataCon
 
-        ifConExTvs   :: [IfaceForAllBndr],  -- Existential tyvars (w/ visibility)
+        ifConExTvs   :: [IfaceTvBndr],  -- Existential tyvars
+        ifConUserTvBinders :: [IfaceForAllBndr],
+          -- The tyvars, in the order the user wrote them
+          -- INVARIANT: the set of tyvars in ifConUserTvBinders is exactly the
+          --            set of ifConExTvs, unioned with the set of ifBinders
+          --            (from the parent IfaceDecl) whose tyvars do not appear
+          --            in ifConEqSpec
+          -- See Note [DataCon user type variable binders] in DataCon
         ifConEqSpec  :: IfaceEqSpec,        -- Equality constraints
         ifConCtxt    :: IfaceContext,       -- Non-stupid context
         ifConArgTys  :: [IfaceType],        -- Arg types
@@ -961,7 +968,7 @@ pprIfaceConDecl :: ShowSub -> Bool
                 -> IfaceConDecl -> SDoc
 pprIfaceConDecl ss gadt_style tycon tc_binders parent
         (IfCon { ifConName = name, ifConInfix = is_infix,
-                 ifConExTvs = ex_tvs,
+                 ifConUserTvBinders = user_tvbs,
                  ifConEqSpec = eq_spec, ifConCtxt = ctxt, ifConArgTys = arg_tys,
                  ifConStricts = stricts, ifConFields = fields })
   | gadt_style = pp_prefix_con <+> dcolon <+> ppr_gadt_ty
@@ -981,19 +988,24 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
     tys_w_strs = zip stricts arg_tys
     pp_prefix_con = pprPrefixIfDeclBndr how_much (occName name)
 
-    (univ_tvs, pp_res_ty) = mk_user_con_res_ty eq_spec
-    ppr_ex_quant = pprIfaceForAllPartMust ex_tvs ctxt
-    ppr_gadt_ty = pprIfaceForAllPart (map tv_to_forall_bndr univ_tvs ++ ex_tvs)
-                                     ctxt pp_tau
+    -- If we're pretty-printing a H98-style declaration with existential
+    -- quantification, then user_tvbs will always consist of the universal
+    -- tyvar binders followed by the existential tyvar binders. So to recover
+    -- the visibilities of the existential tyvar binders, we can simply drop
+    -- the universal tyvar binders from user_tvbs.
+    ex_tvbs = dropList tc_binders user_tvbs
+    ppr_ex_quant = pprIfaceForAllPartMust ex_tvbs ctxt
+    pp_gadt_res_ty = mk_user_con_res_ty eq_spec
+    ppr_gadt_ty = pprIfaceForAllPart user_tvbs ctxt pp_tau
 
         -- A bit gruesome this, but we can't form the full con_tau, and ppr it,
         -- because we don't have a Name for the tycon, only an OccName
     pp_tau | null fields
-           = case pp_args ++ [pp_res_ty] of
+           = case pp_args ++ [pp_gadt_res_ty] of
                 (t:ts) -> fsep (t : map (arrow <+>) ts)
                 []     -> panic "pp_con_taus"
            | otherwise
-           = sep [pp_field_args, arrow <+> pp_res_ty]
+           = sep [pp_field_args, arrow <+> pp_gadt_res_ty]
 
     ppr_bang IfNoBang = whenPprDebug $ char '_'
     ppr_bang IfStrict = char '!'
@@ -1029,17 +1041,15 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
         sel = flSelector lbl
         occ = mkVarOccFS (flLabel lbl)
 
-    mk_user_con_res_ty :: IfaceEqSpec -> ([IfaceTvBndr], SDoc)
+    mk_user_con_res_ty :: IfaceEqSpec -> SDoc
     -- See Note [Result type of a data family GADT]
     mk_user_con_res_ty eq_spec
       | IfDataInstance _ tc tys <- parent
-      = (con_univ_tvs, pprIfaceType (IfaceTyConApp tc (substIfaceTcArgs gadt_subst tys)))
+      = pprIfaceType (IfaceTyConApp tc (substIfaceTcArgs gadt_subst tys))
       | otherwise
-      = (con_univ_tvs, sdocWithDynFlags (ppr_tc_app gadt_subst))
+      = sdocWithDynFlags (ppr_tc_app gadt_subst)
       where
         gadt_subst = mkIfaceTySubst eq_spec
-        con_univ_tvs = filterOut (inDomIfaceTySubst gadt_subst) $
-                       map ifTyConBinderTyVar tc_binders
 
     ppr_tc_app gadt_subst dflags
        = pprPrefixIfDeclBndr how_much (occName tycon)
@@ -1081,9 +1091,6 @@ ppr_rough :: Maybe IfaceTyCon -> SDoc
 ppr_rough Nothing   = dot
 ppr_rough (Just tc) = ppr tc
 
-tv_to_forall_bndr :: IfaceTvBndr -> IfaceForAllBndr
-tv_to_forall_bndr tv = TvBndr tv Specified
-
 {-
 Note [Result type of a data family GADT]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1381,7 +1388,7 @@ freeNamesIfConDecl (IfCon { ifConExTvs   = ex_tvs, ifConCtxt = ctxt
                           , ifConFields  = flds
                           , ifConEqSpec  = eq_spec
                           , ifConStricts = bangs })
-  = freeNamesIfTyVarBndrs ex_tvs &&&
+  = fnList freeNamesIfTvBndr ex_tvs &&&
     freeNamesIfContext ctxt &&&
     fnList freeNamesIfType arg_tys &&&
     mkNameSet (map flSelector flds) &&&
@@ -1865,7 +1872,7 @@ instance Binary IfaceConDecls where
             _ -> error "Binary(IfaceConDecls).get: Invalid IfaceConDecls"
 
 instance Binary IfaceConDecl where
-    put_ bh (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) = do
+    put_ bh (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) = do
         putIfaceTopBndr bh a1
         put_ bh a2
         put_ bh a3
@@ -1873,10 +1880,11 @@ instance Binary IfaceConDecl where
         put_ bh a5
         put_ bh a6
         put_ bh a7
-        put_ bh (length a8)
-        mapM_ (put_ bh) a8
-        put_ bh a9
+        put_ bh a8
+        put_ bh (length a9)
+        mapM_ (put_ bh) a9
         put_ bh a10
+        put_ bh a11
     get bh = do
         a1 <- getIfaceTopBndr bh
         a2 <- get bh
@@ -1885,11 +1893,12 @@ instance Binary IfaceConDecl where
         a5 <- get bh
         a6 <- get bh
         a7 <- get bh
+        a8 <- get bh
         n_fields <- get bh
-        a8 <- replicateM n_fields (get bh)
-        a9 <- get bh
+        a9 <- replicateM n_fields (get bh)
         a10 <- get bh
-        return (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)
+        a11 <- get bh
+        return (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11)
 
 instance Binary IfaceBang where
     put_ bh IfNoBang        = putByte bh 0
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 096430e04f..c287d56688 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -21,6 +21,7 @@ module IfaceType (
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
         IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..),
 
+        ifForAllBndrTyVar, ifForAllBndrName,
         ifTyConBinderTyVar, ifTyConBinderName,
 
         -- Equality testing
@@ -336,11 +337,19 @@ stripIfaceInvisVars dflags tyvars
   | gopt Opt_PrintExplicitKinds dflags = tyvars
   | otherwise = filterOut isInvisibleTyConBinder tyvars
 
--- | Extract a IfaceTvBndr from a IfaceTyConBinder
+-- | Extract an 'IfaceTvBndr' from an 'IfaceForAllBndr'.
+ifForAllBndrTyVar :: IfaceForAllBndr -> IfaceTvBndr
+ifForAllBndrTyVar = binderVar
+
+-- | Extract the variable name from an 'IfaceForAllBndr'.
+ifForAllBndrName :: IfaceForAllBndr -> IfLclName
+ifForAllBndrName fab = ifaceTvBndrName (ifForAllBndrTyVar fab)
+
+-- | Extract an 'IfaceTvBndr' from an 'IfaceTyConBinder'.
 ifTyConBinderTyVar :: IfaceTyConBinder -> IfaceTvBndr
 ifTyConBinderTyVar = binderVar
 
--- | Extract the variable name from a IfaceTyConBinder
+-- | Extract the variable name from an 'IfaceTyConBinder'.
 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
 ifTyConBinderName tcb = ifaceTvBndrName (ifTyConBinderTyVar tcb)
 
diff --git a/compiler/iface/MkIface.hs b/compiler/iface/MkIface.hs
index 184ee48984..a12cff2226 100644
--- a/compiler/iface/MkIface.hs
+++ b/compiler/iface/MkIface.hs
@@ -1643,7 +1643,8 @@ tyConToIfaceDecl env tycon
         = IfCon   { ifConName    = dataConName data_con,
                     ifConInfix   = dataConIsInfix data_con,
                     ifConWrapper = isJust (dataConWrapId_maybe data_con),
-                    ifConExTvs   = map toIfaceForAllBndr ex_bndrs',
+                    ifConExTvs   = map toIfaceTvBndr ex_tvs',
+                    ifConUserTvBinders = map toIfaceForAllBndr user_bndrs',
                     ifConEqSpec  = map (to_eq_spec . eqSpecPair) eq_spec,
                     ifConCtxt    = tidyToIfaceContext con_env2 theta,
                     ifConArgTys  = map (tidyToIfaceType con_env2) arg_tys,
@@ -1653,9 +1654,9 @@ tyConToIfaceDecl env tycon
                     ifConSrcStricts = map toIfaceSrcBang
                                           (dataConSrcBangs data_con)}
         where
-          (univ_tvs, _ex_tvs, eq_spec, theta, arg_tys, _)
+          (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
             = dataConFullSig data_con
-          ex_bndrs = dataConExTyVarBinders data_con
+          user_bndrs = dataConUserTyVarBinders data_con
 
           -- Tidy the univ_tvs of the data constructor to be identical
           -- to the tyConTyVars of the type constructor.  This means
@@ -1667,9 +1668,21 @@ tyConToIfaceDecl env tycon
           con_env1 = (fst tc_env1, mkVarEnv (zipEqual "ifaceConDecl" univ_tvs tc_tyvars))
                      -- A bit grimy, perhaps, but it's simple!
 
-          (con_env2, ex_bndrs') = tidyTyVarBinders con_env1 ex_bndrs
+          (con_env2, ex_tvs') = tidyTyCoVarBndrs con_env1 ex_tvs
+          user_bndrs' = map (tidyUserTyVarBinder con_env2) user_bndrs
           to_eq_spec (tv,ty) = (tidyTyVar con_env2 tv, tidyToIfaceType con_env2 ty)
 
+          -- By this point, we have tidied every universal and existential
+          -- tyvar. Because of the dcUserTyVarBinders invariant
+          -- (see Note [DataCon user type variable binders]), *every*
+          -- user-written tyvar must be contained in the substitution that
+          -- tidying produced. Therefore, tidying the user-written tyvars is a
+          -- simple matter of looking up each variable in the substitution,
+          -- which tidyTyVarOcc accomplishes.
+          tidyUserTyVarBinder :: TidyEnv -> TyVarBinder -> TyVarBinder
+          tidyUserTyVarBinder env (TvBndr tv vis) =
+            TvBndr (tidyTyVarOcc env tv) vis
+
 classToIfaceDecl :: TidyEnv -> Class -> (TidyEnv, IfaceDecl)
 classToIfaceDecl env clas
   = ( env1
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 8633658dd9..6d04171ab7 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -894,11 +894,12 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
         IfNewTyCon  con  -> do  { data_con  <- tc_con_decl con
                                 ; mkNewTyConRhs tycon_name tycon data_con }
   where
-    univ_tv_bndrs :: [TyVarBinder]
-    univ_tv_bndrs = tyConTyVarBinders tc_tybinders
+    univ_tvs :: [TyVar]
+    univ_tvs = binderVars (tyConTyVarBinders tc_tybinders)
 
     tc_con_decl (IfCon { ifConInfix = is_infix,
                          ifConExTvs = ex_bndrs,
+                         ifConUserTvBinders = user_bndrs,
                          ifConName = dc_name,
                          ifConCtxt = ctxt, ifConEqSpec = spec,
                          ifConArgTys = args, ifConFields = lbl_names,
@@ -906,9 +907,19 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
                          ifConSrcStricts = if_src_stricts})
      = -- Universally-quantified tyvars are shared with
        -- parent TyCon, and are already in scope
-       bindIfaceForAllBndrs ex_bndrs    $ \ ex_tv_bndrs -> do
+       bindIfaceTyVars ex_bndrs    $ \ ex_tvs -> do
         { traceIf (text "Start interface-file tc_con_decl" <+> ppr dc_name)
 
+          -- By this point, we have bound every universal and existential
+          -- tyvar. Because of the dcUserTyVarBinders invariant
+          -- (see Note [DataCon user type variable binders]), *every* tyvar in
+          -- ifConUserTvBinders has a matching counterpart somewhere in the
+          -- bound universals/existentials. As a result, calling tcIfaceTyVar
+          -- below is always guaranteed to succeed.
+        ; user_tv_bndrs <- mapM (\(TvBndr (name, _) vis) ->
+                                    TvBndr <$> tcIfaceTyVar name <*> pure vis)
+                                user_bndrs
+
         -- Read the context and argument types, but lazily for two reasons
         -- (a) to avoid looking tugging on a recursive use of
         --     the type itself, which is knot-tied
@@ -947,7 +958,7 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
                        -- worker.
                        -- See Note [Bangs on imported data constructors] in MkId
                        lbl_names
-                       univ_tv_bndrs ex_tv_bndrs
+                       univ_tvs ex_tvs user_tv_bndrs
                        eq_spec theta
                        arg_tys orig_res_ty tycon
         ; traceIf (text "Done interface-file tc_con_decl" <+> ppr dc_name)
@@ -1839,6 +1850,13 @@ bindIfaceForAllBndr :: IfaceForAllBndr -> (TyVar -> ArgFlag -> IfL a) -> IfL a
 bindIfaceForAllBndr (TvBndr tv vis) thing_inside
   = bindIfaceTyVar tv $ \tv' -> thing_inside tv' vis
 
+bindIfaceTyVars :: [IfaceTvBndr] -> ([TyVar] -> IfL a) -> IfL a
+bindIfaceTyVars [] thing_inside = thing_inside []
+bindIfaceTyVars (tv:tvs) thing_inside
+  = bindIfaceTyVar tv   $ \tv' ->
+    bindIfaceTyVars tvs $ \tvs' ->
+    thing_inside (tv' : tvs')
+
 bindIfaceTyVar :: IfaceTvBndr -> (TyVar -> IfL a) -> IfL a
 bindIfaceTyVar (occ,kind) thing_inside
   = do  { name <- newIfaceName (mkTyVarOccFS occ)
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 01579830f8..2033fcff36 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -490,12 +490,15 @@ pcTyCon is_enum name cType tyvars cons
                 False           -- Not in GADT syntax
 
 pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
-pcDataCon n univs = pcDataConWithFixity False n univs []  -- no ex_tvs
+pcDataCon n univs = pcDataConWithFixity False n univs
+                      []    -- no ex_tvs
+                      univs -- the univs are precisely the user-written tyvars
 
 pcDataConWithFixity :: Bool      -- ^ declared infix?
                     -> Name      -- ^ datacon name
                     -> [TyVar]   -- ^ univ tyvars
                     -> [TyVar]   -- ^ ex tyvars
+                    -> [TyVar]   -- ^ user-written tyvars
                     -> [Type]    -- ^ args
                     -> TyCon
                     -> DataCon
@@ -509,19 +512,20 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (n
 -- one DataCon unique per pair of Ints.
 
 pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
-                     -> [TyVar] -> [TyVar]
+                     -> [TyVar] -> [TyVar] -> [TyVar]
                      -> [Type] -> TyCon -> DataCon
 -- The Name should be in the DataName name space; it's the name
 -- of the DataCon itself.
 
-pcDataConWithFixity' declared_infix dc_name wrk_key rri tyvars ex_tyvars arg_tys tycon
+pcDataConWithFixity' declared_infix dc_name wrk_key rri
+                     tyvars ex_tyvars user_tyvars arg_tys tycon
   = data_con
   where
     data_con = mkDataCon dc_name declared_infix prom_info
                 (map (const no_bang) arg_tys)
                 []      -- No labelled fields
-                (mkTyVarBinders Specified tyvars)
-                (mkTyVarBinders Specified ex_tyvars)
+                tyvars ex_tyvars
+                (mkTyVarBinders Specified user_tyvars)
                 []      -- No equality spec
                 []      -- No theta
                 arg_tys (mkTyConApp tycon (mkTyVarTys tyvars))
@@ -552,7 +556,7 @@ mkDataConWorkerName data_con wrk_key =
 pcSpecialDataCon :: Name -> [Type] -> TyCon -> RuntimeRepInfo -> DataCon
 pcSpecialDataCon dc_name arg_tys tycon rri
   = pcDataConWithFixity' False dc_name (dataConWorkerUnique (nameUnique dc_name)) rri
-                         [] [] arg_tys tycon
+                         [] [] [] arg_tys tycon
 
 {-
 ************************************************************************
@@ -1418,7 +1422,8 @@ nilDataCon  = pcDataCon nilDataConName alpha_tyvar [] listTyCon
 consDataCon :: DataCon
 consDataCon = pcDataConWithFixity True {- Declared infix -}
                consDataConName
-               alpha_tyvar [] [alphaTy, mkTyConApp listTyCon alpha_ty] listTyCon
+               alpha_tyvar [] alpha_tyvar
+               [alphaTy, mkTyConApp listTyCon alpha_ty] listTyCon
 -- Interesting: polymorphic recursion would help here.
 -- We can't use (mkListTy alphaTy) in the defn of consDataCon, else mkListTy
 -- gets the over-specific type (Type -> Type)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index fa8b2bbdc2..58a45a954b 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1692,16 +1692,22 @@ tcConDecl rep_tycon tmpl_bndrs res_tmpl
        -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
        ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
        ; let
-           ex_tvs = mkTyVarBinders Inferred qkvs ++
-                    mkTyVarBinders Specified user_qtvs
+           univ_tvbs = tyConTyVarBinders tmpl_bndrs
+           univ_tvs  = binderVars univ_tvbs
+           ex_tvbs   = mkTyVarBinders Inferred qkvs ++
+                       mkTyVarBinders Specified user_qtvs
+           ex_tvs    = qkvs ++ user_qtvs
+           -- For H98 datatypes, the user-written tyvar binders are precisely
+           -- the universals followed by the existentials.
+           -- See Note [DataCon user type variable binders] in DataCon.
+           user_tvbs = univ_tvbs ++ ex_tvbs
            buildOneDataCon (L _ name) = do
              { is_infix <- tcConIsInfixH98 name hs_details
              ; rep_nm   <- newTyConRepName name
 
              ; buildDataCon fam_envs name is_infix rep_nm
                             stricts Nothing field_lbls
-                            (tyConTyVarBinders tmpl_bndrs)
-                            ex_tvs
+                            univ_tvs ex_tvs user_tvbs
                             [{- no eq_preds -}] ctxt arg_tys
                             res_tmpl rep_tycon
                   -- NB:  we put data_tc, the type constructor gotten from the
@@ -1726,24 +1732,30 @@ tcConDecl rep_tycon tmpl_bndrs res_tmpl
        ; tkvs <- quantifyTyVars emptyVarSet vars
 
              -- Zonk to Types
-       ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (tkvs ++ user_tvs)
+       ; (ze, tkvs)     <- zonkTyBndrsX emptyZonkEnv tkvs
+       ; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs
        ; arg_tys <- zonkTcTypeToTypes ze arg_tys
        ; ctxt    <- zonkTcTypeToTypes ze ctxt
        ; res_ty  <- zonkTcTypeToType ze res_ty
 
-       ; let (univ_tvs, ex_tvs, eq_preds, arg_subst)
-               = rejigConRes tmpl_bndrs res_tmpl qtkvs res_ty
-             -- NB: this is a /lazy/ binding, so we pass four thunks to
+       ; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst)
+               = rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty
+             -- NB: this is a /lazy/ binding, so we pass six thunks to
              --     buildDataCon without yet forcing the guards in rejigConRes
              -- See Note [Checking GADT return types]
 
-             -- See Note [Wrong visibility for GADTs]
-             univ_bndrs = mkTyVarBinders Specified univ_tvs
-             ex_bndrs   = mkTyVarBinders Specified ex_tvs
+             -- Compute the user-written tyvar binders. These have the same
+             -- tyvars as univ_tvs/ex_tvs, but perhaps in a different order.
+             -- See Note [DataCon user type variable binders] in DataCon.
+             tkv_bndrs      = mkTyVarBinders Inferred  tkvs'
+             user_tv_bndrs  = mkTyVarBinders Specified user_tvs'
+             all_user_bndrs = tkv_bndrs ++ user_tv_bndrs
+
              ctxt'      = substTys arg_subst ctxt
              arg_tys'   = substTys arg_subst arg_tys
              res_ty'    = substTy  arg_subst res_ty
 
+
        ; fam_envs <- tcGetFamInstEnvs
 
        -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
@@ -1756,7 +1768,7 @@ tcConDecl rep_tycon tmpl_bndrs res_tmpl
              ; buildDataCon fam_envs name is_infix
                             rep_nm
                             stricts Nothing field_lbls
-                            univ_bndrs ex_bndrs eq_preds
+                            univ_tvs ex_tvs all_user_bndrs eq_preds
                             ctxt' arg_tys' res_ty' rep_tycon
                   -- NB:  we put data_tc, the type constructor gotten from the
                   --      constructor type signature into the data constructor;
@@ -1842,58 +1854,6 @@ tcConArg bty
         ; return (arg_ty, getBangStrictness bty) }
 
 {-
-Note [Wrong visibility for GADTs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-GADT tyvars shouldn't all be specified, but it's hard to do much better, as
-described in #11721, which is duplicated here for convenience:
-
-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 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.)
-
 Note [Infix GADT constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We do not currently have syntax to declare an infix constructor in GADT syntax,
@@ -1927,7 +1887,7 @@ defined yet.
 
 So, we want to make rejigConRes lazy and then check the validity of
 the return type in checkValidDataCon.  To do this we /always/ return a
-4-tuple from rejigConRes (so that we can compute the return type from it, which
+6-tuple from rejigConRes (so that we can compute the return type from it, which
 checkValidDataCon needs), but the first three fields may be bogus if
 the return type isn't valid (the last equation for rejigConRes).
 
@@ -1945,19 +1905,26 @@ errors reported in one pass.  See Trac #7175, and #10836.
 -- In this case orig_res_ty = T (e,e)
 
 rejigConRes :: [TyConBinder] -> Type    -- Template for result type; e.g.
-                                  -- data instance T [a] b c = ...
+                                  -- data instance T [a] b c ...
                                   --      gives template ([a,b,c], T [a] b c)
                                   -- Type must be of kind *!
-            -> [TyVar]            -- where MkT :: forall x y z. ...
+            -> [TyVar]            -- The constructor's user-written, inferred
+                                  -- type variables
+            -> [TyVar]            -- The constructor's user-written, specified
+                                  -- type variables
             -> Type               -- res_ty type must be of kind *
             -> ([TyVar],          -- Universal
                 [TyVar],          -- Existential (distinct OccNames from univs)
+                [TyVar],          -- The constructor's rejigged, user-written,
+                                  -- inferred type variables
+                [TyVar],          -- The constructor's rejigged, user-written,
+                                  -- specified type variables
                 [EqSpec],      -- Equality predicates
                 TCvSubst)      -- Substitution to apply to argument types
         -- We don't check that the TyCon given in the ResTy is
         -- the same as the parent tycon, because checkValidDataCon will do it
 
-rejigConRes tmpl_bndrs res_tmpl dc_tvs res_ty
+rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
         -- E.g.  data T [a] b c where
         --         MkT :: forall x y z. T [(x,y)] z z
         -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
@@ -1968,7 +1935,12 @@ rejigConRes tmpl_bndrs res_tmpl dc_tvs res_ty
         --          b              b~z
         --          z
         -- Existentials are the leftover type vars: [x,y]
-        -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], <arg-subst>)
+        -- The user-written type variables are what is listed in the forall:
+        --   [x, y, z] (all specified). We must rejig these as well.
+        --   See Note [DataCon user type variable binders] in DataCon.
+        -- So we return ( [a,b,z], [x,y]
+        --              , [], [x,y,z]
+        --              , [a~(x,y),b~z], <arg-subst> )
   | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
                   ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
                   tcMatchTy res_tmpl res_ty
@@ -1977,9 +1949,19 @@ rejigConRes tmpl_bndrs res_tmpl dc_tvs res_ty
         (arg_subst, substed_ex_tvs)
           = mapAccumL substTyVarBndr kind_subst raw_ex_tvs
 
+        -- After rejigging the existential tyvars, the resulting substitution
+        -- gives us exactly what we need to rejig the user-written tyvars,
+        -- since the dcUserTyVarBinders invariant guarantees that the
+        -- substitution has *all* the tyvars in its domain.
+        -- See Note [DataCon user type variable binders] in DataCon.
+        subst_user_tvs = map (getTyVar "rejigConRes" . substTyVar arg_subst)
+        substed_inferred_tvs  = subst_user_tvs dc_inferred_tvs
+        substed_specified_tvs = subst_user_tvs dc_specified_tvs
+
         substed_eqs = map (substEqSpec arg_subst) raw_eqs
     in
-    (univ_tvs, substed_ex_tvs, substed_eqs, arg_subst)
+    (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs,
+     substed_eqs, arg_subst)
 
   | otherwise
         -- If the return type of the data constructor doesn't match the parent
@@ -1992,8 +1974,10 @@ rejigConRes tmpl_bndrs res_tmpl dc_tvs res_ty
         -- albeit bogus, relying on checkValidDataCon to check the
         --  bad-result-type error before seeing that the other fields look odd
         -- See Note [Checking GADT return types]
-  = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, [], emptyTCvSubst)
+  = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_inferred_tvs, dc_specified_tvs,
+     [], emptyTCvSubst)
   where
+    dc_tvs   = dc_inferred_tvs ++ dc_specified_tvs
     tmpl_tvs = binderVars tmpl_bndrs
 
 {- Note [mkGADTVars]
@@ -3231,12 +3215,11 @@ badDataConTyCon data_con res_ty_tmpl actual_res_ty
     --    underneath the nested foralls and contexts.
     -- 3) Smash together the type variables and class predicates from 1) and
     --    2), and prepend them to the rho type from 2).
-    actual_ex_tvs = dataConExTyVarBinders data_con
+    actual_ex_tvs = dataConExTyVars data_con
     actual_theta  = dataConTheta data_con
     (actual_res_tvs, actual_res_theta, actual_res_rho)
       = tcSplitNestedSigmaTys actual_res_ty
-    actual_res_tvbs = mkTyVarBinders Specified actual_res_tvs
-    suggested_ty = mkForAllTys (actual_ex_tvs ++ actual_res_tvbs) $
+    suggested_ty = mkSpecForAllTys (actual_ex_tvs ++ actual_res_tvs) $
                    mkFunTys (actual_theta ++ actual_res_theta)
                    actual_res_rho
 
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 1174b20b1d..07470e65c6 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -138,8 +138,8 @@ module TyCoRep (
 import GhcPrelude
 
 import {-# SOURCE #-} DataCon( dataConFullSig
-                             , dataConUnivTyVarBinders, dataConExTyVarBinders
-                             , DataCon, filterEqSpec )
+                             , dataConUserTyVarBinders
+                             , DataCon )
 import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
                           , tyCoVarsOfTypeWellScoped
                           , tyCoVarsOfTypesWellScoped
@@ -2651,12 +2651,11 @@ pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons
 pprDataConWithArgs :: DataCon -> SDoc
 pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc]
   where
-    (_univ_tvs, _ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc
-    univ_bndrs = dataConUnivTyVarBinders dc
-    ex_bndrs   = dataConExTyVarBinders dc
-    forAllDoc = pprUserForAll $ (filterEqSpec eq_spec univ_bndrs ++ ex_bndrs)
-    thetaDoc  = pprThetaArrowTy theta
-    argsDoc   = hsep (fmap pprParendType arg_tys)
+    (_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc
+    user_bndrs = dataConUserTyVarBinders dc
+    forAllDoc  = pprUserForAll user_bndrs
+    thetaDoc   = pprThetaArrowTy theta
+    argsDoc    = hsep (fmap pprParendType arg_tys)
 
 
 pprTypeApp :: TyCon -> [Type] -> SDoc
diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs
index c0a7e1cc5a..4862ce204b 100644
--- a/compiler/vectorise/Vectorise/Generic/PData.hs
+++ b/compiler/vectorise/Vectorise/Generic/PData.hs
@@ -78,14 +78,16 @@ buildPDataDataCon orig_name vect_tc repr_tc repr
       comp_tys  <- mkSumTys repr_sel_ty mkPDataType repr
       fam_envs  <- readGEnv global_fam_inst_env
       rep_nm    <- liftDs $ newTyConRepName dc_name
+      let univ_tvbs = mkTyVarBinders Specified tvs
       liftDs $ buildDataCon fam_envs dc_name
                             False                  -- not infix
                             rep_nm
                             (map (const no_bang) comp_tys)
                             (Just $ map (const HsLazy) comp_tys)
                             []                     -- no field labels
-                            (mkTyVarBinders Specified tvs)
+                            tvs
                             []                     -- no existentials
+                            univ_tvbs
                             []                     -- no eq spec
                             []                     -- no context
                             comp_tys
@@ -122,14 +124,16 @@ buildPDatasDataCon orig_name vect_tc repr_tc repr
       comp_tys  <- mkSumTys repr_sels_ty mkPDatasType repr
       fam_envs <- readGEnv global_fam_inst_env
       rep_nm   <- liftDs $ newTyConRepName dc_name
+      let univ_tvbs = mkTyVarBinders Specified tvs
       liftDs $ buildDataCon fam_envs dc_name
                             False                  -- not infix
                             rep_nm
                             (map (const no_bang) comp_tys)
                             (Just $ map (const HsLazy) comp_tys)
                             []                     -- no field labels
-                            (mkTyVarBinders Specified tvs)
+                            tvs
                             []                     -- no existentials
+                            univ_tvbs
                             []                     -- no eq spec
                             []                     -- no context
                             comp_tys
diff --git a/compiler/vectorise/Vectorise/Type/TyConDecl.hs b/compiler/vectorise/Vectorise/Type/TyConDecl.hs
index 0828250363..75025501db 100644
--- a/compiler/vectorise/Vectorise/Type/TyConDecl.hs
+++ b/compiler/vectorise/Vectorise/Type/TyConDecl.hs
@@ -200,8 +200,9 @@ vectDataCon dc
                     (dataConSrcBangs dc)           -- strictness as original constructor
                     (Just $ dataConImplBangs dc)
                     []                             -- no labelled fields for now
-                    univ_bndrs                     -- universally quantified vars
+                    univ_tvs                       -- universally quantified vars
                     []                             -- no existential tvs for now
+                    user_bndrs
                     []                             -- no equalities for now
                     []                             -- no context for now
                     arg_tys                        -- argument types
@@ -213,4 +214,4 @@ vectDataCon dc
     rep_arg_tys = dataConRepArgTys dc
     tycon       = dataConTyCon dc
     (univ_tvs, ex_tvs, eq_spec, theta, _arg_tys, _res_ty) = dataConFullSig dc
-    univ_bndrs  = dataConUnivTyVarBinders dc
+    user_bndrs  = dataConUserTyVarBinders dc
diff --git a/docs/users_guide/8.4.1-notes.rst b/docs/users_guide/8.4.1-notes.rst
index c9100d4d1e..dc762602e2 100644
--- a/docs/users_guide/8.4.1-notes.rst
+++ b/docs/users_guide/8.4.1-notes.rst
@@ -77,6 +77,17 @@ Language
         GInt   :: G Int
         GMaybe :: G Maybe
 
+- The order in which type variables are quantified in GADT constructor type
+  signatures has changed. Before, if you had ``MkT`` as below: ::
+
+      data T a where
+        MkT :: forall b a. b -> T a
+
+  Then the type of ``MkT`` would (counterintuitively) be
+  ``forall a b. b -> T a``! Now, GHC quantifies the type variables in the
+  order that the users writes them, so the type of ``MkT`` is now
+  ``forall b a. b -> T a`` (this matters for :ghc-flag:`-XTypeApplications`).
+
 Compiler
 ~~~~~~~~
 
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, [''])