[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