[Git][ghc/ghc][wip/T18891] Fix kind inference for data types. Again.
Simon Peyton Jones
gitlab at gitlab.haskell.org
Thu Dec 3 23:35:17 UTC 2020
Simon Peyton Jones pushed to branch wip/T18891 at Glasgow Haskell Compiler / GHC
Commits:
9f5d93df by Simon Peyton Jones at 2020-12-03T23:34:16+00:00
Fix kind inference for data types. Again.
This patch fixes several aspects of kind inference for data type
declarations, especially data /instance/ declarations
Specifically
1. 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 no 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]
2. Do not look at the constructor decls of a data/newtype instance
in tcDataFamInstanceHeader. See GHC.Tc.TyCl.Instance
Note [Kind inference for data family instances]. This was a
new realisation that arose when doing (1)
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".
3. Minor improvement in kcTyClDecl, combining GADT and H98 cases
4. Fix #14111 and #8707 by allowing the header of a data instance
to affect kind inferece for the the data constructor signatures;
as described at length in Note [GADT return types] in GHC.Tc.TyCl
This led to a modest refactoring of the arguments (and argument
order) of tcConDecl/tcConDecls.
5. Fix #19000 by inverting the sense of the test in new_locs
in GHC.Tc.Solver.Canonical.canDecomposableTyConAppOK.
Rather to my surprise, CI tells us that we get quite a few compile time
perf improvements in compiler bytes-allocated. Here are the ones that
reduced more than 1%. Good news! I have no idea why.
Test Metric value New value Change
---------------------------------------------------------------------------
ManyAlternatives(normal) ghc/alloc 803792416.0 800063504.0 -0.5%
Naperian(optasm) ghc/alloc 54311984.0 52874144.0 -2.6% GOOD
PmSeriesG(normal) ghc/alloc 57119912.0 53369856.0 -6.6%
PmSeriesS(normal) ghc/alloc 71507464.0 67756248.0 -5.2%
PmSeriesT(normal) ghc/alloc 104597416.0 100846208.0 -3.6%
PmSeriesV(normal) ghc/alloc 70326360.0 66576336.0 -5.3%
T10421(normal) ghc/alloc 132567776.0 128845672.0 -2.8% GOOD
T10421a(normal) ghc/alloc 94605104.0 90858592.0 -4.0%
T10547(normal) ghc/alloc 34996968.0 33557256.0 -4.1% GOOD
T10858(normal) ghc/alloc 212086488.0 208375832.0 -1.7%
T11195(normal) ghc/alloc 310033360.0 306391248.0 -1.2%
T11276(normal) ghc/alloc 145378016.0 141657896.0 -2.6%
T11303b(normal) ghc/alloc 55148504.0 51404904.0 -6.8%
T11374(normal) ghc/alloc 243783840.0 240133008.0 -1.5%
T11822(normal) ghc/alloc 154231136.0 150490720.0 -2.4%
T12150(optasm) ghc/alloc 94489040.0 90752656.0 -4.0% GOOD
T12234(optasm) ghc/alloc 69407208.0 65659624.0 -5.4% GOOD
T12425(optasm) ghc/alloc 115122960.0 111397664.0 -3.2% GOOD
T13035(normal) ghc/alloc 118754176.0 114795136.0 -3.3% GOOD
T13253-spj(normal) ghc/alloc 168969768.0 165225400.0 -2.2% GOOD
T15630(normal) ghc/alloc 201226672.0 197491904.0 -1.9%
T16190(normal) ghc/alloc 289119984.0 285560848.0 -1.2%
T17096(normal) ghc/alloc 326080472.0 322369512.0 -1.1%
T17836b(normal) ghc/alloc 69578304.0 65830328.0 -5.4%
T17977(normal) ghc/alloc 55833520.0 52094448.0 -6.7%
T17977b(normal) ghc/alloc 50731152.0 46983088.0 -7.4%
T18140(normal) ghc/alloc 120628376.0 116879552.0 -3.1% GOOD
T18282(normal) ghc/alloc 170207168.0 166491784.0 -2.2% GOOD
T18304(normal) ghc/alloc 107596576.0 103853360.0 -3.5% GOOD
T3064(normal) ghc/alloc 209696560.0 205954384.0 -1.8%
T4801(normal) ghc/alloc 376239392.0 372505256.0 -1.0%
T5030(normal) ghc/alloc 388667176.0 384947480.0 -1.0%
T5321FD(normal) ghc/alloc 332509600.0 328779208.0 -1.1%
T5321Fun(normal) ghc/alloc 379067288.0 375338056.0 -1.0%
T5837(normal) ghc/alloc 46272360.0 42540544.0 -8.1% GOOD
T6048(optasm) ghc/alloc 99200336.0 95462744.0 -3.8% GOOD
T9020(optasm) ghc/alloc 282057000.0 278339944.0 -1.3%
T9233(normal) ghc/alloc 967401992.0 963669872.0 -0.4%
Metric Decrease:
Naperian
T10421
T10547
T12150
T12234
T12425
T13035
T13253-spj
T18140
T18282
T18304
T5837
T6048
- - - - -
30 changed files:
- compiler/GHC/Hs/Extension.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver/Canonical.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/indexed-types/should_compile/T14111.hs
- + testsuite/tests/indexed-types/should_compile/T8707.hs
- testsuite/tests/indexed-types/should_compile/all.T
- testsuite/tests/indexed-types/should_fail/T8368.stderr
- testsuite/tests/indexed-types/should_fail/T8368a.stderr
- testsuite/tests/patsyn/should_fail/T15685.stderr
- testsuite/tests/polykinds/T13659.stderr
- testsuite/tests/polykinds/T16221a.stderr
- testsuite/tests/th/T11145.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/Hs/Extension.hs
=====================================
@@ -253,9 +253,9 @@ sure that any uses of it as a field are strict.
-- | Used as a data type index for the hsSyn AST; also serves
-- as a singleton type for Pass
data GhcPass (c :: Pass) where
- GhcPs :: GhcPs
- GhcRn :: GhcRn
- GhcTc :: GhcTc
+ GhcPs :: GhcPass 'Parsed
+ GhcRn :: GhcPass 'Renamed
+ GhcTc :: GhcPass 'Typechecked
-- This really should never be entered, but the data-deriving machinery
-- needs the instance to exist.
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2986,7 +2986,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
@@ -3299,8 +3299,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/Solver/Canonical.hs
=====================================
@@ -1885,7 +1885,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
| bndr <- tyConBinders tc
, let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
| otherwise = loc
- new_loc | isVisibleTyConBinder bndr
+ new_loc | isInvisibleTyConBinder bndr
= updateCtLocOrigin new_loc0 toInvisibleOrigin
| otherwise
= new_loc0 ]
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -17,7 +17,8 @@ module GHC.Tc.TyCl (
-- Functions used by GHC.Tc.TyCl.Instance to check
-- data/type family instance declarations
- kcConDecls, tcConDecls, dataDeclChecks, checkValidTyCon,
+ kcConDecls, tcConDecls, DataDeclInfo(..),
+ dataDeclChecks, checkValidTyCon,
tcFamTyPats, tcTyFamInstEqn,
tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
unravelFamInstPats, addConsistencyConstraints,
@@ -38,7 +39,7 @@ import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX
, reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env
-import GHC.Tc.Utils.Unify( emitResidualTvConstraint )
+import GHC.Tc.Utils.Unify( unifyType, emitResidualTvConstraint )
import GHC.Tc.Types.Constraint( emptyWC )
import GHC.Tc.Validity
import GHC.Tc.Utils.Zonk
@@ -130,7 +131,7 @@ Note [Check role annotations in a second pass]
Role inference potentially depends on the types of all of the datacons declared
in a mutually recursive group. The validity of a role annotation, in turn,
depends on the result of role inference. Because the types of datacons might
-be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
+be ill-formed (see #7175 and Note [rejigConRes]) we must check
*all* the tycons in a group for validity before checking *any* of the roles.
Thus, we take two passes over the resulting tycons, first checking for general
validity and then checking for valid role annotations.
@@ -1529,27 +1530,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 +1596,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 +1612,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]) $
+ = addErrCtxt (dataConCtxt [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
- addErrCtxt (dataConCtxtName names) $
+ = -- See Note [kcConDecls: kind-checking data type decls]
+ addErrCtxt (dataConCtxt 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 +1684,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.
+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)
-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.
-
-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 +1723,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}
@@ -2782,18 +2776,14 @@ tcDataDefn err_ctxt roles_info tc_name
; when (isJust mb_ksig) $
checkTc (kind_signatures) (badSigTyDecl tc_name)
- ; tycon <- fixM $ \ tycon -> do
+ ; tycon <- fixM $ \ rec_tycon -> do
{ let final_bndrs = tycon_binders `chkAppend` extra_bndrs
- res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
roles = roles_info tc_name
; data_cons <- tcConDecls
- tycon
- new_or_data
- final_bndrs
- final_res_kind
- res_ty
+ new_or_data DDVanilla
+ rec_tycon final_bndrs final_res_kind
cons
- ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons
+ ; tc_rhs <- mk_tc_rhs hsc_src rec_tycon data_cons
; tc_rep_nm <- newTyConRepName tc_name
; return (mkAlgTyCon tc_name
final_bndrs
@@ -3195,36 +3185,51 @@ consUseGadtSyntax _ = False
-- All constructors have same shape
-----------------------------------
-tcConDecls :: KnotTied TyCon -> NewOrData
- -> [TyConBinder] -> TcKind -- binders and result kind of tycon
- -> KnotTied Type -> [LConDecl GhcRn] -> TcM [DataCon]
-tcConDecls rep_tycon new_or_data tmpl_bndrs res_kind res_tmpl
+data DataDeclInfo
+ = DDVanilla -- data T a b = T1 a | T2 b
+ | DDInstance -- data instance D [a] = D1 a | D2
+ Type -- The header D [a]
+
+mkDDHeaderTy :: DataDeclInfo -> TyCon -> [TyConBinder] -> Type
+mkDDHeaderTy dd_info rep_tycon tc_bndrs
+ = case dd_info of
+ DDVanilla -> mkTyConApp rep_tycon $
+ mkTyVarTys (binderVars tc_bndrs)
+ DDInstance header_ty -> header_ty
+
+tcConDecls :: NewOrData
+ -> DataDeclInfo
+ -> KnotTied TyCon -- Representation TyCon
+ -> [TyConBinder] -- Binders of representation TyCon
+ -> TcKind -- Result kind
+ -> [LConDecl GhcRn] -> TcM [DataCon]
+tcConDecls new_or_data dd_info rep_tycon tmpl_bndrs res_kind
= concatMapM $ addLocM $
- tcConDecl rep_tycon (mkTyConTagMap rep_tycon)
- tmpl_bndrs res_kind res_tmpl new_or_data
- -- It's important that we pay for tag allocation here, once per TyCon,
- -- See Note [Constructor tag allocation], fixes #14657
-
-tcConDecl :: KnotTied TyCon -- Representation tycon. Knot-tied!
+ tcConDecl new_or_data dd_info rep_tycon tmpl_bndrs res_kind
+ (mkTyConTagMap rep_tycon)
+ -- mkTyConTagMap: it's important that we pay for tag allocation here,
+ -- once per TyCon. See Note [Constructor tag allocation], fixes #14657
+
+tcConDecl :: NewOrData
+ -> DataDeclInfo
+ -> KnotTied TyCon -- Representation tycon. Knot-tied!
+ -> [TyConBinder] -- Binders of representation TyCon
+ -> TcKind -- Result kind
-> NameEnv ConTag
- -> [TyConBinder] -> TcKind -- tycon binders and result kind
- -> KnotTied Type
- -- Return type template (T tys), where T is the family TyCon
- -> NewOrData
-> ConDecl GhcRn
-> TcM [DataCon]
-tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
+tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
(ConDeclH98 { con_name = lname@(L _ name)
, con_ex_tvs = explicit_tkv_nms
, con_mb_cxt = hs_ctxt
, con_args = hs_args })
- = addErrCtxt (dataConCtxtName [lname]) $
+ = addErrCtxt (dataConCtxt [lname]) $
do { -- NB: the tyvars from the declaration header are in scope
-- 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 +3247,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 +3283,14 @@ 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
+ user_res_ty = mkDDHeaderTy dd_info rep_tycon tc_bndrs
; traceTc "tcConDecl 2" (ppr name)
; is_infix <- tcConIsInfixH98 name hs_args
@@ -3288,9 +3298,9 @@ 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
+ user_res_ty rep_tycon tag_map
-- NB: we put data_tc, the type constructor gotten from the
-- constructor type signature into the data constructor;
-- that way checkValidDataCon can complain if it's wrong.
@@ -3299,14 +3309,14 @@ 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 new_or_data dd_info rep_tycon tc_bndrs _res_kind tag_map
-- 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
, con_bndrs = L _ outer_hs_bndrs
, con_mb_cxt = cxt, con_g_args = hs_args
, con_res_ty = hs_res_ty })
- = addErrCtxt (dataConCtxtName names) $
+ = addErrCtxt (dataConCtxt names) $
do { traceTc "tcConDecl 1 gadt" (ppr names)
; let (L _ name : _) = names
@@ -3317,10 +3327,23 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
-- See Note [GADT return kinds]
+ -- For data instances (only), ensure that the return type,
+ -- res_ty, is a substitution instance of the header.
+ -- See Note [GADT return types]
+ ; case dd_info of
+ DDVanilla -> return ()
+ DDInstance hdr_ty ->
+ do { (subst, _meta_tvs) <- newMetaTyVars (binderVars tc_bndrs)
+ ; let head_shape = substTy subst hdr_ty
+ ; discardResult $
+ popErrCtxt $ -- Drop dataConCtxt
+ addErrCtxt (dataConResCtxt names) $
+ unifyType Nothing res_ty head_shape }
+
-- See Note [Datatype return kinds]
; let exp_kind = getArgExpKind new_or_data res_kind
-
; btys <- tcConGADTArgs exp_kind hs_args
+
; let (arg_tys, stricts) = unzip btys
; field_lbls <- lookupConstructorFields name
; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
@@ -3343,9 +3366,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; ctxt <- zonkTcTypesToTypesX ze ctxt
; res_ty <- zonkTcTypeToTypeX ze res_ty
- ; let (univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
- = rejigConRes tmpl_bndrs res_tmpl tvbndrs res_ty
- -- See Note [Checking GADT return types]
+ ; let res_tmpl = mkDDHeaderTy dd_info rep_tycon tc_bndrs
+ (univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
+ = rejigConRes tc_bndrs res_tmpl tvbndrs res_ty
+ -- See Note [rejigConRes]
ctxt' = substTys arg_subst ctxt
arg_tys' = substScaledTys arg_subst arg_tys
@@ -3372,8 +3396,65 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
where
skol_info = DataConSkol (unLoc (head names))
-{- Note [GADT return kinds]
+{- Note [GADT return types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data family T :: forall k. k -> Type
+ data instance T (a :: Type) where
+ MkT :: forall b. T b
+
+What kind does `b` have in the signature for MkT?
+Since the return type must be an instance of the type in the header,
+we must have (b :: Type), but you can't tell that by looking only at
+the type of the data constructor; you have to look at the header too.
+If you wrote it out fully, it'd look like
+ data instance T @Type (a :: Type) where
+ MkT :: forall (b::Type). T @Type b
+
+We could reject the program, and expect the user to add kind
+annotations to `MkT` to restrict the signature. But an easy, and
+helpful alternative is this: simply instantiate the type from the
+header with fresh unification variables, and unify with the return
+type of `MkT`. That will force `b` to have kind `Type`. See #8707
+and #14111.
+
+Wrikles
+* At first sight it looks as though this would completely subsume the
+ return-type check in checkValidDataCon. But it does not. Suppose we
+ have
+ data instance T [a] where
+ MkT :: T (F (Maybe a))
+
+ where F is a type function. Then maybe (F (Maybe a)) evaluates to
+ [a], so unifyType will succeed. But we discard the coercion
+ returned by unifyType; and we really don't want to accept this
+ program. The check in checkValidDataCon will, however, reject it.
+ TL;DR: keep the check in checkValidDataCon.
+
+* Consider a data type, rather than a data instance, declaration
+ data S a where { MkS :: b -> S [b] }
+ In tcConDecl, S is knot-tied, so we don't want to unify (S alpha)
+ with (S [b]). To put it another way, unifyType should never see a
+ TcTycon. Simple solution: do *not* do the extra unifyType for
+ data types (DDVanilla) only for data instances (DDInstance); in
+ the latter the family constructor is not knot-tied so there is no
+ problem.
+
+* Consider this (fromn GHC itself):
+
+ data Pass = Parsed | ...
+ data GhcPass (c :: Pass) where
+ GhcPs :: GhcPs
+ ...
+ type GhcPs = GhcPass 'Parsed
+
+ Now GhcPs and GhcPass are mutually recursive. If we did unifyType
+ for datatypes like GhcPass, we would not be able to exand the type
+ synonym (it'd still be a TcTyCon). So again, we don't do uinfyType
+ for data types; we leave it to checkValidDataCon.
+
+Note [GADT return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~
Consider
type family Star where Star = Type
data T :: Type where
@@ -3496,8 +3577,8 @@ For example:
(:--:) :: t1 -> t2 -> T Int
-Note [Checking GADT return types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [rejigConRes]
+~~~~~~~~~~~~~~~~~~
There is a delicacy around checking the return types of a datacon. The
central problem is dealing with a declaration like
@@ -3532,9 +3613,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 +3627,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 +3645,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
@@ -3590,11 +3671,11 @@ rejigConRes tmpl_bndrs res_tmpl dc_tvbndrs res_ty
-- we must do *something*, not just crash. So we do something simple
-- 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)
+ -- See Note [rejigConRes]
+ = (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]
~~~~~~~~~~~~~~~~~~~~
@@ -3634,7 +3715,7 @@ becomes
We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We
know this match will succeed because of the validity check (actually done
-later, but laziness saves us -- see Note [Checking GADT return types]).
+later, but laziness saves us -- see Note [rejigConRes]).
Thus, we get
subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z }
@@ -4081,15 +4162,9 @@ checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
-------------------------------
checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
checkValidDataCon dflags existential_ok tc con
- = setSrcSpan (getSrcSpan con) $
- addErrCtxt (dataConCtxt con) $
- do { -- Check that the return type of the data constructor
- -- matches the type constructor; eg reject this:
- -- data T a where { MkT :: Bogus a }
- -- It's important to do this first:
- -- see Note [Checking GADT return types]
- -- and c.f. Note [Check role annotations in a second pass]
- let tc_tvs = tyConTyVars tc
+ = setSrcSpan con_loc $
+ addErrCtxt (dataConCtxt [L con_loc con_name]) $
+ do { let tc_tvs = tyConTyVars tc
res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
orig_res_ty = dataConOrigResTy con
; traceTc "checkValidDataCon" (vcat
@@ -4098,6 +4173,18 @@ checkValidDataCon dflags existential_ok tc con
, ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)])
+ -- Check that the return type of the data constructor
+ -- matches the type constructor; eg reject this:
+ -- data T a where { MkT :: Bogus a }
+ -- It's important to do this first:
+ -- see Note [rejigCon
+ -- and c.f. Note [Check role annotations in a second pass]
+
+ -- Check that the return type of the data constructor is an instance
+ -- of the header of the header of data decl. This checks for
+ -- data T a where { MkT :: S a }
+ -- data instance D [a] where { MkD :: D (Maybe b) }
+ -- see Note [GADT return types]
; checkTc (isJust (tcMatchTyKi res_ty_tmpl orig_res_ty))
(badDataConTyCon con res_ty_tmpl)
-- Note that checkTc aborts if it finds an error. This is
@@ -4205,7 +4292,9 @@ checkValidDataCon dflags existential_ok tc con
Just (f, _) -> ppr (tyConBinders f) ]
}
where
- ctxt = ConArgCtxt (dataConName con)
+ con_name = dataConName con
+ con_loc = nameSrcSpan con_name
+ ctxt = ConArgCtxt con_name
is_strict = \case
NoSrcStrict -> xopt LangExt.StrictData dflags
bang -> isSrcStrict bang
@@ -4869,14 +4958,17 @@ fieldTypeMisMatch field_name con1 con2
= sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
text "give different types for field", quotes (ppr field_name)]
-dataConCtxtName :: [Located Name] -> SDoc
-dataConCtxtName [con]
- = text "In the definition of data constructor" <+> quotes (ppr con)
-dataConCtxtName con
- = text "In the definition of data constructors" <+> interpp'SP con
+dataConCtxt :: [Located Name] -> SDoc
+dataConCtxt cons = text "In the definition of data constructor" <> plural cons
+ <+> ppr_cons cons
+
+dataConResCtxt :: [Located Name] -> SDoc
+dataConResCtxt cons = text "In the result type of data constructor" <> plural cons
+ <+> ppr_cons cons
-dataConCtxt :: Outputable a => a -> SDoc
-dataConCtxt con = text "In the definition of data constructor" <+> quotes (ppr con)
+ppr_cons :: [Located Name] -> SDoc
+ppr_cons [con] = quotes (ppr con)
+ppr_cons cons = interpp'SP cons
classOpCtxt :: Var -> Type -> SDoc
classOpCtxt sel_id tau = sep [text "When checking the class method:",
=====================================
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]
@@ -740,8 +739,9 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
do { data_cons <- tcExtendTyVarEnv qtvs $
-- For H98 decls, the tyvars scope
-- over the data constructors
- tcConDecls rec_rep_tc new_or_data ty_binders final_res_kind
- orig_res_ty hs_cons
+ tcConDecls new_or_data (DDInstance orig_res_ty)
+ rec_rep_tc ty_binders final_res_kind
+ hs_cons
; rep_tc_name <- newFamInstTyConName lfam_name pats
; axiom_name <- newFamInstAxiomName lfam_name [pats]
@@ -857,7 +857,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 +865,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 +884,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 +1049,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
=====================================
@@ -14,6 +14,11 @@ Language
(Serrano et al, ICFP 2020). More information here: :ref:`impredicative-polymorphism`.
This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension.
+* Kind inference for data/newtype instance declarations is slightly
+ 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.
+
+
Compiler
~~~~~~~~
=====================================
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/indexed-types/should_compile/T14111.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE MagicHash, UnboxedSums, NoImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies #-}
+-- {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE GADTs ,ExplicitNamespaces#-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module T14111 where
+
+import GHC.Exts
+import GHC.Types
+import Prelude (undefined)
+import Data.Kind
+import Data.Void
+
+data family Maybe(x :: TYPE (r :: RuntimeRep))
+
+data instance Maybe (a :: Type ) where
+ MaybeSum :: (# a | (# #) #) -> Maybe a
+
+data instance Maybe (x :: TYPE 'UnliftedRep) where
+ MaybeSumU :: (# x | (# #) #) -> Maybe x
=====================================
testsuite/tests/indexed-types/should_compile/T8707.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, GADTs #-}
+
+module T8707 where
+
+import Data.Kind
+
+data family SingDF (a :: (k, k2 -> Type))
+data Ctor :: k -> Type
+
+data instance SingDF (a :: (Bool, Bool -> Type)) where
+ SFalse :: SingDF '(False, Ctor)
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -300,3 +300,5 @@ test('T18809', normal, compile, ['-O'])
test('CEqCanOccursCheck', normal, compile, [''])
test('GivenLoop', normal, compile, [''])
test('T18875', normal, compile, [''])
+test('T8707', normal, compile, ['-O'])
+test('T14111', normal, compile, ['-O'])
=====================================
testsuite/tests/indexed-types/should_fail/T8368.stderr
=====================================
@@ -1,6 +1,5 @@
-T8368.hs:9:3:
- Data constructor ‘MkFam’ returns type ‘Foo’
- instead of an instance of its parent type ‘Fam a’
- In the definition of data constructor ‘MkFam’
- In the data instance declaration for ‘Fam’
+T8368.hs:9:3: error:
+ • Couldn't match expected type ‘Fam a0’ with actual type ‘Foo’
+ • In the result type of data constructor ‘MkFam’
+ In the data instance declaration for ‘Fam’
=====================================
testsuite/tests/indexed-types/should_fail/T8368a.stderr
=====================================
@@ -1,6 +1,7 @@
-T8368a.hs:7:3:
- Data constructor ‘MkFam’ returns type ‘Fam Bool b’
- instead of an instance of its parent type ‘Fam Int b’
- In the definition of data constructor ‘MkFam’
- In the data instance declaration for ‘Fam’
+T8368a.hs:7:3: error:
+ • Couldn't match type ‘Bool’ with ‘Int’
+ Expected: Fam Int b
+ Actual: Fam Bool b
+ • In the result type of data constructor ‘MkFam’
+ In the data instance declaration for ‘Fam’
=====================================
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/T11145.stderr
=====================================
@@ -1,8 +1,7 @@
T11145.hs:8:1: error:
- • Data constructor ‘MkFuggle’ returns type ‘Fuggle
- Int (Maybe Bool)’
- instead of an instance of its parent type ‘Fuggle
- Int (Maybe (a, b))’
- • In the definition of data constructor ‘MkFuggle’
+ • Couldn't match type ‘Bool’ with ‘(a0, b0)’
+ Expected: Fuggle Int (Maybe (a0, b0))
+ Actual: Fuggle Int (Maybe Bool)
+ • In the result type of data constructor ‘MkFuggle’
In the data instance declaration for ‘Fuggle’
=====================================
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. 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
=====================================
@@ -736,3 +736,4 @@ test('InstanceGivenOverlap', normal, compile, [''])
test('InstanceGivenOverlap2', normal, compile, [''])
test('LocalGivenEqs', normal, compile, [''])
test('LocalGivenEqs2', normal, compile, [''])
+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, [''])
@@ -591,3 +592,4 @@ test('T18640c', normal, compile_fail, [''])
test('T10709', normal, compile_fail, [''])
test('T10709b', normal, compile_fail, [''])
test('GivenForallLoop', normal, compile_fail, [''])
+test('T18891a', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f5d93dfbb7eb30ce37f65e7fa0a7d2d65dd51f5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f5d93dfbb7eb30ce37f65e7fa0a7d2d65dd51f5
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/20201203/a3180bc4/attachment-0001.html>
More information about the ghc-commits
mailing list