[Git][ghc/ghc][wip/T18300] Improve handling of data type return kinds
Simon Peyton Jones
gitlab at gitlab.haskell.org
Mon Jun 15 07:48:20 UTC 2020
Simon Peyton Jones pushed to branch wip/T18300 at Glasgow Haskell Compiler / GHC
Commits:
3ce29bdc by Simon Peyton Jones at 2020-06-15T08:46:16+01:00
Improve handling of data type return kinds
Following a long conversation with Richard, this patch tidies up the
handling of return kinds for data/newtype declarations (vanilla,
family, and instance).
I have substantially edited the Notes in TyCl, so they would
bear careful reading.
Fixes #18300.
In GHC.Tc.Instance.Family.newFamInst we were checking some
Lint-like properties with ASSSERT. Instead I've added
Lint.lintAxiom, and called it from newFamInst.
The one new test, T18300, causes an ASSERT failure in HEAD.
- - - - -
14 changed files:
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Instance/Family.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- + testsuite/tests/polykinds/T18300.hs
- + testsuite/tests/polykinds/T18300.stderr
- testsuite/tests/polykinds/all.T
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -418,7 +418,7 @@ data DataCon
-- NB: for a data instance, the original user result type may
-- differ from the DataCon's representation TyCon. Example
-- data instance T [a] where MkT :: a -> T [a]
- -- The OrigResTy is T [a], but the dcRepTyCon might be :T123
+ -- The dcOrigResTy is T [a], but the dcRepTyCon might be R:TList
-- Now the strictness annotations and field labels of the constructor
dcSrcBangs :: [HsSrcBang],
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -640,23 +640,20 @@ 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 ax_tc lhs rhs roles loc
- = -- See Note [CoAxioms are homogeneous] in "GHC.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
- , cab_roles = roles
- , cab_rhs = tidyType env rhs
- , cab_loc = loc
- , cab_incomps = placeHolderIncomps }
+mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
+ = CoAxBranch { cab_tvs = tvs'
+ , cab_eta_tvs = eta_tvs'
+ , cab_cvs = cvs'
+ , cab_lhs = tidyTypes env lhs
+ , cab_roles = roles
+ , cab_rhs = tidyType env rhs
+ , cab_loc = loc
+ , cab_incomps = placeHolderIncomps }
where
(env1, tvs') = tidyVarBndrs init_tidy_env tvs
(env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
@@ -703,7 +700,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 fam_tc lhs_tys rhs_ty
+ branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
(map (const Nominal) tvs)
(getSrcSpan ax_name)
@@ -721,7 +718,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
, co_ax_tc = tycon
, co_ax_branches = unbranched (branch { cab_incomps = [] }) }
where
- branch = mkCoAxBranch tvs [] [] tycon (mkTyVarTys tvs) rhs_ty
+ branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
roles (getSrcSpan name)
{-
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -13,7 +13,7 @@ See Note [Core Lint guarantee].
module GHC.Core.Lint (
lintCoreBindings, lintUnfolding,
lintPassResult, lintInteractiveExpr, lintExpr,
- lintAnnots, lintTypes,
+ lintAnnots, lintAxiom,
-- ** Debug output
endPass, endPassIO,
@@ -1490,17 +1490,32 @@ lintIdBndr top_lvl bind_site id thing_inside
%************************************************************************
-}
-lintTypes :: DynFlags
- -> [TyCoVar] -- Treat these as in scope
- -> [Type]
+lintAxiom :: DynFlags
+ -> CoAxiom Unbranched
-> Maybe MsgDoc -- Nothing => OK
-lintTypes dflags vars tys
+lintAxiom dflags axiom
| isEmptyBag errs = Nothing
| otherwise = Just (pprMessageBag errs)
where
- (_warns, errs) = initL dflags defaultLintFlags vars linter
- linter = lintBinders LambdaBind vars $ \_ ->
- mapM_ lintType tys
+ (_warns, errs) = initL dflags defaultLintFlags [] $
+ lint_axiom axiom
+
+lint_axiom :: CoAxiom Unbranched -> LintM ()
+lint_axiom ax@(CoAxiom { co_ax_tc = fam_tc })
+ = lintBinders LambdaBind (tvs ++ cvs) $ \_ ->
+ do { let lhs = mkTyConApp fam_tc lhs_args
+ ; lhs' <- lintType lhs
+ ; rhs' <- lintType rhs
+ ; let lhs_kind = typeKind lhs'
+ rhs_kind = typeKind rhs'
+ ; checkL (lhs_kind `eqType` rhs_kind) $
+ hang (text "Inhomogeneous axiom")
+ 2 (ppr ax $$ text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind
+ $$ text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }
+ where
+ CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
+ , cab_lhs = lhs_args, cab_rhs = rhs } = coAxiomSingleBranch ax
+
lintValueType :: Type -> LintM LintedType
-- Types only, not kinds
@@ -1520,7 +1535,7 @@ checkTyCon tc
= checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
-------------------
-lintType :: LintedType -> LintM LintedType
+lintType :: Type -> LintM LintedType
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -292,7 +292,14 @@ See also Note [Wrappers for data instance tycons] in GHC.Types.Id.Make
Indeed the latter type is unknown to the programmer.
- There *is* an instance for (T Int) in the type-family instance
- environment, but it is only used for overlap checking
+ environment, but it is looked up (via tcLookupDataFamilyInst)
+ in can_eq_nc (via tcTopNormaliseNewTypeTF_maybe) when trying to
+ solve representational equalities like
+ T Int ~R# Bool
+ Here we look up (T Int), convert it to R:TInt, and then unwrap the
+ newtype R:TInt.
+
+ It is also looked up in reduceTyFamApp_maybe.
- It's fine to have T in the LHS of a type function:
type instance F (T a) = [a]
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -46,7 +46,8 @@ module GHC.Tc.Gen.HsType (
tcNamedWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
- tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType,
+ tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated,
+ tcCheckLHsType,
tcHsMbContext, tcHsContext, tcLHsPredType,
failIfEmitsConstraints,
solveEqualities, -- useful re-export
@@ -74,6 +75,7 @@ import GHC.Tc.Types.Origin
import GHC.Core.Predicate
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Env
+import GHC.Tc.Utils.Instantiate( tcInstInvisibleTyBinders )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Validity
import GHC.Tc.Utils.Unify
@@ -84,7 +86,7 @@ import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Tc.Errors ( reportAllUnsolved )
import GHC.Tc.Utils.TcType
-import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
+import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBindersN, tcInstInvisibleTyBinder )
import GHC.Core.Type
import GHC.Builtin.Types.Prim
import GHC.Types.Name.Reader( lookupLocalRdrOcc )
@@ -612,12 +614,11 @@ tcHsOpenType, tcHsLiftedType,
tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
-- Used for type signatures
-- Do not do validity checking
-tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
-tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
+tcHsOpenType hs_ty = addTypeCtxt hs_ty $ tcHsOpenTypeNC hs_ty
+tcHsLiftedType hs_ty = addTypeCtxt hs_ty $ tcHsLiftedTypeNC hs_ty
-tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
- ; tcLHsType ty ek }
-tcHsLiftedTypeNC ty = tcLHsType ty liftedTypeKind
+tcHsOpenTypeNC hs_ty = do { ek <- newOpenTypeKind; tcLHsType hs_ty ek }
+tcHsLiftedTypeNC hs_ty = tcLHsType hs_ty liftedTypeKind
-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
@@ -627,12 +628,19 @@ tcCheckLHsType hs_ty exp_kind
; tcLHsType hs_ty ek }
tcInferLHsType :: LHsType GhcRn -> TcM TcType
--- Called from outside: set the context
tcInferLHsType hs_ty
- = addTypeCtxt hs_ty $
- do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty
+ = do { (ty,_kind) <- tcInferLHsTypeKind hs_ty
; return ty }
+tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
+-- Called from outside: set the context
+-- Eagerly instantiate any trailing invisible binders
+tcInferLHsTypeKind lhs_ty@(L loc hs_ty)
+ = addTypeCtxt lhs_ty $
+ setSrcSpan loc $ -- Cover the tcInstInvisibleTyBinders
+ do { (res_ty, res_kind) <- tc_infer_hs_type (mkMode TypeLevel) hs_ty
+ ; tcInstInvisibleTyBinders res_ty res_kind }
+
-- Used to check the argument of GHCi :kind
-- Allow and report wildcards, e.g. :kind T _
-- Do not saturate family applications: see Note [Dealing with :kind]
@@ -1587,14 +1595,14 @@ saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
-- tcTypeKind ty = kind
--
-- If 'ty' is an unsaturated family application with trailing
--- invisible arguments, instanttiate them.
+-- invisible arguments, instantiate them.
-- See Note [saturateFamApp]
saturateFamApp ty kind
| Just (tc, args) <- tcSplitTyConApp_maybe ty
, mustBeSaturated tc
, let n_to_inst = tyConArity tc - length args
- = do { (extra_args, ki') <- tcInstInvisibleTyBinders n_to_inst kind
+ = do { (extra_args, ki') <- tcInstInvisibleTyBindersN n_to_inst kind
; return (ty `mkTcAppTys` extra_args, ki') }
| otherwise
= return (ty, kind)
@@ -1651,7 +1659,7 @@ checkExpectedKind :: HasDebugCallStack
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
+ ; (new_args, act_kind') <- tcInstInvisibleTyBindersN n_to_inst act_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
@@ -3218,11 +3226,16 @@ data DataSort
--
-- See also Note [Datatype return kinds] in GHC.Tc.TyCl
checkDataKindSig :: DataSort -> Kind -> TcM ()
-checkDataKindSig data_sort kind = do
- dflags <- getDynFlags
- traceTc "checkDataKindSig" (ppr kind)
- checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags)
+checkDataKindSig data_sort kind
+ = do { dflags <- getDynFlags
+ ; traceTc "checkDataKindSig" (ppr kind)
+ ; checkTc (is_TYPE_or_Type dflags || is_kind_var)
+ (err_msg dflags) }
where
+ res_kind = snd (tcSplitPiTys kind)
+ -- Look for the result kind after
+ -- peeling off any foralls and arrows
+
pp_dec :: SDoc
pp_dec = text $
case data_sort of
@@ -3259,16 +3272,19 @@ checkDataKindSig data_sort kind = do
-- have return kind `TYPE r` unconditionally (#16827).
is_TYPE :: Bool
- is_TYPE = tcIsRuntimeTypeKind kind
+ is_TYPE = tcIsRuntimeTypeKind res_kind
+
+ is_Type :: Bool
+ is_Type = tcIsLiftedTypeKind res_kind
is_TYPE_or_Type :: DynFlags -> Bool
is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE
- | otherwise = tcIsLiftedTypeKind kind
+ | otherwise = is_Type
-- In the particular case of a data family, permit a return kind of the
-- form `:: k` (where `k` is a bare kind variable).
is_kind_var :: Bool
- is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe kind)
+ is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe res_kind)
| otherwise = False
err_msg :: DynFlags -> SDoc
@@ -3277,7 +3293,7 @@ checkDataKindSig data_sort kind = do
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) ])
+ text "return kind" <+> quotes (ppr res_kind) ])
, if not (tYPE_ok dflags) && is_TYPE && is_newtype &&
not (xopt LangExt.UnliftedNewtypes dflags)
then text "Perhaps you intended to use UnliftedNewtypes"
=====================================
compiler/GHC/Tc/Instance/Family.hs
=====================================
@@ -162,34 +162,27 @@ addressed yet.
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
-- Freshen the type variables of the FamInst branches
newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
- = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
- ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
- -- We used to have an assertion that the tyvars of the RHS were bound
- -- by tcv_set, but in error situations like F Int = a that isn't
- -- true; a later check in checkValidFamInst rejects it
- do { (subst, tvs') <- freshenTyVarBndrs tvs
- ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
- ; dflags <- getDynFlags
- ; let lhs' = substTys subst lhs
- rhs' = substTy subst rhs
- tcvs' = tvs' ++ cvs'
+ = do { -- Use lintAxiom to check that the axiom is well formed
+ dflags <- getDynFlags
; ifErrsM (return ()) $ -- Don't lint when there are errors, because
-- errors might mean TcTyCons.
-- See Note [Recover from validity error] in GHC.Tc.TyCl
when (gopt Opt_DoCoreLinting dflags) $
- -- Check that the types involved in this instance are well formed.
- -- Do /not/ expand type synonyms, for the reasons discussed in
- -- Note [Linting type synonym applications].
- case lintTypes dflags tcvs' (rhs':lhs') of
+ case lintAxiom dflags axiom of
Nothing -> pure ()
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 tvs
+ , ppr cvs
+ , ppr lhs
+ , ppr rhs ]
+
+ -- Freshen the type variables
+ ; (subst, tvs') <- freshenTyVarBndrs tvs
+ ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
+ ; let lhs' = substTys subst lhs
+ rhs' = substTy subst rhs
; return (FamInst { fi_fam = tyConName fam_tc
, fi_flavor = flavor
, fi_tcs = roughMatchTcs lhs
@@ -199,10 +192,6 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
, fi_rhs = rhs'
, fi_axiom = axiom }) }
where
- lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
- rhs_kind = tcTypeKind rhs
- tcv_set = mkVarSet (tvs ++ cvs)
- pp_ax = pprCoAxiom axiom
CoAxBranch { cab_tvs = tvs
, cab_cvs = cvs
, cab_lhs = lhs
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -2896,7 +2896,7 @@ pprTcGblEnv (TcGblEnv { tcg_type_env = type_env,
pprUFM (imp_dep_mods imports) (ppr . sort)
, text "Dependent packages:" <+>
ppr (S.toList $ imp_dep_pkgs imports)]
- where -- The use of sort is just to reduce unnecessary
+ -- The use of sort is just to reduce unnecessary
-- wobbling in testsuite output
ppr_rules :: [LRuleDecl GhcTc] -> SDoc
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -1789,6 +1789,276 @@ and take the wired-in information. That avoids complications.
e.g. the need to make the data constructor worker name for
a constraint tuple match the wired-in one
+Note [Datatype return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are several poorly lit corners around datatype/newtype return kinds.
+This Note explains these. We cover data/newtype families and instances
+in Note [Data family/instance return kinds].
+
+data T a :: <kind> where ... -- See Point DT4
+newtype T a :: <kind> where ... -- See Point DT5
+
+DT1 Where this applies: Only GADT syntax for data/newtype/instance declarations
+ can have declared return kinds. This Note does not apply to Haskell98
+ syntax.
+
+DT2 Where these kinds come from: Return kinds are processed through several
+ different code paths:
+
+ Data/newtypes: The return kind is part of the TyCon kind, gotten either
+ by checkInitialKind (standalone kind signature / CUSK) or
+ inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
+ then passed to tcDataDefn.
+
+ Families: The return kind is either written in a standalone signature
+ or extracted from a family declaration in getInitialKind.
+ If a family declaration is missing a result kind, it is assumed to be
+ Type. This assumption is in getInitialKind for CUSKs or
+ get_fam_decl_initial_kind for non-signature & non-CUSK cases.
+
+ Instances: The data family already has a known kind. The return kind
+ of an instance is then calculated by applying the data family tycon
+ to the patterns provided, as computed by the typeKind lhs_ty in the
+ end of tcDataFamInstHeader. In the case of an instance written in GADT
+ syntax, there are potentially *two* return kinds: the one computed from
+ applying the data family tycon to the patterns, and the one given by
+ the user. This second kind is checked by the tc_kind_sig function within
+ tcDataFamInstHeader.
+
+DT3 Eta-expansion: Any forall-bound variables and function arguments in a result kind
+ become parameters to the type. That is, when we say
+
+ data T a :: Type -> Type where ...
+
+ we really mean for T to have two parameters. The second parameter
+ is produced by processing the return kind in etaExpandAlgTyCon,
+ called in tcDataDefn for data/newtypes and in tcDataFamInstDecl
+ for instances. This is true for data families as well, though their
+ arity only matters for pretty-printing.
+
+ See also Note [TyConBinders for the result kind signatures of a data type]
+ in GHC.Tc.Gen.HsType.
+
+DT4 Datatype return kind restriction: A data type return kind must end
+ in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By
+ "end in", we mean we strip any foralls and function arguments off before
+ checking.
+
+ Examples:
+ data T1 :: Type -- good
+ data T2 :: Bool -> Type -- good
+ data T3 :: Bool -> forall k. Type -- strange, but still accepted
+ data T4 :: forall k. k -> Type -- good
+ data T5 :: Bool -- bad
+ data T6 :: Type -> Bool -- bad
+
+ Exactly the same applies to data instance (but not data family)
+ declarations. Examples
+ data instance D1 :: Type -- good
+ data instance D2 :: Boool -> Type -- good
+
+ We can "look through" type synonyms
+ type Star = Type
+ data T7 :: Bool -> Star -- good (synonym expansion ok)
+ type Arrow = (->)
+ data T8 :: Arrow Bool Type -- good (ditto)
+
+ But we specifically do *not* do type family reduction here.
+ type family ARROW where
+ ARROW = (->)
+ data T9 :: ARROW Bool Type -- bad
+
+ type family F a where
+ F Int = Bool
+ F Bool = Type
+ data T10 :: Bool -> F Bool -- bad
+
+ The /principle/ here is that in the TyCon for a data type or data instance,
+ we must be able to lay out all the type-variable binders, one by one, until
+ we reach (TYPE xx). There is no place for a cast here. We could add one,
+ but let's not!
+
+ This check is done in checkDataKindSig. For data declarations, this
+ call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
+
+DT5 Newtype return kind restriction.
+ If -XUnliftedNewtypes is not on, then newtypes are treated just
+ like datatypes --- see (4) above.
+
+
+ If -XUnliftedNewtypes is on, then a newtype return kind must end in
+ TYPE xyz, for some xyz (after type synonym expansion). The "xyz"
+ may include type families, but the TYPE part must be visible
+ /without/ expanding type families (only synonyms).
+
+ This kind is unified with the kind of the representation type (the
+ type of the one argument to the one constructor). See also steps
+ (2) and (3) of Note [Implementation of UnliftedNewtypes].
+
+ The checks are done in the same places as for datatypes.
+ Examples (assume -XUnliftedNewtypes):
+
+ newtype N1 :: Type -- good
+ newtype N2 :: Bool -> Type -- good
+ newtype N3 :: forall r. Bool -> TYPE r -- good
+
+ type family F (t :: Type) :: RuntimeRep
+ newtype N4 :: forall t -> TYPE (F t) -- good
+
+ type family STAR where
+ STAR = Type
+ newtype N5 :: Bool -> STAR -- bad
+
+Note [Data family/instance return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Within this note, understand "instance" to mean data or newtype
+instance, and understand "family" to mean data family. No type
+families or classes here. Some examples:
+
+data family T a :: <kind> -- See Point DF56
+
+data instance T [a] :: <kind> where ... -- See Point DF2
+newtype instance T [a] :: <kind> where ... -- See Point DF2
+
+Here is the Plan for Data Families
+
+DF1 In a data/newtype instance, we treat the kind of the /data family/,
+ once instantiated, as the "master kind" for the representation
+ TyCon. For example:
+ data family T1 :: Type -> Type -> Type
+ data instance T1 Int :: F Bool -> Type where ...
+ The "master kind" for the representation TyCon R:T1Int comes
+ from T1, not from the signature on the data instance. It is as
+ if we declared
+ data R:T1Int :: Type -> Type where ...
+ See Note [Liberalising data family return kinds] for an alternative
+ plan. But this plan is simple, and ensures that all instances
+ are simple instantiations of the matster, without strange casts.
+
+ An example with non-trivial instantiation:
+ data family T2 :: forall k. Type -> k
+ data instance T :: Type -> Type -> Type where ...
+ Here 'k' gets instantiated with (Type -> Type), driven by
+ the signature on the 'data instance'
+
+ A newtype 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
+
+ Here we get that Foo 'Red :: TYPE (Interpret Red), and our
+ representation newtype looks like
+ newtype R:FooRed :: TYPE (Interpret Red) where
+ FooRedC :: Int# -> R:FooRed
+ Remember: the master kind comes from the /family/ tycon.
+
+DF2 /After/ this instantiation, the return kind of the master kind
+ must obey the usual rules for data/newtype return kinds (DT4, DT5)
+ above. Examples:
+ data family T3 k :: k
+ data instance T3 Type where ... -- OK
+ data instance T3 (Type->Type) where ... -- OK
+ data instance T3 (F Int) where ... -- Not OK
+
+DF3 Any kind signatures on the data/newtype instance are checked for
+ equality with the master kind (and hence may guide instantiation)
+ but are otherwise ignored. So in the T1 example above, we check
+ that (F Int ~ Type) by unification; but otherwise ignore the
+ user-supplied signature from the /family/ not the /instance/.
+
+ We must be sure to instantiate any trailing invisible binders
+ before doing this unification. See the call to tcInstInvisibleBinders
+ in tcDataFamInstHeader. For example:
+ data family D :: forall k. k
+ data instance D :: Type -- forall k. k <: Type
+ data instance D :: Type -> Type -- forall k. k <: Type -> Type
+ -- NB: these do not overlap
+ we must instantiate D before unifying with the signature in the
+ data instance declaration
+
+DF4 We also (redundantly) check that any user-specified return kind
+ signature in the data instance also obeys (4). For example we
+ reject
+ data family T1 :: Type -> Type -> Type
+ data instance T1 Int :: Type -> F Int
+ even if (F Int ~ Bool). We could omit this check, because we
+ use the master kind; but it seems more uniform to check it, again
+ with checkDataKindSig.
+
+DF5 Data /family/ return kind restrictions. Consider
+ data family D8 a :: F a
+ where F is a type family. No data/newtype instance can instantiate
+ this so that it obeys the rules of (4) and (5). So GHC proactively
+ rejects the data /family/ declaration if it can never satisfy (DT4)/(DT5).
+ Remember that a data family supports both data and newtype instances.
+
+ More precisely, the return kind of a data family must be either
+ * TYPE xyz (for some type xyz) or
+ * a kind variable
+ Only in these cases can a data/newtype instance possibly satisfy (4)/(5).
+ This is checked by the call to checkDataKindSig in tcFamDecl1. Examples:
+
+ data family D1 :: Type -- good
+ data family D2 :: Bool -> Type -- good
+ data family D3 k :: k -- good
+ data family D4 :: forall k -> k -- good
+ data family D5 :: forall k. k -> k -- good
+ data family D6 :: forall r. TYPE r -- good
+ data family D7 :: Bool -> STAR -- bad (see STAR from point 5)
+
+DF6 Two return kinds for instances: If an instance has two return kinds,
+ one from the family declaration and one from the instance declaration
+ (see point (2) above), they are unified. More accurately, we make sure
+ that the kind of the applied data family is a subkind of the user-written
+ kind. GHC.Tc.Gen.HsType.checkExpectedKind normally does this check for types, but
+ that's overkill for our needs here. Instead, we just instantiate any
+ invisible binders in the (instantiated) kind of the data family
+ (called lhs_kind in tcDataFamInstHeader) with tcInstInvisibleTyBinders
+ and then unify the resulting kind with the kind written by the user.
+ This unification naturally produces a coercion, which we can drop, as
+ the kind annotation on the instance is redundant (except perhaps for
+ effects of unification).
+
+
+
+ This all is Wrinkle (3) in Note [Implementation of UnliftedNewtypes].
+
+Note [Liberalising data family return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Could we allow this?
+ type family F a where { F Int = Type }
+ data family T a :: F a
+ data instance T Int where
+ MkT :: T Int
+
+In the 'data instance', T Int :: F Int, and F Int = Type, so all seems
+well. But there are lots of complications:
+
+* The representation constructor R:TInt presumably has kind Type.
+ So the axiom connecting the two would have to look like
+ axTInt :: T Int ~ R:TInt |> sym axFInt
+ and that doesn't match expectation in DataFamInstTyCon
+ in AlgTyConFlav
+
+* The wrapper can't have type
+ $WMkT :: Int -> T Int
+ because T Int has the wrong kind. It would have to be
+ $WMkT :: Int -> (T Int) |> axFInt
+
+* The code for $WMkT would also be more complicated, needing
+ two coherence coercions. Try it!
+
+* Code for pattern matching would be complicated in an
+ exactly dual way.
+
+So yes, we could allow this, but we currently do not. That's
+why we have
+
Note [Implementation of UnliftedNewtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expected behavior of UnliftedNewtypes:
@@ -1865,11 +2135,12 @@ Wrinkle: Consider (#17021, typecheck/should_fail/T17021)
newtype T :: TYPE (Id LiftedRep) where
MkT :: Int -> T
- In the type of MkT, we must end with (Int |> TYPE (sym axId)) -> T, never Int -> (T |>
- TYPE axId); otherwise, the result type of the constructor wouldn't match the
- datatype. However, type-checking the HsType T might reasonably result in
- (T |> hole). We thus must ensure that this cast is dropped, forcing the
- type-checker to add one to the Int instead.
+ In the type of MkT, we must end with (Int |> TYPE (sym axId)) -> T,
+ never Int -> (T |> TYPE axId); otherwise, the result type of the
+ constructor wouldn't match the datatype. However, type-checking the
+ HsType T might reasonably result in (T |> hole). We thus must ensure
+ that this cast is dropped, forcing the type-checker to add one to
+ the Int instead.
Why is it always safe to drop the cast? This result type is type-checked by
tcHsOpenType, so its kind definitely looks like TYPE r, for some r. It is
@@ -1881,7 +2152,7 @@ Wrinkle: Consider (#17021, typecheck/should_fail/T17021)
Note that this is possible in the H98 case only for a data family, because
the H98 syntax doesn't permit a kind signature on the newtype itself.
-There are also some changes for deailng with families:
+There are also some changes for dealing with families:
1. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if
UnliftedNewtypes is on. This allows us to write things like:
@@ -2290,187 +2561,6 @@ Since the LHS of an associated type family default is always just variables,
it won't contain any tycons. Accordingly, the patterns used in the substitution
won't actually be knot-tied, even though we're in the knot. This is too
delicate for my taste, but it works.
-
-Note [Datatype return kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are several poorly lit corners around datatype/newtype return kinds.
-This Note explains these. Within this note, always understand "instance"
-to mean data or newtype instance, and understand "family" to mean data
-family. No type families or classes here. Some examples:
-
-data T a :: <kind> where ... -- See Point 4
-newtype T a :: <kind> where ... -- See Point 5
-
-data family T a :: <kind> -- See Point 6
-
-data instance T [a] :: <kind> where ... -- See Point 4
-newtype instance T [a] :: <kind> where ... -- See Point 5
-
-1. Where this applies: Only GADT syntax for data/newtype/instance declarations
- can have declared return kinds. This Note does not apply to Haskell98
- syntax.
-
-2. Where these kinds come from: Return kinds are processed through several
- different code paths:
-
- Data/newtypes: The return kind is part of the TyCon kind, gotten either
- by checkInitialKind (standalone kind signature / CUSK) or
- inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
- then passed to tcDataDefn.
-
- Families: The return kind is either written in a standalone signature
- or extracted from a family declaration in getInitialKind.
- If a family declaration is missing a result kind, it is assumed to be
- Type. This assumption is in getInitialKind for CUSKs or
- get_fam_decl_initial_kind for non-signature & non-CUSK cases.
-
- Instances: The data family already has a known kind. The return kind
- of an instance is then calculated by applying the data family tycon
- to the patterns provided, as computed by the typeKind lhs_ty in the
- end of tcDataFamInstHeader. In the case of an instance written in GADT
- syntax, there are potentially *two* return kinds: the one computed from
- applying the data family tycon to the patterns, and the one given by
- the user. This second kind is checked by the tc_kind_sig function within
- tcDataFamInstHeader.
-
-3. Eta-expansion: Any forall-bound variables and function arguments in a result kind
- become parameters to the type. That is, when we say
-
- data T a :: Type -> Type where ...
-
- we really mean for T to have two parameters. The second parameter
- is produced by processing the return kind in etaExpandAlgTyCon,
- called in tcDataDefn for data/newtypes and in tcDataFamInstDecl
- for instances. This is true for data families as well, though their
- arity only matters for pretty-printing.
-
- See also Note [TyConBinders for the result kind signatures of a data type]
- in GHC.Tc.Gen.HsType.
-
-4. Datatype return kind restriction: A data/data-instance return kind must end
- in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By
- "end in", we mean we strip any foralls and function arguments off before
- checking: this remaining part of the type is returned from etaExpandAlgTyCon.
-
- Examples:
- data T1 :: Type -- good
- data T2 :: Bool -> Type -- good
- data T3 :: Bool -> forall k. Type -- strange, but still accepted
- data T4 :: forall k. k -> Type -- good
- data T5 :: Bool -- bad
- data T6 :: Type -> Bool -- bad
-
- Exactly the same applies to data instance (but not data family)
- declarations. Examples
- data instance D1 :: Type -- good
- data instance D2 :: Boool -> Type -- good
-
- We can "look through" type synonyms
- type Star = Type
- data T7 :: Bool -> Star -- good (synonym expansion ok)
- type Arrow = (->)
- data T8 :: Arrow Bool Type -- good (ditto)
-
- But we specifically do *not* do type family reduction here.
- type family ARROW where
- ARROW = (->)
- data T9 :: ARROW Bool Type -- bad
-
- type family F a where
- F Int = Bool
- F Bool = Type
- data T10 :: Bool -> F Bool -- bad
-
- The /principle/ here is that in the TyCon for a data type or data instance,
- we must be able to lay out all the type-variable binders, one by one, until
- we reach (TYPE xx). There is no place for a cast here. We could add one,
- but let's not!
-
- This check is done in checkDataKindSig. For data declarations, this
- call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
-
-4a Because data instances in GADT syntax can have two return kinds (see
- point (2) above), we must check both return kinds. The user-written return
- kind is checked by the call to checkDataKindSig in tcDataFamInstDecl. Examples:
-
- data family D (a :: Nat) :: k -- good (see Point 6)
-
- data instance D 1 :: Type -- good
- data instance D 2 :: F Bool -- bad
-
-5. Newtype return kind restriction: If -XUnliftedNewtypes is on, then
- a newtype/newtype-instance return kind must end in TYPE xyz, for some
- xyz (after type synonym expansion). The "xyz" may include type families,
- but the TYPE part must be visible with expanding type families (only synonyms).
- This kind is unified with the kind of the representation type (the type
- of the one argument to the one constructor). See also steps (2) and (3)
- of Note [Implementation of UnliftedNewtypes].
-
- If -XUnliftedNewtypes is not on, then newtypes are treated just like datatypes.
-
- The checks are done in the same places as for datatypes.
- Examples (assume -XUnliftedNewtypes):
-
- newtype N1 :: Type -- good
- newtype N2 :: Bool -> Type -- good
- newtype N3 :: forall r. Bool -> TYPE r -- good
-
- type family F (t :: Type) :: RuntimeRep
- newtype N4 :: forall t -> TYPE (F t) -- good
-
- type family STAR where
- STAR = Type
- newtype N5 :: Bool -> STAR -- bad
-
-6. Family return kind restrictions: The return kind of a data family must
- be either TYPE xyz (for some xyz) or a kind variable. The idea is that
- instances may specialise the kind variable to fit one of the restrictions
- above. This is checked by the call to checkDataKindSig in tcFamDecl1.
- Examples:
-
- data family D1 :: Type -- good
- data family D2 :: Bool -> Type -- good
- data family D3 k :: k -- good
- data family D4 :: forall k -> k -- good
- data family D5 :: forall k. k -> k -- good
- data family D6 :: forall r. TYPE r -- good
- data family D7 :: Bool -> STAR -- bad (see STAR from point 5)
-
-7. Two return kinds for instances: If an instance has two return kinds,
- one from the family declaration and one from the instance declaration
- (see point (2) above), they are unified. More accurately, we make sure
- that the kind of the applied data family is a subkind of the user-written
- kind. GHC.Tc.Gen.HsType.checkExpectedKind normally does this check for types, but
- that's overkill for our needs here. Instead, we just instantiate any
- invisible binders in the (instantiated) kind of the data family
- (called lhs_kind in tcDataFamInstHeader) with tcInstInvisibleTyBinders
- and then unify the resulting kind with the kind written by the user.
- This unification naturally produces a coercion, which we can drop, as
- the kind annotation on the instance is redundant (except perhaps for
- effects of unification).
-
- 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
-
- Here we get that Foo 'Red :: TYPE (Interpret Red) and we have to
- unify the kind with TYPE IntRep.
-
- Example requiring subkinding:
-
- data family D :: forall k. k
- data instance D :: Type -- forall k. k <: Type
- data instance D :: Type -> Type -- forall k. k <: Type -> Type
- -- NB: these do not overlap
-
- This all is Wrinkle (3) in Note [Implementation of UnliftedNewtypes].
-
-}
{- *********************************************************************
@@ -2500,8 +2590,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
-- When UnliftedNewtypes is enabled, we loosen this restriction
-- on the return kind. See Note [Implementation of UnliftedNewtypes], wrinkle (1).
-- See also Note [Datatype return kinds]
- ; let (_, final_res_kind) = splitPiTys res_kind
- ; checkDataKindSig DataFamilySort final_res_kind
+ ; checkDataKindSig DataFamilySort res_kind
; tc_rep_name <- newTyConRepName tc_name
; let inj = Injective $ replicate (length binders) True
tycon = mkFamilyTyCon tc_name binders
@@ -2796,7 +2885,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo
hs_pats hs_rhs_ty
-- Don't print results they may be knot-tied
-- (tcFamInstEqnGuts zonks to Type)
- ; return (mkCoAxBranch qtvs [] [] fam_tc pats rhs_ty
+ ; return (mkCoAxBranch qtvs [] [] pats rhs_ty
(map (const Nominal) qtvs)
loc) }
@@ -3168,8 +3257,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
}
tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
- -- NB: don't use res_kind here, as it's ill-scoped. Instead, we get
- -- the res_kind by typechecking the result type.
+ -- 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_g_ext = implicit_tkv_nms
, con_names = names
, con_qvars = explicit_tkv_nms
@@ -3186,16 +3275,11 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
bindImplicitTKBndrs_Skol implicit_tkv_nms $
bindExplicitTKBndrs_Skol explicit_tkv_nms $
do { ctxt <- tcHsMbContext cxt
- ; casted_res_ty <- tcHsOpenType hs_res_ty
- ; res_ty <- if not debugIsOn then return $ discardCast casted_res_ty
- else case splitCastTy_maybe casted_res_ty of
- Just (ty, _) -> do unlifted_nts <- xoptM LangExt.UnliftedNewtypes
- MASSERT( unlifted_nts )
- MASSERT( new_or_data == NewType )
- return ty
- _ -> return casted_res_ty
+ ; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
+
-- See Note [Datatype return kinds]
- ; let exp_kind = getArgExpKind new_or_data (typeKind res_ty)
+ ; let exp_kind = getArgExpKind new_or_data res_kind
+
; btys <- tcConArgs exp_kind hs_args
; let (arg_tys, stricts) = unzip btys
; field_lbls <- lookupConstructorFields name
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -703,7 +703,6 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
-- Check the result kind; it may come from a user-written signature.
-- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a)
- ; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind
; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs
all_pats = pats `chkAppend` extra_pats
orig_res_ty = mkTyConApp fam_tc all_pats
@@ -712,10 +711,12 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
; traceTc "tcDataFamInstDecl" $
vcat [ text "Fam tycon:" <+> ppr fam_tc
, text "Pats:" <+> ppr pats
- , text "visibliities:" <+> ppr (tcbVisibilities fam_tc pats)
+ , text "visiblities:" <+> ppr (tcbVisibilities fam_tc pats)
, text "all_pats:" <+> ppr all_pats
, text "ty_binders" <+> ppr ty_binders
, text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
+ , text "res_kind:" <+> ppr res_kind
+ , text "final_res_kind:" <+> ppr final_res_kind
, text "eta_pats" <+> ppr eta_pats
, text "eta_tcbs" <+> ppr eta_tcbs ]
@@ -733,9 +734,9 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
- ; let axiom = mkSingleCoAxiom Representational axiom_name
- post_eta_qtvs eta_tvs [] fam_tc eta_pats
- (mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs))
+ ; let ax_rhs = mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs)
+ axiom = mkSingleCoAxiom Representational axiom_name
+ post_eta_qtvs eta_tvs [] fam_tc eta_pats ax_rhs
parent = DataFamInstTyCon axiom fam_tc all_pats
-- NB: Use the full ty_binders from the pats. See bullet toward
@@ -850,13 +851,17 @@ tcDataFamInstHeader
tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
hs_ctxt hs_pats m_ksig hs_cons new_or_data
= do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
- ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind)))
+ ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
<- pushTcLevelM_ $
solveEqualities $
bindImplicitTKBndrs_Q_Skol imp_vars $
bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
do { stupid_theta <- tcHsContext hs_ctxt
; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
+ ; (lhs_applied_ty, lhs_applied_kind)
+ <- tcInstInvisibleTyBinders lhs_ty lhs_kind
+ -- See Note [Data family/instance return kinds]
+ -- in GHC.Tc.TyCl point (DF3)
-- Ensure that the instance is consistent
-- with its parent class
@@ -868,21 +873,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
- -- See Note [Datatype return kinds] in GHC.Tc.TyCl, 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
+ -- Check that the result kind of the TyCon applied to its args
+ -- is compatible with the explicit signature (or Type, if there
+ -- is none)
+ ; let hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats
; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind
- -- Check that the result kind of the TyCon applied to its args
- -- is compatible with the explicit signature (or Type, if there
- -- is none)
; traceTc "tcDataFamInstHeader" $
vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ]
; return ( stupid_theta
, lhs_applied_ty
+ , lhs_applied_kind
, res_kind ) }
-- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
@@ -899,13 +900,17 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
; (ze, qtvs) <- zonkTyBndrs qtvs
; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
- ; res_kind <- zonkTcTypeToTypeX ze res_kind
+ ; master_res_kind <- zonkTcTypeToTypeX ze master_res_kind
+ ; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
-- We check that res_kind is OK with checkDataKindSig in
-- tcDataFamInstDecl, after eta-expansion. We need to check that
-- it's ok because res_kind can come from a user-written kind signature.
-- See Note [Datatype return kinds], point (4a)
+ ; checkDataKindSig (DataInstanceSort new_or_data) master_res_kind
+ ; checkDataKindSig (DataInstanceSort new_or_data) instance_res_kind
+
-- Check that type patterns match the class instance head
-- The call to splitTyConApp_maybe here is just an inlining of
-- the body of unravelFamInstPats.
@@ -913,7 +918,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
Just (_, pats) -> pure pats
Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
- ; return (qtvs, pats, res_kind, stupid_theta) }
+ ; return (qtvs, pats, master_res_kind, stupid_theta) }
where
fam_name = tyConName fam_tc
data_ctxt = DataKindCtxt fam_name
@@ -972,7 +977,7 @@ however, so this Note aims to describe these subtleties:
* The representation tycon Drep is parameterised over the free
variables of the pattern, in no particular order. So there is no
guarantee that 'p' and 'q' will come last in Drep's parameters, and
- in the right order. So, if the /patterns/ of the family insatance
+ in the right order. So, if the /patterns/ of the family instance
are eta-reducible, we re-order Drep's parameters to put the
eta-reduced type variables last.
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -16,7 +16,7 @@ module GHC.Tc.Utils.Instantiate (
instCall, instDFunType, instStupidTheta, instTyVarsWith,
newWanted, newWanteds,
- tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
+ tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
newOverloadedLit, mkOverLit,
@@ -365,13 +365,19 @@ instStupidTheta orig theta
* *
********************************************************************* -}
--- | Instantiates up to n invisible binders
--- Returns the instantiating types, and body kind
-tcInstInvisibleTyBinders :: Int -> TcKind -> TcM ([TcType], TcKind)
+-- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
+-- returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
+tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
+tcInstInvisibleTyBinders ty kind
+ = do { (extra_args, kind') <- tcInstInvisibleTyBindersN n_invis kind
+ ; return (mkAppTys ty extra_args, kind') }
+ where
+ n_invis = invisibleTyBndrCount kind
-tcInstInvisibleTyBinders 0 kind
+tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
+tcInstInvisibleTyBindersN 0 kind
= return ([], kind)
-tcInstInvisibleTyBinders n ty
+tcInstInvisibleTyBindersN n ty
= go n empty_subst ty
where
empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
=====================================
testsuite/tests/polykinds/T18300.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs, PolyKinds, DataKinds, TypeFamilies #-}
+
+module Foo where
+
+import GHC.Exts
+import Data.Kind
+
+type family F a :: RuntimeRep
+type instance F Int = 'LiftedRep
+
+data family T a :: TYPE (F a)
+
+data instance T Int where
+ MkT :: Int -> T Int
+
+-- ASSERT error in HEAD
=====================================
testsuite/tests/polykinds/T18300.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T18300.hs:13:1: error:
+ • Data instance has non-* return kind ‘TYPE (F Int)’
+ • In the data instance declaration for ‘T’
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -219,3 +219,4 @@ test('T16902', normal, compile_fail, [''])
test('CuskFam', normal, compile, [''])
test('T17841', normal, compile_fail, [''])
test('T17963', normal, compile_fail, [''])
+test('T18300', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -685,7 +685,7 @@ test('UnliftedNewtypesUnifySig', normal, compile, [''])
test('UnliftedNewtypesForall', normal, compile, [''])
test('UnlifNewUnify', normal, compile, [''])
test('UnliftedNewtypesLPFamily', normal, compile, [''])
-test('UnliftedNewtypesDifficultUnification', when(compiler_debugged(), expect_broken(18300)), compile, [''])
+test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
test('T16832', normal, ghci_script, ['T16832.script'])
test('T16995', normal, compile, [''])
test('T17007', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3ce29bdc99994aed33fab2ef2ee3d695cb8ff133
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3ce29bdc99994aed33fab2ef2ee3d695cb8ff133
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/20200615/1b50733c/attachment-0001.html>
More information about the ghc-commits
mailing list