Commit 53ff2cd0 authored by Richard Eisenberg's avatar Richard Eisenberg

Fix #17021 by checking more return kinds

All the details are in new Note [Datatype return kinds] in
TcTyClsDecls.

Test case: typecheck/should_fail/T17021{,b}
           typecheck/should_compile/T17021a

Updates haddock submodule
parent 75168d07
Pipeline #16854 passed with stages
in 544 minutes and 23 seconds
......@@ -198,6 +198,17 @@ axiom as a whole, and they are computed only when the final axiom is built.
During serialization, the list is converted into a list of the indices
of the branches.
Note [CoAxioms are homogeneous]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All axioms must be *homogeneous*, meaning that the kind of the LHS must
match the kind of the RHS. In practice, this means:
Given a CoAxiom { co_ax_tc = ax_tc },
for every branch CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }:
typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs
This is checked in FamInstEnv.mkCoAxBranch.
-}
-- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
......@@ -233,6 +244,7 @@ data CoAxBranch
, cab_roles :: [Role] -- See Note [CoAxBranch roles]
, cab_lhs :: [Type] -- Type patterns to match against
, cab_rhs :: Type -- Right-hand side of the equality
-- See Note [CoAxioms are homogeneous]
, cab_incomps :: [CoAxBranch] -- The previous incompatible branches
-- See Note [Storing compatibility]
}
......
......@@ -638,13 +638,16 @@ that Note.
mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
-> [TyVar] -- Extra eta tyvars
-> [CoVar] -- possibly stale covars
-> TyCon -- family/newtype TyCon (for error-checking only)
-> [Type] -- LHS patterns
-> Type -- RHS
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
= CoAxBranch { cab_tvs = tvs'
mkCoAxBranch tvs eta_tvs cvs ax_tc lhs rhs roles loc
= -- See Note [CoAxioms are homogeneous] in Core.Coercion.Axiom
ASSERT( typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs )
CoAxBranch { cab_tvs = tvs'
, cab_eta_tvs = eta_tvs'
, cab_cvs = cvs'
, cab_lhs = tidyTypes env lhs
......@@ -698,7 +701,7 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
, co_ax_implicit = False
, co_ax_branches = unbranched (branch { cab_incomps = [] }) }
where
branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
branch = mkCoAxBranch tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
(map (const Nominal) tvs)
(getSrcSpan ax_name)
......@@ -716,7 +719,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
, co_ax_tc = tycon
, co_ax_branches = unbranched (branch { cab_incomps = [] }) }
where
branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
branch = mkCoAxBranch tvs [] [] tycon (mkTyVarTys tvs) rhs_ty
roles (getSrcSpan name)
{-
......
......@@ -1388,7 +1388,8 @@ lintInTy ty
= addLoc (InType ty) $
do { ty' <- applySubstTy ty
; k <- lintType ty'
; lintKind k -- The kind returned by lintType is already
; addLoc (InKind ty' k) $
lintKind k -- The kind returned by lintType is already
-- a LintedKind but we also want to check that
-- k :: *, which lintKind does
; return (ty', k) }
......@@ -2278,6 +2279,7 @@ data LintLocInfo
| ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
| TopLevelBindings
| InType Type -- Inside a type
| InKind Type Kind -- Inside a kind
| InCo Coercion -- Inside a coercion
initL :: DynFlags -> LintFlags -> [Var]
......@@ -2533,6 +2535,8 @@ dumpLoc TopLevelBindings
= (noSrcLoc, Outputable.empty)
dumpLoc (InType ty)
= (noSrcLoc, text "In the type" <+> quotes (ppr ty))
dumpLoc (InKind ty ki)
= (noSrcLoc, text "In the kind of" <+> parens (ppr ty <+> dcolon <+> ppr ki))
dumpLoc (InCo co)
= (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
......
......@@ -355,8 +355,8 @@ types are apart. This has practical consequences for the ability for closed
type family applications to reduce. See test case
indexed-types/should_compile/Overlap14.
Note [Unifying with skolems]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Unification with skolems]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we discover that two types unify if and only if a skolem variable is
substituted, we can't properly unify the types. But, that skolem variable
may later be instantiated with a unifyable type. So, we return maybeApart
......
......@@ -498,8 +498,21 @@ nlHsTyVar x = noLoc (HsTyVar noExtField NotPromoted (noLoc x))
nlHsFunTy a b = noLoc (HsFunTy noExtField (parenthesizeHsType funPrec a) b)
nlHsParTy t = noLoc (HsParTy noExtField t)
nlHsTyConApp :: IdP (GhcPass p) -> [LHsType (GhcPass p)] -> LHsType (GhcPass p)
nlHsTyConApp tycon tys = foldl' nlHsAppTy (nlHsTyVar tycon) tys
nlHsTyConApp :: LexicalFixity -> IdP (GhcPass p)
-> [LHsTypeArg (GhcPass p)] -> LHsType (GhcPass p)
nlHsTyConApp fixity tycon tys
| Infix <- fixity
, HsValArg ty1 : HsValArg ty2 : rest <- tys
= foldl' mk_app (noLoc $ HsOpTy noExtField ty1 (noLoc tycon) ty2) rest
| otherwise
= foldl' mk_app (nlHsTyVar tycon) tys
where
mk_app :: LHsType (GhcPass p) -> LHsTypeArg (GhcPass p) -> LHsType (GhcPass p)
mk_app fun@(L _ (HsOpTy {})) arg = mk_app (noLoc $ HsParTy noExtField fun) arg
-- parenthesize things like `(A + B) C`
mk_app fun (HsValArg ty) = noLoc (HsAppTy noExtField fun (parenthesizeHsType appPrec ty))
mk_app fun (HsTypeArg _ ki) = noLoc (HsAppKindTy noSrcSpan fun (parenthesizeHsType appPrec ki))
mk_app fun (HsArgPar _) = noLoc (HsParTy noExtField fun)
nlHsAppKindTy ::
LHsType (GhcPass p) -> LHsKind (GhcPass p) -> LHsType (GhcPass p)
......
......@@ -1044,10 +1044,13 @@ mk_fail_msg dflags pat = "Pattern match failure in do expression at " ++
dsHsVar :: Id -> DsM CoreExpr
dsHsVar var
-- See Wrinkle in Note [Detecting forced eta expansion]
= ASSERT2(null (badUseOfLevPolyPrimop var ty), ppr var $$ ppr ty)
return (varToCoreExpr var) -- See Note [Desugaring vars]
| let bad_tys = badUseOfLevPolyPrimop var ty
, not (null bad_tys)
= do { levPolyPrimopErr (ppr var) ty bad_tys
; return unitExpr } -- return something eminently safe
| otherwise
= return (varToCoreExpr var) -- See Note [Desugaring vars]
where
ty = idType var
......@@ -1134,6 +1137,8 @@ This invariant is checked in dsExpr.
With that representation invariant, we simply look inside every HsWrap
to see if its body is an HsVar whose Id hasNoBinding. Then, we look
at the wrapped type. If it has any levity polymorphic arguments, reject.
Because we might have an HsVar without a wrapper, we check in dsHsVar
as well. typecheck/should_fail/T17021 triggers this case.
Interestingly, this approach does not look to see whether the Id in
question will be eta expanded. The logic is this:
......@@ -1144,20 +1149,6 @@ question will be eta expanded. The logic is this:
argument. If its wrapped type contains levity polymorphic arguments, reject.
So, either way, we're good to reject.
Wrinkle
~~~~~~~
Currently, all levity-polymorphic Ids are wrapped in HsWrap.
However, this is not set in stone, in the future we might make
instantiation more lazy. (See "Visible type application", ESOP '16.)
If we spot a levity-polymorphic hasNoBinding Id without a wrapper,
then that is surely a problem. In this case, we raise an assertion failure.
This failure can be changed to a call to `levPolyPrimopErr` in the future,
if we decide to change instantiation.
We can just check HsVar and HsConLikeOut for RealDataCon, since
we don't have levity-polymorphic pattern synonyms. (This might change
in the future.)
-}
-- | Takes an expression and its instantiated type. If the expression is an
......
......@@ -183,13 +183,14 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
-- Note [Linting type synonym applications].
case lintTypes dflags tcvs' (rhs':lhs') of
Nothing -> pure ()
Just fail_msg -> pprPanic "Core Lint error" (vcat [ fail_msg
Just fail_msg -> pprPanic "Core Lint error in newFamInst" $
vcat [ fail_msg
, ppr fam_tc
, ppr subst
, ppr tvs'
, ppr cvs'
, ppr lhs'
, ppr rhs' ])
, ppr rhs' ]
; return (FamInst { fi_fam = tyConName fam_tc
, fi_flavor = flavor
, fi_tcs = roughMatchTcs lhs
......
......@@ -54,7 +54,6 @@ module TcHsType (
typeLevelMode, kindLevelMode,
kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
checkExpectedKind_pp,
-- Sort-checking kinds
tcLHsKindSig, checkDataKindSig, DataSort(..),
......@@ -400,7 +399,7 @@ tcHsTypeApp wc_ty kind
setXOptM LangExt.PartialTypeSignatures $
-- See Note [Wildcards in visible type application]
tcNamedWildCardBinders sig_wcs $ \ _ ->
tcCheckLHsType hs_ty kind
tcCheckLHsType hs_ty (TheKind kind)
-- We do not kind-generalize type applications: we just
-- instantiate with exactly what the user says.
-- See Note [No generalization in type application]
......@@ -466,10 +465,11 @@ tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
tcCheckLHsType hs_ty exp_kind
= addTypeCtxt hs_ty $
tc_lhs_type typeLevelMode hs_ty exp_kind
do { ek <- newExpectedKind exp_kind
; tc_lhs_type typeLevelMode hs_ty ek }
tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
-- Called from outside: set the context
......@@ -1431,27 +1431,18 @@ checkExpectedKind :: HasDebugCallStack
-> TcKind -- ^ the expected kind
-> TcM TcType
-- Just a convenience wrapper to save calls to 'ppr'
checkExpectedKind hs_ty ty act exp
= checkExpectedKind_pp (ppr hs_ty) ty act exp
checkExpectedKind_pp :: HasDebugCallStack
=> SDoc -- ^ The thing we are checking
-> TcType -- ^ type we're checking
-> TcKind -- ^ the known kind of that type
-> TcKind -- ^ the expected kind
-> TcM TcType
checkExpectedKind_pp pp_hs_ty ty act_kind exp_kind
checkExpectedKind hs_ty ty act_kind exp_kind
= do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind)
; (new_args, act_kind') <- tcInstInvisibleTyBinders n_to_inst act_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
, uo_thing = Just pp_hs_ty
, uo_thing = Just (ppr hs_ty)
, uo_visible = True } -- the hs_ty is visible
; traceTc "checkExpectedKindX" $
vcat [ pp_hs_ty
vcat [ ppr hs_ty
, text "act_kind':" <+> ppr act_kind'
, text "exp_kind:" <+> ppr exp_kind ]
......@@ -1473,7 +1464,6 @@ checkExpectedKind_pp pp_hs_ty ty act_kind exp_kind
n_act_invis_bndrs = invisibleTyBndrCount act_kind
n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
---------------------------
tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
tcHsMbContext Nothing = return []
......@@ -2909,7 +2899,7 @@ Hence using zonked_kinds when forming tvs'.
-----------------------------------
etaExpandAlgTyCon :: [TyConBinder]
-> Kind
-> Kind -- must be zonked
-> TcM ([TyConBinder], Kind)
-- GADT decls can have a (perhaps partial) kind signature
-- e.g. data T a :: * -> * -> * where ...
......@@ -2919,6 +2909,7 @@ etaExpandAlgTyCon :: [TyConBinder]
-- Never emits constraints.
-- It's a little trickier than you might think: see
-- Note [TyConBinders for the result kind signature of a data type]
-- See Note [Datatype return kinds] in TcTyClsDecls
etaExpandAlgTyCon tc_bndrs kind
= do { loc <- getSrcSpanM
; uniqs <- newUniqueSupply
......@@ -2987,6 +2978,8 @@ data DataSort
-- 1. @TYPE r@ (for some @r@), or
--
-- 2. @k@ (where @k@ is a bare kind variable; see #12369)
--
-- See also Note [Datatype return kinds] in TcTyClsDecls
checkDataKindSig :: DataSort -> Kind -> TcM ()
checkDataKindSig data_sort kind = do
dflags <- getDynFlags
......@@ -2995,11 +2988,11 @@ checkDataKindSig data_sort kind = do
pp_dec :: SDoc
pp_dec = text $
case data_sort of
DataDeclSort DataType -> "data type"
DataDeclSort NewType -> "newtype"
DataInstanceSort DataType -> "data instance"
DataInstanceSort NewType -> "newtype instance"
DataFamilySort -> "data family"
DataDeclSort DataType -> "Data type"
DataDeclSort NewType -> "Newtype"
DataInstanceSort DataType -> "Data instance"
DataInstanceSort NewType -> "Newtype instance"
DataFamilySort -> "Data family"
is_newtype :: Bool
is_newtype =
......@@ -3042,8 +3035,8 @@ checkDataKindSig data_sort kind = do
err_msg :: DynFlags -> SDoc
err_msg dflags =
sep [ (sep [ text "Kind signature on" <+> pp_dec <+>
text "declaration has non-" <>
sep [ (sep [ pp_dec <+>
text "has non-" <>
(if tYPE_ok dflags then text "TYPE" else ppr liftedTypeKind)
, (if is_data_family then text "and non-variable" else empty) <+>
text "return kind" <+> quotes (ppr kind) ])
......
......@@ -688,6 +688,8 @@ tcDataFamInstDecl mb_clsinfo
-- NB: we can do this after eta-reducing the axiom, because if
-- we did it before the "extra" tvs from etaExpandAlgTyCon
-- would always be eta-reduced
--
-- See also Note [Datatype return kinds] in TcTyClsDecls
; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind
; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs
......@@ -797,7 +799,7 @@ tcDataFamInstHeader
-- Here the "header" is the bit before the "where"
tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
hs_ctxt hs_pats m_ksig hs_cons new_or_data
= do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty)))
= do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, lhs_applied_kind)))
<- pushTcLevelM_ $
solveEqualities $
bindImplicitTKBndrs_Q_Skol imp_vars $
......@@ -815,8 +817,17 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
-- Add constraints from the data constructors
; kcConDecls new_or_data res_kind hs_cons
; lhs_ty <- checkExpectedKind_pp pp_lhs lhs_ty lhs_kind res_kind
; return (stupid_theta, lhs_ty) }
-- See Note [Datatype return kinds] in TcTyClsDecls, point (7).
; (lhs_extra_args, lhs_applied_kind)
<- tcInstInvisibleTyBinders (invisibleTyBndrCount lhs_kind)
lhs_kind
; let lhs_applied_ty = lhs_ty `mkTcAppTys` lhs_extra_args
hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats
; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind
; return ( stupid_theta
, lhs_applied_ty
, lhs_applied_kind ) }
-- See TcTyClsDecls Note [Generalising in tcFamTyPatsGuts]
-- This code (and the stuff immediately above) is very similar
......@@ -830,9 +841,9 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
-- Zonk the patterns etc into the Type world
; (ze, qtvs) <- zonkTyBndrs qtvs
-- See Note [Unifying data family kinds] about the discardCast
; lhs_ty <- zonkTcTypeToTypeX ze (discardCast lhs_ty)
; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
; lhs_applied_kind <- zonkTcTypeToTypeX ze lhs_applied_kind
-- Check that type patterns match the class instance head
-- The call to splitTyConApp_maybe here is just an inlining of
......@@ -840,12 +851,10 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
; pats <- case splitTyConApp_maybe lhs_ty of
Just (_, pats) -> pure pats
Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
; return (qtvs, pats, typeKind lhs_ty, stupid_theta) }
-- See Note [Unifying data family kinds] about why we need typeKind here
; return (qtvs, pats, lhs_applied_kind, stupid_theta) }
where
fam_name = tyConName fam_tc
data_ctxt = DataKindCtxt fam_name
pp_lhs = pprHsFamInstLHS fam_name mb_bndrs hs_pats fixity hs_ctxt
exp_bndrs = mb_bndrs `orElse` []
-- See Note [Implementation of UnliftedNewtypes] in TcTyClsDecls, wrinkle (2).
......@@ -863,7 +872,11 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
; lvl <- getTcLevel
; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
-- Perhaps surprisingly, we don't need the skolemised tvs themselves
; return (substTy subst inner_kind) }
; let final_kind = substTy subst inner_kind
; checkDataKindSig (DataInstanceSort new_or_data) $
snd $ tcSplitPiTys final_kind
-- See Note [Datatype return kinds], end of point (4)
; return final_kind }
{- Note [Result kind signature for a data family instance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -874,36 +887,6 @@ we actually have a place to put the regeneralised variables.
Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
Examples in indexed-types/should_compile/T12369
Note [Unifying data family kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we kind-check a newtype instance with -XUnliftedNewtypes, we must
unify the kind of the data family with any declared kind in the instance
declaration. For example:
data Color = Red | Blue
type family Interpret (x :: Color) :: RuntimeRep where
Interpret 'Red = 'IntRep
Interpret 'Blue = 'WordRep
data family Foo (x :: Color) :: TYPE (Interpret x)
newtype instance Foo 'Red :: TYPE IntRep where
FooRedC :: Int# -> Foo 'Red
We end up unifying `TYPE (Interpret 'Red)` (the kind of Foo, instantiated
with 'Red) and `TYPE IntRep` (the declared kind of the instance). This
unification succeeds, resulting in a coercion. The big question: what to
do with this coercion? Answer: nothing! A kind annotation on a newtype instance
is always redundant (except, perhaps, in that it helps guide unification). We
have a definitive kind for the data family from the data family declaration,
and so we learn nothing really new from the kind signature on an instance.
We still must perform this unification (done in the call to checkExpectedKind
toward the beginning of tcDataFamInstHeader), but the result is unhelpful. If there
is a cast, it will wrap the lhs_ty, and so we just drop it before splitting the
lhs_ty to reveal the underlying patterns. Because of the potential of dropping
a cast like this, we just use typeKind in the result instead of propagating res_kind
from above.
This Note is wrinkle (3) in Note [Implementation of UnliftedNewtypes] in TcTyClsDecls.
Note [Eta-reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
......@@ -936,7 +919,8 @@ There are several fiddly subtleties lurking here
tycon Drep. The kind of D says it takes four arguments, but the
data instance header only supplies three. But the AlgTyCon for Drep
itself must have enough TyConBinders so that its result kind is Type.
So, with etaExpandAlgTyCon we make up some extra TyConBinders
So, with etaExpandAlgTyCon we make up some extra TyConBinders.
See point (3) in Note [Datatype return kinds] in TcTyClsDecls.
* The result kind in the instance might be a polykind, like this:
data family DP a :: forall k. k -> *
......
This diff is collapsed.
......@@ -923,6 +923,77 @@ for further details. If you are using kind polymorphism and are confused as to
why GHC is rejecting (or accepting) your program, we encourage you to turn on
these flags, especially :ghc-flag:`-fprint-explicit-kinds`.
Datatype return kinds
---------------------
With :extension:`KindSignatures`, we can give the kind of a datatype written
in GADT-syntax (see :extension:`GADTSyntax`). For example::
data T :: Type -> Type where ...
There are a number of restrictions around these *return kinds*. The text below
considers :extension:`UnliftedNewtypes` and data families (enabled by :extension:`TypeFamilies`).
The discussion also assumes familiarity with :ref:`levity polymorphism <runtime-rep>`.
1. ``data`` and ``data instance`` declarations must have return kinds that
end in ``TYPE LiftedRep``. (Recall that ``Type`` is just a synonym for
``TYPE LiftedRep``.) By "end in", we refer to the kind left over after
all arguments (introduced either by ``forall`` or ``->``) are stripped
off and type synonyms expanded. Note that no type family expansion
is done when performing this check.
2. If :extension:`UnliftedNewtypes` is enabled, then ``newtype`` and
``newtype instance`` declarations must have return kinds that end
in ``TYPE rep`` for some ``rep``. The ``rep`` may mention type families,
but the ``TYPE`` must be apparent without type family expansion.
(Type synonym expansion is acceptable.)
If :extension:`UnliftedNewtypes` is not enabled, then ``newtype`` and
``newtype instance`` declarations have the same restrictions as ``data``
declarations.
3. A ``data`` or ``newtype`` instance actually can have *two* return kinds.
The first is the kind derived by applying the data family to the
patterns provided in the instance declaration. The second is given by
a kind annotation. Both return kinds must satisfy the restrictions
above.
Examples::
data T1 :: Type -- good: Type expands to TYPE LiftedRep
data T2 :: TYPE LiftedRep -- good
data T3 :: forall k. k -> Type -> Type -- good: arguments are dropped
type LR = LiftedRep
data T3 :: TYPE LR -- good: we look through type synonyms
type family F a where
F Int = LiftedRep
data T4 :: TYPE (F Int) -- bad: we do not look through type families
type family G a where
G Int = Type
data T5 :: G Int -- bad: we do not look through type families
-- assume -XUnliftedNewtypes
newtype T6 :: Type where ... -- good
newtype T7 :: TYPE (F Int) where ... -- good
newtype T8 :: G Int where ... -- bad
data family DF a :: Type
data instance DF Int :: Type -- good
data instance DF Bool :: TYPE LiftedRep -- good
data instance DF Char :: G Int -- bad
data family DF2 k :: k -- good
data family DF2 Type -- good
data family DF2 Bool -- bad
data family DF2 (G Int) -- bad for 2 reasons:
-- a type family can't be in a pattern, and
-- the kind fails the restrictions here
.. index::
single: TYPE
single: levity polymorphism
......
T15787.hs:15:43: error:
• Expected kind ‘ob’, but ‘k’ has kind ‘*’
• In the second argument of ‘Kl_kind’, namely ‘k’
In the type ‘Kl_kind (m :: ob -> ob) k’
T15787.hs:15:14: error:
• Expected a type, but ‘k’ has kind ‘ob’
• In the type ‘k’
In the definition of data constructor ‘Kl’
In the data declaration for ‘Kl_kind’
......@@ -9,13 +9,13 @@ T7230.hs:48:32: error:
at T7230.hs:47:1-68
or from: xs ~ (x : xs1)
bound by a pattern with constructor:
SCons :: forall {a} (x :: a) (xs :: [a]).
SCons :: forall {k} (x :: k) (xs :: [k]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘crash’
at T7230.hs:48:8-27
or from: xs1 ~ (x1 : xs2)
bound by a pattern with constructor:
SCons :: forall {a} (x :: a) (xs :: [a]).
SCons :: forall {k} (x :: k) (xs :: [k]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘crash’
at T7230.hs:48:17-26
......
......@@ -8,7 +8,7 @@ T9222.hs:14:3: error:
at T9222.hs:14:3-43
‘c’ is a rigid type variable bound by
the type of the constructor ‘Want’:
forall {i1} {j1} (a :: (i1, j1)) (b :: i1) (c :: j1).
forall {k1} {j1} (a :: (k1, j1)) (b :: k1) (c :: j1).
((a ~ '(b, c)) => Proxy b) -> Want a
at T9222.hs:14:3-43
• In the ambiguity check for ‘Want’
......
{-# LANGUAGE StandaloneKindSignatures, PolyKinds, DataKinds, TypeFamilies,
UnliftedNewtypes #-}
module T17021a where
import Data.Kind
import GHC.Exts
type family Id x where
Id x = x
type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
newtype LevId x = MkLevId x
type LevId2 :: (r ~ Id LiftedRep) => TYPE r -> TYPE r
newtype LevId2 x = MkLevId2 x
......@@ -700,3 +700,4 @@ test('T12926', reqlib('vector'), compile, ['-O2'])
test('T17710', normal, compile, [''])
test('T17792', normal, compile, [''])
test('T17024', normal, compile, [''])
test('T17021a', normal, compile, [''])
......@@ -8,4 +8,3 @@ newtype A where
MkA :: Int# -> A
newtype B = MkB Int#
T12729.hs:8:4: error:
A newtype cannot have an unlifted argument type
T12729.hs:7:1: error:
Newtype has non-* return kind ‘TYPE 'IntRep’
Perhaps you intended to use UnliftedNewtypes
• In the definition of data constructor ‘MkA’
In the newtype declaration for ‘A’
T12729.hs:10:13: error:
• A newtype cannot have an unlifted argument type
Perhaps you intended to use UnliftedNewtypes
• In the definition of data constructor ‘MkB’
In the newtype declaration for ‘B’
• In the newtype declaration for ‘A’
T14048a.hs:6:1: error:
• Kind signature on data type declaration has non-*
return kind ‘Constraint’
• Data type has non-* return kind ‘Constraint’
• In the data declaration for ‘Foo’
T14048b.hs:7:1: error:
Kind signature on data family declaration has non-TYPE
Data family has non-TYPE
and non-variable return kind ‘Constraint’
• In the data family declaration for ‘Foo’
T14048c.hs:9:1: error:
• Kind signature on data instance declaration has non-*
return kind ‘Constraint’
• Data instance has non-* return kind ‘Constraint’
• In the data instance declaration for ‘Foo’
T15807.hs:12:24: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘k0 -> *’
• In the first argument of ‘App’, namely ‘f’
In the type ‘App @f a’
In the definition of data constructor ‘MkApp’
T15807.hs:12:26: error:
• Couldn't match kind ‘*’ with ‘k0 -> *’
When matching kinds
k0 :: *
f :: k0 -> *
• In the second argument of ‘App’, namely ‘a’
In the type ‘App @f a’
T15807.hs:12:12: error:
• Expected kind ‘f -> *’, but ‘f’ has kind ‘*’
• In the type ‘f a’
In the definition of data constructor ‘MkApp’
In the data declaration for ‘App’
T15883.hs:9:19:
A newtype cannot have an unlifted argument type
T15883.hs:9:1: error:
• Newtype has non-* return kind ‘TYPE rep’
Perhaps you intended to use UnliftedNewtypes
In the definition of data constructor ‘MkFoo’
In the newtype declaration for ‘Foo’
• In the newtype declaration for ‘Foo’
T16821.hs:12:1: error:
• Kind signature on newtype declaration has non-TYPE
return kind ‘Id (*)’
• Newtype has non-TYPE return kind ‘Id (*)’
• In the newtype declaration for ‘T’
T16829a.hs:9:1: error:
• Kind signature on newtype declaration has non-*
return kind ‘TYPE 'IntRep’
• Newtype has non-* return kind ‘TYPE 'IntRep’
Perhaps you intended to use UnliftedNewtypes
• In the newtype declaration for ‘T’
T16829b.hs:10:1: error:
• Kind signature on newtype instance declaration has non-*
return kind ‘TYPE 'IntRep’
• Newtype instance has non-* return kind ‘TYPE 'IntRep’
Perhaps you intended to use UnliftedNewtypes
• In the newtype instance declaration for ‘T’
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnliftedNewtypes #-}
module T17021 where
import Data.Kind
import GHC.Exts
type family Id (x :: a) :: a where
Id x = x
newtype T :: TYPE (Id LiftedRep) where
MkT :: Int -> T
f :: T
f = MkT 42
T17021.hs:18:5: error:
Cannot use function with levity-polymorphic arguments:
T17021.MkT :: Int -> T
(Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
are eta-expanded internally because they must occur fully saturated.
Use -fprint-typechecker-elaboration to display the full expression.)
Levity-polymorphic arguments: Int :: TYPE (Id 'LiftedRep)
T17021.hs:18:9: error:
A levity-polymorphic type is not allowed here:
Type: Int
Kind: TYPE (Id 'LiftedRep)
In the type of expression: 42
{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
module T17021b where
import Data.Kind
data family Fix (f :: Type