Commit 59e0f754 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent 502647f7
......@@ -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],
......
......@@ -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)
{-
......
......@@ -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]
......
......@@ -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]
......
......@@ -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]
......@@ -1582,14 +1590,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)
......@@ -1646,7 +1654,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
......@@ -3228,11 +3236,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
......@@ -3269,16 +3282,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
......@@ -3287,7 +3303,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"
......
......@@ -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
......
......@@ -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
......
This diff is collapsed.
......@@ -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.
......
......@@ -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))
......
{-# 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
T18300.hs:13:1: error:
• Data instance has non-* return kind ‘TYPE (F Int)’
• In the data instance declaration for ‘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, [''])
......@@ -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, [''])
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment