Commit 42392383 authored by Richard Eisenberg's avatar Richard Eisenberg

Fix #12369 by being more flexible with data insts

Previously, a data family's kind had to end in `Type`,
and data instances had to list all the type patterns for the
family. However, both of these restrictions were unnecessary:

- A data family's kind can usefully end in a kind variable `k`.
  See examples on #12369.

- A data instance need not list all patterns, much like how a
  GADT-style data declaration need not list all type parameters,
  when a kind signature is in place. This is useful, for example,
  here:

    data family Sing (a :: k)
    data instance Sing :: Bool -> Type where ...

This patch also improved a few error messages, as some error
plumbing had to be moved around.

See new Note [Arity of data families] in FamInstEnv for more
info.

test case: indexed-types/should_compile/T12369
parent 1696dbf4
......@@ -34,7 +34,7 @@ module TcHsSyn (
emptyZonkEnv, mkEmptyZonkEnv,
zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
zonkCoToCo, zonkSigType,
zonkEvBinds,
zonkEvBinds, zonkTcEvBinds
) where
#include "HsVersions.h"
......
......@@ -31,10 +31,12 @@ module TcHsType (
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcLHsType, tcCheckLHsType,
tcHsContext, tcLHsPredType, tcInferApps, tcInferArgs,
tcHsContext, tcLHsPredType, tcInferApps, tcTyApps,
solveEqualities, -- useful re-export
kindGeneralize,
typeLevelMode, kindLevelMode,
kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
-- Sort-checking kinds
tcLHsKindSig,
......@@ -275,7 +277,7 @@ tcHsVectInst ty
-- Ignoring the binders looks pretty dodgy to me
= do { (cls, cls_kind) <- tcClass cls_name
; (applied_class, _res_kind)
<- tcInferApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
<- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
; case tcSplitTyConApp_maybe applied_class of
Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
return (cls, args)
......@@ -320,7 +322,7 @@ 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 Type
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
tcCheckLHsType hs_ty exp_kind
= addTypeCtxt hs_ty $
tc_lhs_type typeLevelMode hs_ty exp_kind
......@@ -469,13 +471,13 @@ tc_infer_hs_type mode (HsAppTy ty1 ty2)
= do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
; fun_kind' <- zonkTcType fun_kind
; tcInferApps mode fun_ty fun_ty' fun_kind' arg_tys }
; tcTyApps mode fun_ty fun_ty' fun_kind' arg_tys }
tc_infer_hs_type mode (HsParTy t) = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
| not (op `hasKey` funTyConKey)
= do { (op', op_kind) <- tcTyVar mode op
; op_kind' <- zonkTcType op_kind
; tcInferApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
; tcTyApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
tc_infer_hs_type mode (HsKindSig ty sig)
= do { sig' <- tc_lhs_kind (kindLevel mode) sig
; ty' <- tc_lhs_type mode ty sig'
......@@ -785,42 +787,8 @@ bigConstraintTuple arity
2 (text "Instead, use a nested tuple")
---------------------------
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. However, it does *not* necessarily
-- apply all the arguments, if the kind runs out of binders.
-- Never calls 'matchExpectedFunKind'; when the kind runs out of binders,
-- this stops processing.
-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
-- These kinds should be used to instantiate invisible kind variables;
-- they come from an enclosing class for an associated type/data family.
-- This version will instantiate all invisible arguments left over after
-- the visible ones. Used only when typechecking type/data family patterns
-- (where we need to instantiate all remaining invisible parameters; for
-- example, consider @type family F :: k where F = Int; F = Maybe@. We
-- need to instantiate the @k@.)
tcInferArgs :: Outputable fun
=> fun -- ^ the function
-> [TyConBinder] -- ^ function kind's binders
-> Maybe (VarEnv Kind) -- ^ possibly, kind info (see above)
-> [LHsType GhcRn] -- ^ args
-> TcM (TCvSubst, [TyBinder], [TcType], [LHsType GhcRn], Int)
-- ^ (instantiating subst, un-insted leftover binders,
-- typechecked args, untypechecked args, n)
tcInferArgs fun tc_binders mb_kind_info args
= do { let binders = tyConBindersTyBinders tc_binders -- UGH!
; (subst, leftover_binders, args', leftovers, n)
<- tc_infer_args typeLevelMode fun binders mb_kind_info args 1
-- now, we need to instantiate any remaining invisible arguments
; let (invis_bndrs, other_binders) = break isVisibleBinder leftover_binders
; (subst', invis_args)
<- tcInstBinders subst mb_kind_info invis_bndrs
; return ( subst'
, other_binders
, args' `chkAppend` invis_args
, leftovers, n ) }
-- | See comments for 'tcInferArgs'. But this version does not instantiate
-- any remaining invisible arguments. "RAE" update
tc_infer_args :: Outputable fun
=> TcTyMode
-> fun -- ^ the function
......@@ -855,51 +823,80 @@ tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
go subst [] all_args n acc
= return (subst, [], reverse acc, all_args, n)
-- | Applies a type to a list of arguments.
-- Always consumes all the arguments, using 'matchExpectedFunKind' as
-- necessary. If you wish to apply a type to a list of HsTypes, this is
-- your function.
-- Used for type-checking types only.
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. Always consumes all the arguments,
-- using matchExpectedFunKind as necessary.
-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
-- These kinds should be used to instantiate invisible kind variables;
-- they come from an enclosing class for an associated type/data family.
tcInferApps :: TcTyMode
-> Maybe (VarEnv Kind) -- ^ Possibly, kind info (see above)
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function (could be knot-tied)
-> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, result kind)
tcInferApps mode orig_ty ty ki args = go [] ty ki args 1
-> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
tcInferApps mode mb_kind_info orig_ty ty ki args = go [] [] ty ki args 1
where
go _acc_args fun fun_kind [] _ = return (fun, fun_kind)
go acc_args fun fun_kind args n
go _acc_hs_args acc_args fun fun_kind [] _ = return (fun, reverse acc_args, fun_kind)
go acc_hs_args acc_args fun fun_kind args n
| let (binders, res_kind) = splitPiTys fun_kind
, not (null binders)
= do { (subst, leftover_binders, args', leftover_args, n')
<- tc_infer_args mode orig_ty binders Nothing args n
<- tc_infer_args mode orig_ty binders mb_kind_info args n
; let fun_kind' = substTyUnchecked subst $
mkPiTys leftover_binders res_kind
; go (reverse (dropTail (length leftover_args) args) ++ acc_args)
; go (reverse (dropTail (length leftover_args) args) ++ acc_hs_args)
(reverse args' ++ acc_args)
(mkNakedAppTys fun args') fun_kind' leftover_args n' }
go acc_args fun fun_kind (arg:args) n
= do { (co, arg_k, res_k) <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_args))
go acc_hs_args acc_args fun fun_kind (arg:args) n
= do { (co, arg_k, res_k) <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_hs_args))
fun_kind
; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
tc_lhs_type mode arg arg_k
; go (arg : acc_args)
; go (arg : acc_hs_args) (arg' : acc_args)
(mkNakedAppTy (fun `mkNakedCastTy` co) arg')
res_k args (n+1) }
-- | Applies a type to a list of arguments.
-- Always consumes all the arguments, using 'matchExpectedFunKind' as
-- necessary. If you wish to apply a type to a list of HsTypes, this is
-- your function.
-- Used for type-checking types only.
tcTyApps :: TcTyMode
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function (could be knot-tied)
-> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, result kind)
tcTyApps mode orig_ty ty ki args
= do { (ty', _args, ki') <- tcInferApps mode Nothing orig_ty ty ki args
; return (ty', ki') }
--------------------------
checkExpectedKind :: HsType GhcRn -- HsType whose kind we're checking
-> TcType -- the type whose kind we're checking
-> TcKind -- the known kind of that type, k
-> TcKind -- the expected kind, exp_kind
-> TcM TcType -- a possibly-inst'ed, casted type :: exp_kind
-- like checkExpectedKindX, but returns only the final type; convenient wrapper
checkExpectedKind :: HsType GhcRn
-> TcType
-> TcKind
-> TcKind
-> TcM TcType
checkExpectedKind hs_ty ty act exp = fstOf3 <$> checkExpectedKindX Nothing hs_ty ty act exp
checkExpectedKindX :: Outputable hs_ty
=> Maybe (VarEnv Kind) -- Possibly, instantiations for kind vars
-> hs_ty -- HsType whose kind we're checking
-> TcType -- the type whose kind we're checking
-> TcKind -- the known kind of that type, k
-> TcKind -- the expected kind, exp_kind
-> TcM (TcType, [TcType], TcCoercionN)
-- (an possibly-inst'ed, casted type :: exp_kind, the new args, the coercion)
-- Instantiate a kind (if necessary) and then call unifyType
-- (checkExpectedKind ty act_kind exp_kind)
-- checks that the actual kind act_kind is compatible
-- with the expected kind exp_kind
checkExpectedKind hs_ty ty act_kind exp_kind
= do { (ty', act_kind') <- instantiate ty act_kind exp_kind
checkExpectedKindX mb_kind_env hs_ty ty act_kind exp_kind
= do { (ty', new_args, act_kind') <- instantiate ty act_kind exp_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
, uo_thing = Just (ppr hs_ty)
......@@ -909,7 +906,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind
, ppr exp_kind
, ppr co_k ])
; let result_ty = ty' `mkNakedCastTy` co_k
; return result_ty }
; return (result_ty, new_args, co_k) }
where
-- we need to make sure that both kinds have the same number of implicit
-- foralls out front. If the actual kind has more, instantiate accordingly.
......@@ -919,26 +916,29 @@ checkExpectedKind hs_ty ty act_kind exp_kind
-> TcKind -- of this kind
-> TcKind -- but expected to be of this one
-> TcM ( TcType -- the inst'ed type
, [TcType] -- the new args
, TcKind ) -- its new kind
instantiate ty act_ki exp_ki
= let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
instantiateTyUntilN (length exp_bndrs) ty act_ki
instantiateTyUntilN mb_kind_env (length exp_bndrs) ty act_ki
-- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
-- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
-- (In other words, this function is very forgiving about bad values of @n@.)
instantiateTyN :: Int -- ^ @n@
instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations
-- (for assoc. type patterns)
-> Int -- ^ @n@
-> TcType -- ^ the type
-> [TyBinder] -> TcKind -- ^ its kind
-> TcM (TcType, TcKind) -- ^ The inst'ed type with kind
instantiateTyN n ty bndrs inner_ki
-> TcM (TcType, [TcType], TcKind) -- ^ The inst'ed type, new args, kind
instantiateTyN mb_kind_env n ty bndrs inner_ki
= let -- NB: splitAt is forgiving with invalid numbers
(inst_bndrs, leftover_bndrs) = splitAt n bndrs
ki = mkPiTys bndrs inner_ki
empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
in
if n <= 0 then return (ty, ki) else
do { (subst, inst_args) <- tcInstBinders empty_subst Nothing inst_bndrs
if n <= 0 then return (ty, [], ki) else
do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
ki' = substTy subst rebuilt_ki
; traceTc "instantiateTyN" (vcat [ ppr ty <+> dcolon <+> ppr ki
......@@ -946,18 +946,20 @@ instantiateTyN n ty bndrs inner_ki
, ppr subst
, ppr rebuilt_ki
, ppr ki' ])
; return (mkNakedAppTys ty inst_args, ki') }
; return (mkNakedAppTys ty inst_args, inst_args, ki') }
-- | Instantiate a type to have at most @n@ invisible arguments.
instantiateTyUntilN :: Int -- ^ @n@
instantiateTyUntilN :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
-> Int -- ^ @n@
-> TcType -- ^ the type
-> TcKind -- ^ its kind
-> TcM (TcType, TcKind) -- ^ The inst'ed type with kind
instantiateTyUntilN n ty ki
-> TcM (TcType, [TcType], TcKind) -- ^ The inst'ed type, new args,
-- final kind
instantiateTyUntilN mb_kind_env n ty ki
= let (bndrs, inner_ki) = splitPiTysInvisible ki
num_to_inst = length bndrs - n
in
instantiateTyN num_to_inst ty bndrs inner_ki
instantiateTyN mb_kind_env num_to_inst ty bndrs inner_ki
---------------------------
tcHsContext :: LHsContext GhcRn -> TcM [PredType]
......@@ -1039,8 +1041,8 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
; return (ty, tc_kind) }
| otherwise
= do { (tc_ty, kind) <- instantiateTyN (length (tyConBinders tc_tc))
ty tc_kind_bndrs tc_inner_ki
= do { (tc_ty, _, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
ty tc_kind_bndrs tc_inner_ki
-- tc and tc_ty must not be traced here, because that would
-- force the evaluation of a potentially knot-tied variable (tc),
-- and the typechecker would hang, as per #11708
......@@ -1771,17 +1773,22 @@ tcTyClTyVars tycon_name thing_inside
thing_inside binders res_kind }
-----------------------------------
tcDataKindSig :: Kind -> TcM ([TyConBinder], Kind)
tcDataKindSig :: Bool -- ^ Do we require the result to be *?
-> Kind -> TcM ([TyConBinder], Kind)
-- GADT decls can have a (perhaps partial) kind signature
-- e.g. data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for
-- the argument kinds, and checks that the result kind is indeed *.
-- the argument kinds, and checks that the result kind is indeed * if requested.
-- (Otherwise, checks to make sure that the result kind is either * or a type variable.)
-- See Note [Arity of data families] in FamInstEnv for more info.
-- We use it also to make up argument type variables for for data instances.
-- Never emits constraints.
-- Returns the new TyVars, the extracted TyBinders, and the new, reduced
-- result kind (which should always be Type or a synonym thereof)
tcDataKindSig kind
= do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
tcDataKindSig check_for_type kind
= do { checkTc (isLiftedTypeKind res_kind || (not check_for_type &&
isJust (tcGetCastedTyVar_maybe res_kind)))
(badKindSig check_for_type kind)
; span <- getSrcSpanM
; us <- newUniqueSupply
; rdr_env <- getLocalRdrEnv
......@@ -1801,9 +1808,11 @@ tcDataKindSig kind
where
(tv_bndrs, res_kind) = splitPiTys kind
badKindSig :: Kind -> SDoc
badKindSig kind
= hang (text "Kind signature on data type declaration has non-* return kind")
badKindSig :: Bool -> Kind -> SDoc
badKindSig check_for_type kind
= hang (sep [ text "Kind signature on data type declaration has non-*"
, (if check_for_type then empty else text "and non-variable") <+>
text "return kind" ])
2 (ppr kind)
{-
......
......@@ -638,8 +638,9 @@ tcDataFamInstDecl mb_clsinfo
; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
-- Kind check type patterns
; let mb_kind_env = thdOf3 <$> mb_clsinfo
; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
(kcDataDefn (unLoc fam_tc_name) pats defn) $
(kcDataDefn mb_kind_env (unLoc fam_tc_name) pats defn) $
\tvs pats res_kind ->
do { stupid_theta <- solveEqualities $ tcHsContext ctxt
......@@ -655,17 +656,27 @@ tcDataFamInstDecl mb_clsinfo
; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
; axiom_name <- newFamInstAxiomName fam_tc_name [pats']
-- Deal with any kind signature.
-- See also Note [Arity of data families] in FamInstEnv
; (extra_tcbs, final_res_kind) <- tcDataKindSig True res_kind'
; let (eta_pats, etad_tvs) = eta_reduce pats'
eta_tvs = filterOut (`elem` etad_tvs) tvs'
-- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced
full_tvs = eta_tvs ++ etad_tvs
-- Put the eta-removed tyvars at the end
-- Remember, tvs' is in arbitrary order (except kind vars are
-- first, so there is no reason to suppose that the etad_tvs
-- (obtained from the pats) are at the end (Trac #11148)
orig_res_ty = mkTyConApp fam_tc pats'
extra_pats = map (mkTyVarTy . binderVar) extra_tcbs
all_pats = pats' `chkAppend` extra_pats
orig_res_ty = mkTyConApp fam_tc all_pats
; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
do { let ty_binders = mkTyConBindersPreferAnon full_tvs liftedTypeKind
do { let ty_binders = mkTyConBindersPreferAnon full_tvs res_kind'
`chkAppend` extra_tcbs
; data_cons <- tcConDecls rec_rep_tc
(ty_binders, orig_res_ty) cons
; tc_rhs <- case new_or_data of
......@@ -676,10 +687,10 @@ tcDataFamInstDecl mb_clsinfo
; let axiom = mkSingleCoAxiom Representational
axiom_name eta_tvs [] fam_tc eta_pats
(mkTyConApp rep_tc (mkTyVarTys eta_tvs))
parent = DataFamInstTyCon axiom fam_tc pats'
parent = DataFamInstTyCon axiom fam_tc all_pats
-- NB: Use the full_tvs from the pats. See bullet toward
-- NB: Use the full ty_binders from the pats. See bullet toward
-- the end of Note [Data type families] in TyCon
rep_tc = mkAlgTyCon rep_tc_name
ty_binders liftedTypeKind
......@@ -697,10 +708,10 @@ tcDataFamInstDecl mb_clsinfo
-- Remember to check validity; no recursion to worry about here
-- Check that left-hand sides are ok (mono-types, no type families,
-- consistent instantiations, etc)
; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'
; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats' extra_pats
-- Result kind must be '*' (otherwise, we have too few patterns)
; checkTc (isLiftedTypeKind res_kind') $
; checkTc (isLiftedTypeKind final_res_kind) $
tooFewParmsErr (tyConArity fam_tc)
; checkValidTyCon rep_tc
......
......@@ -33,7 +33,8 @@ import TcTyDecls
import TcClassDcl
import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
import TcDeriv (DerivInfo)
import TcUnify
import TcEvidence ( tcCoercionKind, isEmptyTcEvBinds )
import TcUnify ( checkConstraints )
import TcHsType
import TcMType
import TysWiredIn ( unitTy )
......@@ -61,6 +62,7 @@ import Outputable
import Maybes
import Unify
import Util
import Pair
import SrcLoc
import ListSetOps
import DynFlags
......@@ -826,7 +828,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
= tcTyClTyVars tc_name $ \ binders res_kind -> do
{ traceTc "data family:" (ppr tc_name)
; checkFamFlag tc_name
; (extra_binders, real_res_kind) <- tcDataKindSig res_kind
; (extra_binders, real_res_kind) <- tcDataKindSig False res_kind
; tc_rep_name <- newTyConRepName tc_name
; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
real_res_kind
......@@ -870,7 +872,11 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
Just eqns -> do {
-- Process the equations, creating CoAxBranches
; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, binders, res_kind)
; let fam_tc_shape = FamTyConShape { fs_name = tc_name
, fs_arity = length $ hsQTvExplicit tvs
, fs_flavor = TypeFam
, fs_binders = binders
, fs_res_kind = res_kind }
; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
-- Do not attempt to drop equations dominated by earlier
......@@ -970,7 +976,7 @@ tcDataDefn roles_info
(HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = ctxt, dd_kindSig = mb_ksig
, dd_cons = cons })
= do { (extra_bndrs, real_res_kind) <- tcDataKindSig res_kind
= do { (extra_bndrs, real_res_kind) <- tcDataKindSig True res_kind
; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
roles = roles_info tc_name
......@@ -1090,7 +1096,8 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
setSrcSpan loc $
tcAddFamInstCtxt (text "default type instance") tc_name $
do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
; let shape@(fam_tc_name, fam_arity, _, _) = famTyConShape fam_tc
; let shape@(FamTyConShape { fs_name = fam_tc_name
, fs_arity = fam_arity }) = famTyConShape fam_tc
-- Kind of family check
; ASSERT( fam_tc_name == tc_name )
......@@ -1104,12 +1111,19 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
; let pats = HsIB { hsib_vars = imp_vars ++ map hsLTyVarName exp_vars
, hsib_body = map hsLTyVarBndrToType exp_vars
, hsib_closed = False } -- this field is ignored, anyway
-- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
-- the LHsQTyVars used for declaring a tycon, but the names here
-- are different.
-- You might think we should pass in some ClsInstInfo, as we're looking
-- at an associated type. But this would be wrong, because an associated
-- type default LHS can mention *different* type variables than the
-- enclosing class. So it's treated more as a freestanding beast.
; (pats', rhs_ty)
<- tcFamTyPats shape Nothing pats
(discardResult . tcCheckLHsType rhs) $ \tvs pats rhs_kind ->
(kcTyFamEqnRhs Nothing (mkFamApp fam_tc_name pats) rhs) $
\tvs pats rhs_kind ->
do { rhs_ty <- solveEqualities $
tcCheckLHsType rhs rhs_kind
......@@ -1150,7 +1164,7 @@ proper tcMatchTys here.) -}
-------------------------
kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn GhcRn -> TcM ()
kcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_)
kcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name })
(L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
, tfe_pats = pats
, tfe_rhs = hs_ty }))
......@@ -1159,20 +1173,47 @@ kcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_)
(wrongTyFamName fam_tc_name eqn_tc_name)
; discardResult $
tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type
pats (discardResult . (tcCheckLHsType hs_ty)) }
pats (kcTyFamEqnRhs Nothing (mkFamApp fam_tc_name pats) hs_ty) }
-- Infer the kind of the type on the RHS of a type family eqn. Then use
-- this kind to check the kind of the LHS of the equation. This is useful
-- as the callback to tc_fam_ty_pats and the kind-checker to
-- tcFamTyPats.
kcTyFamEqnRhs :: Maybe ClsInstInfo
-> HsType GhcRn -- ^ Eqn LHS (for errors only)
-> LHsType GhcRn -- ^ Eqn RHS
-> TcKind -- ^ Inferred kind of left-hand side
-> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side
kcTyFamEqnRhs mb_clsinfo lhs_ty rhs_hs_ty lhs_ki
= do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
(_lhs_ty', new_pats, insted_lhs_ki)
<- instantiateTyUntilN mb_kind_env 0 bogus_ty lhs_ki
; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki
; return (new_pats, insted_lhs_ki) }
where
mb_kind_env = thdOf3 <$> mb_clsinfo
bogus_ty = pprPanic "kcTyFamEqnRhs" (ppr lhs_ty $$ ppr rhs_hs_ty)
-- useful when we need an HsType GhcRn for error messages
-- not exported from this module
mkFamApp :: Name -> HsTyPats GhcRn -> HsType GhcRn
mkFamApp fam_tc_name (HsIB { hsib_body = pats })
= unLoc $ mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_tc_name)) pats
tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
-> TcM CoAxBranch
-- Needs to be here, not in TcInstDcls, because closed families
-- (typechecked here) have TyFamInstEqns
tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
tcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name }) mb_clsinfo
(L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
, tfe_pats = pats
, tfe_rhs = hs_ty }))
= ASSERT( fam_tc_name == eqn_tc_name )
setSrcSpan loc $
tcFamTyPats fam_tc_shape mb_clsinfo pats
(discardResult . (tcCheckLHsType hs_ty)) $
(kcTyFamEqnRhs mb_clsinfo (mkFamApp fam_tc_name pats) hs_ty) $
\tvs pats res_kind ->
do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
......@@ -1185,25 +1226,62 @@ tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
(map (const Nominal) tvs')
loc) }
kcDataDefn :: Name -- ^ the family name, for error msgs only
kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
-- (associated types only)
-> Name -- ^ the family name, for error msgs only
-> HsTyPats GhcRn -- ^ the patterns, for error msgs only
-> HsDataDefn GhcRn -- ^ the RHS
-> TcKind -- ^ the expected kind
-> TcM ()
-> TcKind -- ^ the kind of the tycon applied to pats
-> TcM ([TcType], TcKind)
-- ^ the kind signature might force instantiation
-- of the tycon; this returns any extra args and the inst'ed kind
-- See Note [Instantiating a family tycon]
-- Used for 'data instance' only
-- Ordinary 'data' is handled by kcTyClDec
kcDataDefn fam_name (HsIB { hsib_body = pats })
kcDataDefn mb_kind_env fam_name pats
(HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
= do { _ <- tcHsContext ctxt
; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
-- See Note [Failing early in kcDataDefn]
; discardResult $
case mb_kind of
Nothing -> unifyKind (Just hs_ty_pats) res_k liftedTypeKind
Just k -> do { k' <- tcLHsKindSig k
; unifyKind (Just hs_ty_pats) res_k k' } }
; exp_res_kind <- case mb_kind of
Nothing -> return liftedTypeKind
Just k -> tcLHsKindSig k
-- The expected type might have a forall at the type. Normally, we
-- can't skolemise in kinds because we don't have type-level lambda.
-- But here, we're at the top-level of an instance declaration, so
-- 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
; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind
; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise
-- we don't need to do anything substantive with the tvs' because the
-- quantifyTyVars in tcFamTyPats will catch them.
; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind
tv_prs = zip (map tyVarName tvs_to_skolemise) tvs'
skol_info = SigSkol InstDeclCtxt exp_res_kind tv_prs
; (ev_binds, (_, new_args, co))
<- solveEqualities $
checkConstraints skol_info tvs' [] $
checkExpectedKindX mb_kind_env hs_fam_app
bogus_ty res_k inner_res_kind'
; let Pair lhs_ki rhs_ki = tcCoercionKind co
; when debugIsOn $
do { (_, ev_binds) <- zonkTcEvBinds emptyZonkEnv ev_binds
; MASSERT( isEmptyTcEvBinds ev_binds )
; lhs_ki <- zonkTcType lhs_ki
; rhs_ki <- zonkTcType rhs_ki
; MASSERT( lhs_ki `tcEqType` rhs_ki ) }
; return (new_args, lhs_ki) }
where
hs_ty_pats = unLoc $ mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_name)) pats
bogus_ty = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats)
hs_fam_app = mkFamApp fam_name pats