[Git][ghc/ghc][wip/T18891] Fix kind inference for data types. Again.

Simon Peyton Jones gitlab at gitlab.haskell.org
Wed Nov 25 17:38:58 UTC 2020



Simon Peyton Jones pushed to branch wip/T18891 at Glasgow Haskell Compiler / GHC


Commits:
4bdd70d9 by Simon Peyton Jones at 2020-11-25T17:38:08+00:00
Fix kind inference for data types. Again.

This patch improves kcConDecls, when we are inferring the kind
of a data type decl.

Specifically

* In kcConDecls/kcConDecl make it clear that the tc_res_kind argument
  is only used in the H98 case; and in that case there is not result
  kind signature; and hence no need for the disgusting splitPiTys in
  kcConDecls (now thankfully gone).

  The GADT case is a bit different to before, and much nicer.
  This is what fixes #18891.

  See Note [kcConDecls: kind-checking data type decls]

* Do not look at the constructor decls of a data/newtype instance
  in tcDataFamInstanceHeader. See new
  Note [Kind inference for data family instances]

  This causes a few knock-on effects in the tests suite, because
  we require more information than before in the instance /header/.

  New user-manual material about this in "Kind inference in data type
  declarations" and "Kind inference for data/newtype instance
  declarations".

* Minor improvement in kcTyClDecl, combining GADT and H98 case.

Fixes #18891

- - - - -


22 changed files:

- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- docs/users_guide/9.2.1-notes.rst
- docs/users_guide/exts/poly_kinds.rst
- testsuite/tests/dependent/should_fail/T13780a.stderr
- testsuite/tests/deriving/should_compile/T11416.hs
- testsuite/tests/deriving/should_compile/T9359.hs
- testsuite/tests/patsyn/should_fail/T15685.stderr
- testsuite/tests/polykinds/T13659.stderr
- testsuite/tests/polykinds/T16221a.stderr
- testsuite/tests/th/T9692.hs
- + testsuite/tests/typecheck/should_compile/T18891.hs
- testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
- testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
- testsuite/tests/typecheck/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/T18891a.hs
- + testsuite/tests/typecheck/should_fail/T18891a.stderr
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
- + testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
- + testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2981,7 +2981,7 @@ bindOuterSigTKBndrs_Tv_M :: TcTyMode
                          -> TcM a -> TcM (HsOuterSigTyVarBndrs GhcTc, a)
 -- Do not push level; do not make implication constraint; use Tvs
 -- Two major clients of this "bind-only" path are:
---    Note [Kind-checking for GADTs] in TyCl
+--    Note [Using TyVarTvs for kind-checking GADTs] in GHC.Tc.TyCl
 --    Note [Checking partial type signatures]
 bindOuterSigTKBndrs_Tv_M mode
   = bindOuterTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True
@@ -3294,8 +3294,8 @@ When we /must/ clone.
   When kind-checking T, we give (a :: kappa1). Then:
 
   - In kcConDecl we make a TyVarTv unification variable kappa2 for k2
-    (as described in Note [Kind-checking for GADTs], even though this
-    example is an existential)
+    (as described in Note [Using TyVarTvs for kind-checking GADTs],
+    even though this example is an existential)
   - So we get (b :: kappa2) via bindExplicitTKBndrs_Tv
   - We end up unifying kappa1 := kappa2, because of the (SameKind a b)
 


=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -1529,27 +1529,16 @@ kcTyClDecl :: TyClDecl GhcRn -> TcTyCon -> TcM ()
 --    result kind signature have already been dealt with
 --    by inferInitialKind, so we can ignore them here.
 
-kcTyClDecl (DataDecl { tcdLName    = (L _ name)
-                     , tcdDataDefn = defn }) tyCon
-  | HsDataDefn { dd_cons = cons@((L _ (ConDeclGADT {})) : _)
-               , dd_ctxt = (L _ [])
-               , dd_ND = new_or_data } <- defn
-  = -- See Note [Implementation of UnliftedNewtypes] STEP 2
-    kcConDecls new_or_data (tyConResKind tyCon) cons
-
-    -- hs_tvs and dd_kindSig already dealt with in inferInitialKind
-    -- This must be a GADT-style decl,
-    --        (see invariants of DataDefn declaration)
-    -- so (a) we don't need to bring the hs_tvs into scope, because the
-    --        ConDecls bind all their own variables
-    --    (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
-
-  | HsDataDefn { dd_ctxt = ctxt
-               , dd_cons = cons
-               , dd_ND = new_or_data } <- defn
+kcTyClDecl (DataDecl { tcdLName    = (L _ name), tcdDataDefn = defn }) tycon
+  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_ND = new_or_data } <- defn
   = bindTyClTyVars name $ \ _ _ _ ->
-    do { _ <- tcHsContext ctxt
-       ; kcConDecls new_or_data (tyConResKind tyCon) cons
+       -- NB: binding these tyvars isn't necessary for GADTs, but it does no
+       -- harm.  For GADTs, each data con brings its own tyvars into scope,
+       -- and the ones from this bindTyClTyVars are either not mentioned or
+       -- (conceivably) shadowed.
+    do { traceTc "kcTyClDecl" (ppr tycon $$ ppr (tyConTyVars tycon) $$ ppr (tyConResKind tycon))
+       ; _ <- tcHsContext ctxt
+       ; kcConDecls new_or_data (tyConResKind tycon) cons
        }
 
 kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs }) _tycon
@@ -1606,13 +1595,12 @@ kcConGADTArgs new_or_data res_kind con_args = case con_args of
 
 kcConDecls :: NewOrData
            -> Kind             -- The result kind signature
+                               --   Used only in H98 case
            -> [LConDecl GhcRn] -- The data constructors
            -> TcM ()
-kcConDecls new_or_data res_kind cons
-  = mapM_ (wrapLocM_ (kcConDecl new_or_data final_res_kind)) cons
-  where
-    (_, final_res_kind) = splitPiTys res_kind
-        -- See Note [kcConDecls result kind]
+-- See Note [kcConDecls: kind-checking data type decls]
+kcConDecls new_or_data tc_res_kind cons
+  = mapM_ (wrapLocM_ (kcConDecl new_or_data tc_res_kind)) cons
 
 -- Kind check a data constructor. In additional to the data constructor,
 -- we also need to know about whether or not its corresponding type was
@@ -1623,82 +1611,69 @@ kcConDecl :: NewOrData
           -> Kind  -- Result kind of the type constructor
                    -- Usually Type but can be TYPE UnliftedRep
                    -- or even TYPE r, in the case of unlifted newtype
+                   -- Used only in H98 case
           -> ConDecl GhcRn
           -> TcM ()
-kcConDecl new_or_data res_kind (ConDeclH98
+kcConDecl new_or_data tc_res_kind (ConDeclH98
   { con_name = name, con_ex_tvs = ex_tvs
   , con_mb_cxt = ex_ctxt, con_args = args })
   = addErrCtxt (dataConCtxtName [name]) $
     discardResult                   $
     bindExplicitTKBndrs_Tv ex_tvs $
     do { _ <- tcHsMbContext ex_ctxt
-       ; kcConH98Args new_or_data res_kind args
+       ; kcConH98Args new_or_data tc_res_kind args
          -- We don't need to check the telescope here,
          -- because that's done in tcConDecl
        }
 
-kcConDecl new_or_data res_kind (ConDeclGADT
+kcConDecl new_or_data
+          _tc_res_kind   -- Not used in GADT case (and doesn't make sense)
+          (ConDeclGADT
     { con_names = names, con_bndrs = L _ outer_bndrs, con_mb_cxt = cxt
     , con_g_args = args, con_res_ty = res_ty })
-  = -- Even though the GADT-style data constructor's type is closed,
-    -- we must still kind-check the type, because that may influence
-    -- the inferred kind of the /type/ constructor.  Example:
-    --    data T f a where
-    --      MkT :: f a -> T f a
-    -- If we don't look at MkT we won't get the correct kind
-    -- for the type constructor T
+  = -- See Note [kcConDecls: kind-checking data type decls]
     addErrCtxt (dataConCtxtName names) $
     discardResult                      $
     bindOuterSigTKBndrs_Tv outer_bndrs $
-        -- Why "_Tv"?  See Note [Kind-checking for GADTs]
+        -- Why "_Tv"?  See Note [Using TyVarTvs for kind-checking GADTs]
     do { _ <- tcHsMbContext cxt
-       ; kcConGADTArgs new_or_data res_kind args
-       ; _ <- tcHsOpenType res_ty
+       ; traceTc "kcConDecl:GADT {" (ppr names $$ ppr res_ty)
+       ; con_res_kind <- newOpenTypeKind
+       ; _ <- tcCheckLHsType res_ty (TheKind con_res_kind)
+       ; kcConGADTArgs new_or_data con_res_kind args
+       ; traceTc "kcConDecl:GADT }" (ppr names $$ ppr con_res_kind)
        ; return () }
 
-{- Note [kcConDecls result kind]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We might have e.g.
-    data T a :: Type -> Type where ...
-or
-    newtype instance N a :: Type -> Type  where ..
-in which case, the 'res_kind' passed to kcConDecls will be
-   Type->Type
-
-We must look past those arrows, or even foralls, to the Type in the
-corner, to pass to kcConDecl c.f. #16828. Hence the splitPiTys here.
-
-I am a bit concerned about tycons with a declaration like
-   data T a :: Type -> forall k. k -> Type  where ...
-
-It does not have a CUSK, so kcInferDeclHeader will make a TcTyCon
-with tyConResKind of Type -> forall k. k -> Type.  Even that is fine:
-the splitPiTys will look past the forall.  But I'm bothered about
-what if the type "in the corner" mentions k?  This is incredibly
-obscure but something like this could be bad:
-   data T a :: Type -> foral k. k -> TYPE (F k) where ...
-
-I bet we are not quite right here, but my brain suffered a buffer
-overflow and I thought it best to nail the common cases right now.
-
-Note [Recursion and promoting data constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We don't want to allow promotion in a strongly connected component
-when kind checking.
-
-Consider:
-  data T f = K (f (K Any))
-
-When kind checking the `data T' declaration the local env contains the
-mappings:
-  T -> ATcTyCon <some initial kind>
-  K -> APromotionErr
-
-APromotionErr is only used for DataCons, and only used during type checking
-in tcTyClGroup.
-
-Note [Kind-checking for GADTs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [kcConDecls: kind-checking data type decls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+kcConDecls is used when we are inferring the kind of the type
+constructor in a data type declaration.  E.g.
+    data T f a = MkT (f a)
+we want to infer the kind of 'f' and 'a'. The basic plan is described
+in Note [Inferring kinds for type declarations]; here are doing Step 2.
+
+In the H98 case, for unlifted newtypes only, we need the result kind of
+the TyCon, to unify with the argument kind.  The tycon's result kind
+is not used at all in the GADT case.
+
+In the GADT case we may have this:
+   data T f a where
+      MkT :: forall g b. g b -> T g b
+Notice that the variables f,a, and g,b are quite distinct.
+Nevertheless, this decl must still influence the kind T (which is,
+remember Step 1, something like T :: kappa1 -> kappa2 -> Type), otherwise
+we'd infer the bogus kind T :: forall k1 k2. k1 -> k2 -> Type.
+
+The data constructor type influences the kind of T simply by
+kind-checking the result type (T g b), which will force 'f' and 'g' to
+have the same kinds. This is the call to
+    tcCheckLHsType res_ty (TheKind con_res_kind)
+Because this is the result type of an arrow, we know the kind must be
+of form (TYPE rr), and we get better error messages if we enforce that
+here (e.g. test gadt10).
+
+Note [Using TyVarTvs for kind-checking GADTs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
   data Proxy a where
@@ -1708,26 +1683,27 @@ Consider
 It seems reasonable that this should be accepted. But something very strange
 is going on here: when we're kind-checking this declaration, we need to unify
 the kind of `a` with k and j -- even though k and j's scopes are local to the type of
-MkProxy{1,2}. The best approach we've come up with is to use TyVarTvs during
-the kind-checking pass. First off, note that it's OK if the kind-checking pass
-is too permissive: we'll snag the problems in the type-checking pass later.
-(This extra permissiveness might happen with something like
+MkProxy{1,2}.
+
+In effect, we are simply gathering constraints on the shape of Proxy's
+kind, with no skolemisation or implication constraints involved at all.
+
+The best approach we've come up with is to use TyVarTvs during the
+kind-checking pass, rather than ordinary skolems. This is why we use
+the "_Tv" variant, bindOuterSigTKBndrs_Tv.
+
+Our only goal is to gather constraints on the kind of the type constructor;
+we do not certify that the data declaration is well-kinded. For example:
 
   data SameKind :: k -> k -> Type
   data Bad a where
     MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
 
-which would be accepted if k1 and k2 were TyVarTvs. This is correctly rejected
-in the second pass, though. Test case: polykinds/TyVarTvKinds3)
-Recall that the kind-checking pass exists solely to collect constraints
-on the kinds and to power unification.
-
-To achieve the use of TyVarTvs, we must be careful to use specialized functions
-that produce TyVarTvs, not ordinary skolems. This is why we need
-kcExplicitTKBndrs and kcImplicitTKBndrs in GHC.Tc.Gen.HsType, separate from their
-tc... variants.
+which would be accepted by kcConDecl because k1 and k2 are
+TyVarTvs. It is correctly rejected in the second pass, tcConDecl.
+(Test case: polykinds/TyVarTvKinds3)
 
-The drawback of this approach is sometimes it will accept a definition that
+One drawback of this approach is sometimes it will accept a definition that
 a (hypothetical) declarative specification would likely reject. As a general
 rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
 the whole point of CUSKs is to allow polymorphic recursion. Yet, the TyVarTvs
@@ -1746,6 +1722,23 @@ be rejected (without a CUSK). However, the accepted definitions are indeed
 well-kinded and any rejected definitions would be accepted with a CUSK,
 and so this wrinkle need not cause anyone to lose sleep.
 
+Note [Recursion and promoting data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don't want to allow promotion in a strongly connected component
+when kind checking.
+
+Consider:
+  data T f = K (f (K Any))
+
+When kind checking the `data T' declaration the local env contains the
+mappings:
+  T -> ATcTyCon <some initial kind>
+  K -> APromotionErr
+
+APromotionErr is only used for DataCons, and only used during type checking
+in tcTyClGroup.
+
+
 ************************************************************************
 *                                                                      *
 \subsection{Type checking}
@@ -3214,7 +3207,7 @@ tcConDecl :: KnotTied TyCon          -- Representation tycon. Knot-tied!
           -> ConDecl GhcRn
           -> TcM [DataCon]
 
-tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
+tcConDecl rep_tycon tag_map tc_bndrs res_kind res_tmpl new_or_data
           (ConDeclH98 { con_name = lname@(L _ name)
                       , con_ex_tvs = explicit_tkv_nms
                       , con_mb_cxt = hs_ctxt
@@ -3224,7 +3217,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
 
          -- Get hold of the existential type variables
          -- e.g. data T a = forall k (b::k) f. MkT a (f b)
-         -- Here tmpl_bndrs = {a}
+         -- Here tc_bndrs = {a}
          --      hs_qvars = HsQTvs { hsq_implicit = {k}
          --                        , hsq_explicit = {f,b} }
 
@@ -3242,29 +3235,35 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
                  }
 
 
-       ; let tmpl_tvs = binderVars tmpl_bndrs
-       ; let fake_ty  = mkSpecForAllTys tmpl_tvs $
+       ; let tc_tvs   = binderVars tc_bndrs
+             fake_ty  = mkSpecForAllTys  tc_tvs      $
                         mkInvisForAllTys exp_tvbndrs $
                         mkPhiTy ctxt $
                         mkVisFunTys arg_tys $
                         unitTy
              -- That type is a lie, of course. (It shouldn't end in ()!)
              -- And we could construct a proper result type from the info
-             -- at hand. But the result would mention only the tmpl_tvs,
+             -- at hand. But the result would mention only the univ_tvs,
              -- and so it just creates more work to do it right. Really,
              -- we're only doing this to find the right kind variables to
              -- quantify over, and this type is fine for that purpose.
 
-         -- exp_tvs have explicit, user-written binding sites
+         -- exp_tvbndrs have explicit, user-written binding sites
          -- the kvs below are those kind variables entirely unmentioned by the user
          --   and discovered only by generalization
 
        ; kvs <- kindGeneralizeAll fake_ty
 
-       ; let skol_tvs = kvs ++ tmpl_tvs
+       ; let skol_tvs = tc_tvs ++ kvs ++ binderVars exp_tvbndrs
        ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
-
-             -- Zonk to Types
+             -- The skol_info claims that all the variables are bound
+             -- by the data constructor decl, whereas actually the
+             -- univ_tvs are bound by the data type decl itself.  It
+             -- would be better to have a doubly-nested implication.
+             -- But that just doesn't seem worth it.
+             -- See test dependent/should_fail/T13780a
+
+       -- Zonk to Types
        ; (ze, qkvs)          <- zonkTyBndrs kvs
        ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
        ; arg_tys             <- zonkScaledTcTypesToTypesX ze arg_tys
@@ -3272,15 +3271,13 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
 
        -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
        ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
-       ; let
-           univ_tvbs = tyConInvisTVBinders tmpl_bndrs
-           univ_tvs  = binderVars univ_tvbs
-           ex_tvbs   = mkTyVarBinders InferredSpec qkvs ++ user_qtvbndrs
-           ex_tvs    = binderVars ex_tvbs
-           -- For H98 datatypes, the user-written tyvar binders are precisely
-           -- the universals followed by the existentials.
-           -- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
-           user_tvbs = univ_tvbs ++ ex_tvbs
+       ; let univ_tvbs = tyConInvisTVBinders tc_bndrs
+             ex_tvbs   = mkTyVarBinders InferredSpec qkvs ++ user_qtvbndrs
+             ex_tvs    = binderVars ex_tvbs
+                -- For H98 datatypes, the user-written tyvar binders are precisely
+                -- the universals followed by the existentials.
+                -- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
+             user_tvbs = univ_tvbs ++ ex_tvbs
 
        ; traceTc "tcConDecl 2" (ppr name)
        ; is_infix <- tcConIsInfixH98 name hs_args
@@ -3288,7 +3285,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
        ; fam_envs <- tcGetFamInstEnvs
        ; dc <- buildDataCon fam_envs name is_infix rep_nm
                             stricts Nothing field_lbls
-                            univ_tvs ex_tvs user_tvbs
+                            tc_tvs ex_tvs user_tvbs
                             [{- no eq_preds -}] ctxt arg_tys
                             res_tmpl rep_tycon tag_map
                   -- NB:  we put data_tc, the type constructor gotten from the
@@ -3299,7 +3296,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
   where
     skol_info = DataConSkol name
 
-tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
+tcConDecl rep_tycon tag_map tc_bndrs _res_kind res_tmpl new_or_data
   -- NB: don't use res_kind here, as it's ill-scoped. Instead,
   -- we get the res_kind by typechecking the result type.
           (ConDeclGADT { con_names = names
@@ -3344,7 +3341,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
        ; res_ty        <- zonkTcTypeToTypeX   ze res_ty
 
        ; let (univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
-               = rejigConRes tmpl_bndrs res_tmpl tvbndrs res_ty
+               = rejigConRes tc_bndrs res_tmpl tvbndrs res_ty
              -- See Note [Checking GADT return types]
 
              ctxt'      = substTys arg_subst ctxt
@@ -3532,9 +3529,9 @@ errors reported in one pass.  See #7175, and #10836.
 --      TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
 -- In this case orig_res_ty = T (e,e)
 
-rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type    -- Template for result type; e.g.
-                                  -- data instance T [a] b c ...
-                                  --      gives template ([a,b,c], T [a] b c)
+rejigConRes :: [KnotTied TyConBinder]  -- Template for result type; e.g.
+            -> KnotTied Type           -- data instance T [a] b c ...
+                                       --      gives template ([a,b,c], T [a] b c)
             -> [InvisTVBinder]    -- The constructor's type variables (both inferred and user-written)
             -> KnotTied Type      -- res_ty
             -> ([TyVar],          -- Universal
@@ -3546,10 +3543,10 @@ rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type    -- Template for result
         -- We don't check that the TyCon given in the ResTy is
         -- the same as the parent tycon, because checkValidDataCon will do it
 -- NB: All arguments may potentially be knot-tied
-rejigConRes tmpl_bndrs res_tmpl dc_tvbndrs res_ty
+rejigConRes tc_tvbndrs res_tmpl dc_tvbndrs 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
+        -- The {a,b,c} are the tc_tvs, and the {x,y,z} are the dc_tvs
         --     (NB: unlike the H98 case, the dc_tvs are not all existential)
         -- Then we generate
         --      Univ tyvars     Eq-spec
@@ -3564,7 +3561,7 @@ rejigConRes tmpl_bndrs res_tmpl dc_tvbndrs res_ty
         --              , [], [x,y,z]
         --              , [a~(x,y),b~z], <arg-subst> )
   | Just subst <- tcMatchTy res_tmpl res_ty
-  = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
+  = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tc_tvs dc_tvs subst
         raw_ex_tvs = dc_tvs `minusList` univ_tvs
         (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs
 
@@ -3591,10 +3588,10 @@ rejigConRes tmpl_bndrs res_tmpl dc_tvbndrs 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, dc_tvbndrs, [], emptyTCvSubst)
+  = (tc_tvs, dc_tvs `minusList` tc_tvs, dc_tvbndrs, [], emptyTCvSubst)
   where
-    dc_tvs   = binderVars dc_tvbndrs
-    tmpl_tvs = binderVars tmpl_bndrs
+    dc_tvs = binderVars dc_tvbndrs
+    tc_tvs = binderVars tc_tvbndrs
 
 {- Note [mkGADTVars]
 ~~~~~~~~~~~~~~~~~~~~


=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -688,9 +688,8 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
           -- Do /not/ check that the number of patterns = tyConArity fam_tc
           -- See [Arity of data families] in GHC.Core.FamInstEnv
        ; (qtvs, pats, res_kind, stupid_theta)
-             <- tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs
-                                    fixity hs_ctxt hs_pats m_ksig hs_cons
-                                    new_or_data
+             <- tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
+                                    hs_ctxt hs_pats m_ksig new_or_data
 
        -- Eta-reduce the axiom if possible
        -- Quite tricky: see Note [Implementing eta reduction for data families]
@@ -857,7 +856,7 @@ TyVarEnv will simply be empty, and there is nothing to worry about.
 tcDataFamInstHeader
     :: AssocInstInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
     -> LexicalFixity -> LHsContext GhcRn
-    -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn]
+    -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn)
     -> NewOrData
     -> TcM ([TyVar], [Type], Kind, ThetaType)
 -- The "header" of a data family instance is the part other than
@@ -865,7 +864,7 @@ tcDataFamInstHeader
 --    e.g.  data instance D [a] :: * -> * where ...
 -- Here the "header" is the bit before the "where"
 tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
-                    hs_ctxt hs_pats m_ksig hs_cons new_or_data
+                    hs_ctxt hs_pats m_ksig new_or_data
   = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
        ; (tclvl, wanted, (scoped_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
             <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
@@ -884,8 +883,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
                   -- Add constraints from the result signature
                   ; res_kind <- tc_kind_sig m_ksig
 
-                  -- Add constraints from the data constructors
-                  ; kcConDecls new_or_data res_kind hs_cons
+                  -- Do not add constraints from the data constructors
+                  -- See Note [Kind inference for data family instances]
 
                   -- Check that the result kind of the TyCon applied to its args
                   -- is compatible with the explicit signature (or Type, if there
@@ -1049,6 +1048,86 @@ however, so this Note aims to describe these subtleties:
   themselves.  Heavy sigh.  But not truly hard; that's what tcbVisibilities
   does.
 
+Note [Kind inference for data family instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this GADT-style data type declaration, where I have used
+fresh variables in the data constructor's type, to stress that c,d are
+quite distinct from a,b.
+   data T a b where
+     MkT :: forall c d. c d -> T c d
+
+Following Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
+to infer T's kind, we initially give T :: kappa, a monomorpic kind,
+gather constraints from the header and data constructors, and conclude
+   T :: (kappa1 -> type) -> kappa1 -> Type
+Then we generalise, giving
+   T :: forall k. (k->Type) -> k -> Type
+
+Now what about a data /instance/ decl
+   data family T :: forall k. (k->Type) -> k -> Type
+
+   data instance T p Int where ...
+
+No doubt here! The poly-kinded T is instantiated with k=Type, so the
+header really looks like
+   data instance T @Type (p :: Type->Type) Int where ...
+
+But what about this?
+   data instance T p q where
+      MkT :: forall r. r Int -> T r Int
+
+So what kind do 'p' and 'q' have?  No clues from the header, but from
+the data constructor we can clearly see that (r :: Type->Type).  Does
+that mean that the the /entire data instance/ is instantiated at Type,
+like this?
+   data instance T @Type (p :: Type->Type) (q :: Type) where
+      ...
+
+Not at all! This is a /GADT/-style decl, so the kind argument might
+be specialised in this particular data constructor, thus:
+   data instance T @k (p :: k->Type) (q :: k) where
+     MkT :: forall (r :: Type -> Type).
+            r Int -> T @Type r Int
+(and perhaps specialised differently in some other data
+constructor MkT2).
+
+The key difference in this case and 'data T' at the top of this Note
+is that we have no known kind for 'data T'. We thus forbid different
+specialisations of T in its constructors, in an attempt to avoid
+inferring polymorphic recursion. In data family T, however, there is
+no problem with polymorphic recursion: we already /fully know/ T's
+kind -- that came from the family declaration, and is not influenced
+by the data instances -- and hence we /can/ specialise T's kind
+differently in different GADT data constructors.
+
+SHORT SUMMARY: in a data instance decl, it's not clear whether kind
+constraints arising from the data constructors should be considered
+local to the (GADT) data /constructor/ or should apply to the entire
+data instance.
+
+DESIGN CHOICE: in data/newtype family instance declarations, we ignore
+the /data constructor/ declarations altogether, looking only at the
+data instance /header/.
+
+Observations:
+* This choice is simple to describe, as well as simple to implment.
+  For a data/newtype instance decl, the instance kinds are influenced
+  /only/ by the header.
+
+* We could treat Haskell-98 style data-instance decls differently, by
+  taking the data constructors into account, since there are no GADT
+  issues.  But we don't, for simplicity, and because it means you can
+  understand the data type instance by looking only at the header.
+
+* Newtypes can be declared in GADT syntax, but they can't do GADT-style
+  specialisation, so like Haskell-98 definitions we could take the
+  data constructors into account.  Again we don't, for the same reason.
+
+So for now at least, we keep the simplest choice. See #18891 and !4419
+for more discussion of this issue.
+
+Kind inference for data types (Xie et al) https://arxiv.org/abs/1911.06153
+takes a slightly different approach.
 -}
 
 


=====================================
docs/users_guide/9.2.1-notes.rst
=====================================
@@ -40,6 +40,12 @@ Compiler
 - GHCi's ``:kind!`` command now expands through type synonyms in addition to type
   families. See :ghci-cmd:`:kind`.
 
+- Kind inference for data/newtype instance declarations is sligtly
+  more restrictive than before.  See the user manual :ref:`kind-inference-data-family-instances`.
+  This is a breaking change, albeit
+  a fairly obscure one that corrects a specification bug.
+
+
 ``ghc-prim`` library
 ~~~~~~~~~~~~~~~~~~~~
 


=====================================
docs/users_guide/exts/poly_kinds.rst
=====================================
@@ -130,8 +130,45 @@ This rule has occasionally-surprising consequences (see
 The kind-polymorphism from the class declaration makes ``D1``
 kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F2``.
 
+Kind inference in type signatures
+---------------------------------
+
+When kind-checking a type, GHC considers only what is written in that
+type when figuring out how to generalise the type's kind.
+
+For example,
+consider these definitions (with :extension:`ScopedTypeVariables`): ::
+
+  data Proxy a    -- Proxy :: forall k. k -> Type
+  p :: forall a. Proxy a
+  p = Proxy :: Proxy (a :: Type)
+
+GHC reports an error, saying that the kind of ``a`` should be a kind variable
+``k``, not ``Type``. This is because, by looking at the type signature
+``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
+restricted to be ``Type``. The function definition is then rejected for being
+more specific than its type signature.
+
+.. _explicit-kind-quantification:
+
+Explicit kind quantification
+----------------------------
+
+Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification,
+as in these examples: ::
+
+  data Proxy :: forall k. k -> Type
+  f :: (forall k (a :: k). Proxy a -> ()) -> Int
+
+Note that the second example has a ``forall`` that binds both a kind ``k`` and
+a type variable ``a`` of kind ``k``. In general, there is no limit to how
+deeply nested this sort of dependency can work. However, the dependency must
+be well-scoped: ``forall (a :: k) k. ...`` is an error.
+
+
 .. _inferring-variable-order:
 
+
 Inferring the order of variables in a type/class declaration
 ------------------------------------------------------------
 
@@ -490,41 +527,91 @@ This also applies to GADT-style data instances: ::
       --   • In the data instance declaration for ‘T’
 
 
-Kind inference in closed type families
---------------------------------------
+Kind inference in data type declarations
+----------------------------------------
 
-Although all open type families are considered to have a complete
-user-supplied kind signature, we can relax this condition for closed
-type families, where we have equations on which to perform kind
-inference. GHC will infer kinds for the arguments and result types of a
-closed type family.
+Consider the declaration ::
 
-GHC supports *kind-indexed* type families, where the family matches both
-on the kind and type. GHC will *not* infer this behaviour without a
-complete user-supplied kind signature, as doing so would sometimes infer
-non-principal types. Indeed, we can see kind-indexing as a form
-of polymorphic recursion, where a type is used at a kind other than
-its most general in its own definition.
+  data T1 f a = MkT1 (f a)
+  data T2 f a where
+    MkT2 :: f a -> T f a
 
-For example: ::
+In both cases GHC looks at the data constructor declarations to
+give constraints on the kind of ``T``, yielding ::
 
-    type family F1 a where
-      F1 True  = False
-      F1 False = True
-      F1 x     = x
-    -- F1 fails to compile: kind-indexing is not inferred
+  T1, T2 :: forall k. (k -> Type) -> k -> Type
 
-    type family F2 (a :: k) where
-      F2 True  = False
-      F2 False = True
-      F2 x     = x
-    -- F2 fails to compile: no complete signature
+Consider the type ::
+
+  data G (a :: k) where
+    GInt    :: G Int
+    GMaybe  :: G Maybe
+
+This datatype ``G`` is GADT-like in both its kind and its type. Suppose you
+have ``g :: G a``, where ``a :: k``. Then pattern matching to discover that
+``g`` is in fact ``GMaybe`` tells you both that ``k ~ (Type -> Type)`` and
+``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds`
+be in effect, but pattern-matching on ``G`` requires no extension beyond
+:extension:`GADTs`. That this works is actually a straightforward extension
+of regular GADTs and a consequence of the fact that kinds and types are the
+same.
+
+Note that the datatype ``G`` is used at different kinds in its body, and
+therefore that kind-indexed GADTs use a form of polymorphic recursion.
+It is thus only possible to use this feature if you have provided a
+complete user-supplied kind signature (CUSK)
+for the datatype (:ref:`complete-kind-signatures`), or a standalone
+kind signature (:ref:`standalone-kind-signatures`);
+in the case of ``G`` we have a CUSK.
+If you wish to see the kind indexing explicitly, you can do so by enabling :ghc-flag:`-fprint-explicit-kinds` and querying ``G`` with GHCi's :ghci-cmd:`:info` command: ::
+
+  > :set -fprint-explicit-kinds
+  > :info G
+  type role G nominal nominal
+  type G :: forall k. k -> Type
+  data G @k a where
+    GInt   :: G @Type Int
+    GMaybe :: G @(Type -> Type) Maybe
+
+where you can see the GADT-like nature of the two constructors.
+
+.. _kind-inference-data-family-instances:
+
+Kind inference for data/newtype instance declarations
+-----------------------------------------------------
+
+Consider these declarations ::
+
+   data family T :: forall k. (k->Type) -> k -> Type
+
+   data instance T p q where
+      MkT :: forall r. r Int -> T r Int
+
+Here ``T`` has an invisible kind argument; and perhaps it is instantiated
+to ``Type`` in the instance, thus ::
+
+   data instance T @Type (p :: Type->Type) (q :: Type) where
+      MkT :: forall r. r Int -> T r Int
+
+Or perhaps we intended the specialisation to be in the GADT data
+constructor, thus ::
+
+   data instance T @k (p :: k->Type) (q :: k) where
+      MkT :: forall r. r Int -> T @Type r Int
+
+It gets more complicated if there are multiple constructors.  In
+general, there is no principled way to tell which type specialisation
+comes from the data instance, and which from the individual GADT data
+constructors.
+
+So GHC implements this rule: in data/newtype instance declararations
+(unlike ordinary data/newtype declarations) we do *not* look at the
+constructor declarations when inferring the shape of the instance
+header.  The principle is that *the instantiation of the data instance
+should be apparent from the header alone*.  This principle makes the
+program easier to understand, and avoids the swamp of complexity
+indicated above.
 
-    type family F3 (a :: k) :: k where
-      F3 True  = False
-      F3 False = True
-      F3 x     = x
-    -- OK
 
 Kind inference in class instance declarations
 ---------------------------------------------
@@ -555,43 +642,8 @@ infrastructure, and it's not clear the payoff is worth it. If you want
 to restrict ``b``\ 's kind in the instance above, just use a kind
 signature in the instance head.
 
-Kind inference in type signatures
----------------------------------
-
-When kind-checking a type, GHC considers only what is written in that
-type when figuring out how to generalise the type's kind.
-
-For example,
-consider these definitions (with :extension:`ScopedTypeVariables`): ::
-
-  data Proxy a    -- Proxy :: forall k. k -> Type
-  p :: forall a. Proxy a
-  p = Proxy :: Proxy (a :: Type)
-
-GHC reports an error, saying that the kind of ``a`` should be a kind variable
-``k``, not ``Type``. This is because, by looking at the type signature
-``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
-restricted to be ``Type``. The function definition is then rejected for being
-more specific than its type signature.
-
-.. _explicit-kind-quantification:
-
-Explicit kind quantification
-----------------------------
-
-Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification,
-as in these examples: ::
-
-  data Proxy :: forall k. k -> Type
-  f :: (forall k (a :: k). Proxy a -> ()) -> Int
-
-Note that the second example has a ``forall`` that binds both a kind ``k`` and
-a type variable ``a`` of kind ``k``. In general, there is no limit to how
-deeply nested this sort of dependency can work. However, the dependency must
-be well-scoped: ``forall (a :: k) k. ...`` is an error.
-
-Implicit quantification in type synonyms and type family instances
-------------------------------------------------------------------
+Kind inference in type synonyms and type family instances
+---------------------------------------------------------
 
 Consider the scoping rules for type synonyms and type family instances, such as
 these::
@@ -706,29 +758,44 @@ kinds. Consequently, visible dependent quantifiers are rejected in any context
 that is unambiguously the type of a term. They are also rejected in the types
 of data constructors.
 
-Kind-indexed GADTs
-------------------
+Kind inference in closed type families
+--------------------------------------
 
-Consider the type ::
+Although all open type families are considered to have a complete
+user-supplied kind signature (:ref:`complete-kind-signatures`),
+we can relax this condition for closed
+type families, where we have equations on which to perform kind
+inference. GHC will infer kinds for the arguments and result types of a
+closed type family.
 
-  data G (a :: k) where
-    GInt    :: G Int
-    GMaybe  :: G Maybe
+GHC supports *kind-indexed* type families, where the family matches both
+on the kind and type. GHC will *not* infer this behaviour without a
+complete user-supplied kind signature or standalone kind
+signature (see :ref:`standalone-kind-signatures`),
+because doing so would sometimes infer
+non-principal types. Indeed, we can see kind-indexing as a form
+of polymorphic recursion, where a type is used at a kind other than
+its most general in its own definition.
 
-This datatype ``G`` is GADT-like in both its kind and its type. Suppose you
-have ``g :: G a``, where ``a :: k``. Then pattern matching to discover that
-``g`` is in fact ``GMaybe`` tells you both that ``k ~ (Type -> Type)`` and
-``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds`
-be in effect, but pattern-matching on ``G`` requires no extension beyond
-:extension:`GADTs`. That this works is actually a straightforward extension
-of regular GADTs and a consequence of the fact that kinds and types are the
-same.
+For example: ::
 
-Note that the datatype ``G`` is used at different kinds in its body, and
-therefore that kind-indexed GADTs use a form of polymorphic recursion.
-It is thus only possible to use this feature if you have provided a
-complete user-supplied kind signature
-for the datatype (:ref:`complete-kind-signatures`).
+    type family F1 a where
+      F1 True  = False
+      F1 False = True
+      F1 x     = x
+    -- F1 fails to compile: kind-indexing is not inferred
+
+    type family F2 (a :: k) where
+      F2 True  = False
+      F2 False = True
+      F2 x     = x
+    -- F2 fails to compile: no complete signature
+
+    type family F3 (a :: k) :: k where
+      F3 True  = False
+      F3 False = True
+      F3 x     = x
+    -- OK
 
 Higher-rank kinds
 -----------------


=====================================
testsuite/tests/dependent/should_fail/T13780a.stderr
=====================================
@@ -3,7 +3,7 @@ T13780a.hs:9:40: error:
     • Couldn't match kind ‘a’ with ‘Bool’
       Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
       ‘a’ is a rigid type variable bound by
-        a family instance declaration
+        the data constructor ‘SMkFoo’
         at T13780a.hs:9:20-31
     • In the second argument of ‘(~)’, namely ‘MkFoo’
       In the definition of data constructor ‘SMkFoo’


=====================================
testsuite/tests/deriving/should_compile/T11416.hs
=====================================
@@ -12,9 +12,11 @@ newtype T f (a :: ConstantT Type f) = T (f a)
   deriving Functor
 
 data family TFam1 (f :: k1) (a :: k2)
-newtype instance TFam1 f (ConstantT a f) = TFam1 (f a)
+newtype instance TFam1 (f :: k -> Type) (ConstantT (a :: k) f)
+                 = TFam1 (f a)
   deriving Functor
 
 data family TFam2 (f :: k1) (a :: k2)
-newtype instance TFam2 f (a :: ConstantT Type f) = TFam2 (f a)
+newtype instance TFam2 (f :: Type -> Type) (a :: ConstantT Type f)
+                 = TFam2 (f a)
   deriving Functor


=====================================
testsuite/tests/deriving/should_compile/T9359.hs
=====================================
@@ -9,6 +9,5 @@ data Cmp a where
  deriving (Show, Eq)
 
 data family   CmpInterval (a :: Cmp k) (b :: Cmp k) :: Type
-data instance CmpInterval (V c)         Sup          = Starting c
+data instance CmpInterval (V (c :: Type)) Sup = Starting c
   deriving( Show )
-


=====================================
testsuite/tests/patsyn/should_fail/T15685.stderr
=====================================
@@ -1,13 +1,13 @@
 
 T15685.hs:13:24: error:
-    • Could not deduce: a ~ [k0]
-      from the context: as ~ (a1 : as1)
+    • Could not deduce: k ~ [k0]
+      from the context: as ~ (a : as1)
         bound by a pattern with constructor:
-                   Here :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]).
-                           f a2 -> NS f (a2 : as),
+                   Here :: forall {k} (f :: k -> *) (a :: k) (as :: [k]).
+                           f a -> NS f (a : as),
                  in a pattern synonym declaration
         at T15685.hs:13:19-26
-      ‘a’ is a rigid type variable bound by
+      ‘k’ is a rigid type variable bound by
         the inferred type of HereNil :: NS f as
         at T15685.hs:13:9-15
       Possible fix: add a type signature for ‘HereNil’


=====================================
testsuite/tests/polykinds/T13659.stderr
=====================================
@@ -1,6 +1,6 @@
 
-T13659.hs:14:27: error:
-    • Expected a type, but ‘a’ has kind ‘[*]’
-    • In the first argument of ‘Format’, namely ‘'[Int, a]’
-      In the type ‘Format '[Int, a]’
+T13659.hs:14:15: error:
+    • Expected kind ‘[*]’, but ‘a’ has kind ‘*’
+    • In the first argument of ‘Format’, namely ‘a’
+      In the type ‘Format a’
       In the definition of data constructor ‘I’


=====================================
testsuite/tests/polykinds/T16221a.stderr
=====================================
@@ -1,7 +1,7 @@
 
 T16221a.hs:6:49: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
-      ‘k1’ is a rigid type variable bound by
+    • Expected kind ‘k’, but ‘b’ has kind ‘k2’
+      ‘k2’ is a rigid type variable bound by
         an explicit forall k (b :: k)
         at T16221a.hs:6:20
       ‘k’ is a rigid type variable bound by


=====================================
testsuite/tests/th/T9692.hs
=====================================
@@ -12,7 +12,7 @@ class C a where
         data F a (b :: k) :: Type
 
 instance C Int where
-        data F Int x = FInt x
+        data F Int (x :: Type) = FInt x
 
 $( do info <- qReify (mkName "F")
       runIO $ putStrLn $ pprint info


=====================================
testsuite/tests/typecheck/should_compile/T18891.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs, UnliftedNewtypes, StandaloneKindSignatures, RankNTypes, TypeFamilies, PolyKinds #-}
+
+module T18891 where
+
+import GHC.Exts( TYPE )
+
+data family T2 (a :: k)
+data instance T2 a where
+  MkT2 :: T2 Maybe
+
+newtype N3 :: forall k -> TYPE k where
+  MkN3 :: N3 m -> N3 m
+
+type N4 :: forall k -> TYPE k
+newtype N4 :: forall k -> TYPE k where
+  MkN4 :: N4 m -> N4 m


=====================================
testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
=====================================
@@ -4,6 +4,8 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
 
 module UnliftedNewtypesUnassociatedFamily where
 
@@ -20,7 +22,16 @@ newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep])
 data instance DFT 'LiftedRep = MkDFT4 | MkDFT5
 
 data family DF :: TYPE (r :: RuntimeRep)
-newtype instance DF = MkDF1 Int#
-newtype instance DF = MkDF2 Word#
-newtype instance DF = MkDF3 (# Int#, Word# #)
+
+-- Use a type application
+newtype instance DF @IntRep = MkDF1 Int#
+
+-- Use a kind signature
+newtype instance DF :: TYPE 'WordRep where
+  MkDF2 :: Word# -> DF
+
+-- Also uses a kind signature
+newtype instance DF :: TYPE ('TupleRep '[ 'IntRep, 'WordRep ]) where
+  MkDF3 :: (# Int#, Word# #) -> DF
+
 data instance DF = MkDF4 | MkDF5


=====================================
testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
=====================================
@@ -10,14 +10,14 @@
 module UnliftedNewtypesUnassociatedFamily where
 
 import GHC.Int (Int(I#))
-import GHC.Exts (Int#,Word#,RuntimeRep(IntRep))
+import GHC.Exts (Int#,Word#,RuntimeRep(IntRep, WordRep))
 import GHC.Exts (TYPE)
 
 type KindOf (a :: TYPE k) = k
 
 data family D (a :: TYPE r) :: TYPE r
 
-newtype instance D a = MkWordD Word#
+newtype instance D (a :: TYPE 'WordRep) = MkWordD Word#
 
-newtype instance D a :: TYPE (KindOf a) where
-  MkIntD :: forall (a :: TYPE 'IntRep). Int# -> D a
+newtype instance D (a :: TYPE 'IntRep) :: TYPE (KindOf a) where
+  MkIntD :: forall (b :: TYPE 'IntRep). Int# -> D b


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -728,4 +728,5 @@ test('T18831', normal, compile, [''])
 test('T18920', normal, compile, [''])
 test('T15942', normal, compile, [''])
 test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
+test('T18891', normal, compile, [''])
 


=====================================
testsuite/tests/typecheck/should_fail/T18891a.hs
=====================================
@@ -0,0 +1,13 @@
+{-# LANGUAGE GADTs, UnliftedNewtypes, StandaloneKindSignatures, RankNTypes, TypeFamilies, PolyKinds #-}
+
+module T18891 where
+
+import GHC.Exts( TYPE )
+
+newtype N1 :: forall k. TYPE k where
+   MkN1 :: N1 -> N1
+
+type N2 :: forall k. TYPE k
+newtype N2 :: forall k. TYPE k where
+  MkN2 :: N2 -> N2
+


=====================================
testsuite/tests/typecheck/should_fail/T18891a.stderr
=====================================
@@ -0,0 +1,12 @@
+
+T18891a.hs:8:4: error:
+    • A newtype constructor must have a return type of form T a1 ... an
+      MkN1 :: N1 -> N1
+    • In the definition of data constructor ‘MkN1’
+      In the newtype declaration for ‘N1’
+
+T18891a.hs:12:3: error:
+    • A newtype constructor must have a return type of form T a1 ... an
+      MkN2 :: N2 -> N2
+    • In the definition of data constructor ‘MkN2’
+      In the newtype declaration for ‘N2’


=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
=====================================
@@ -1,11 +1,5 @@
-UnliftedNewtypesFamilyKindFail2.hs:12:20:
-     Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
-     In the first argument of ‘F’, namely ‘5’
-      In the newtype instance declaration for ‘F’
-
-UnliftedNewtypesFamilyKindFail2.hs:12:31:
-     Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
-     In the first argument of ‘F’, namely ‘5’
-      In the type ‘(F 5)’
-      In the definition of data constructor ‘MkF’
 
+UnliftedNewtypesFamilyKindFail2.hs:12:20: error:
+    • Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
+    • In the first argument of ‘F’, namely ‘5’
+      In the newtype instance declaration for ‘F’


=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE GADTs #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep))
+
+data family DF :: TYPE (r :: RuntimeRep)
+
+-- All these fail: see #18891 and !4419
+-- See Note [Kind inference for data family instances]
+-- in GHC.Tc.TyCl.Instance
+newtype instance DF = MkDF1a Int#
+newtype instance DF = MkDF2a Word#
+newtype instance DF = MkDF3a (# Int#, Word# #)


=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
=====================================
@@ -0,0 +1,18 @@
+
+UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error:
+    • Expecting a lifted type, but ‘Int#’ is unlifted
+    • In the type ‘Int#’
+      In the definition of data constructor ‘MkDF1a’
+      In the newtype instance declaration for ‘DF’
+
+UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error:
+    • Expecting a lifted type, but ‘Word#’ is unlifted
+    • In the type ‘Word#’
+      In the definition of data constructor ‘MkDF2a’
+      In the newtype instance declaration for ‘DF’
+
+UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error:
+    • Expecting a lifted type, but ‘(# Int#, Word# #)’ is unlifted
+    • In the type ‘(# Int#, Word# #)’
+      In the definition of data constructor ‘MkDF3a’
+      In the newtype instance declaration for ‘DF’


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -546,6 +546,7 @@ test('UnliftedNewtypesConstraintFamily', normal, compile_fail, [''])
 test('UnliftedNewtypesMismatchedKind', normal, compile_fail, [''])
 test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
 test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
+test('UnliftedNewtypesUnassociatedFamilyFail', normal, compile_fail, [''])
 test('T13834', normal, compile_fail, [''])
 test('T17077', normal, compile_fail, [''])
 test('T16512a', normal, compile_fail, [''])
@@ -589,3 +590,4 @@ test('T18640b', normal, compile_fail, [''])
 test('T18640c', normal, compile_fail, [''])
 test('T10709', normal, compile_fail, [''])
 test('T10709b', normal, compile_fail, [''])
+test('T18891a', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4bdd70d9ad7b4de288341e0797d314c1166dd2ce

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4bdd70d9ad7b4de288341e0797d314c1166dd2ce
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201125/a90b2588/attachment-0001.html>


More information about the ghc-commits mailing list