diff options
Diffstat (limited to 'compiler/typecheck/TcTyClsDecls.hs')
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 196 |
1 files changed, 106 insertions, 90 deletions
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index e68efd09f9..6fee0124a3 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -126,8 +126,8 @@ tcTyClGroup tyclds = do { -- Step 1: kind-check this group and returns the final -- (possibly-polymorphic) kind of each TyCon and Class -- See Note [Kind checking for type and class decls] - names_w_poly_kinds <- kcTyClGroup tyclds - ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds) + tc_tycons <- kcTyClGroup tyclds + ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons)) -- Step 2: type-check all groups together, returning -- the final TyCons and Classes @@ -143,13 +143,12 @@ tcTyClGroup tyclds -- NB: if the decls mention any ill-staged data cons -- (see Note [Recusion and promoting data constructors]) -- we will have failed already in kcTyClGroup, so no worries here - ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $ + ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $ -- Also extend the local type envt with bindings giving -- the (polymorphic) kind of each knot-tied TyCon or Class -- See Note [Type checking recursive type and class declarations] - tcExtendKindEnv2 [ mkTcTyConPair name kind m_arity - | (name, kind, m_arity) <- names_w_poly_kinds ] $ + tcExtendKindEnv2 (map mkTcTyConPair tc_tycons) $ -- Kind and type check declarations for this group mapM (tcTyClDecl rec_flags) decls } @@ -169,8 +168,12 @@ tcTyClGroup tyclds -- they may be mentioned in interface files ; tcExtendTyConEnv tyclss $ tcAddImplicits tyclss } + where + ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma + , ppr (tyConBinders tc) <> comma + , ppr (tyConResKind tc) ]) -zipRecTyClss :: [(Name, Kind, Maybe Arity)] +zipRecTyClss :: [TcTyCon] -> [TyCon] -- Knot-tied -> [(Name,TyThing)] -- Build a name-TyThing mapping for the TyCons bound by decls @@ -178,8 +181,8 @@ zipRecTyClss :: [(Name, Kind, Maybe Arity)] -- The TyThings in the result list must have a visible ATyCon, -- because typechecking types (in, say, tcTyClDecl) looks at -- this outer constructor -zipRecTyClss kind_pairs rec_tycons - = [ (name, ATyCon (get name)) | (name, _kind, _m_arity) <- kind_pairs ] +zipRecTyClss tc_tycons rec_tycons + = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ] where rec_tc_env :: NameEnv TyCon rec_tc_env = foldr add_tc emptyNameEnv rec_tycons @@ -260,7 +263,7 @@ See also Note [Kind checking recursive type and class declarations] -} -kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind,Maybe Arity)] +kcTyClGroup :: TyClGroup Name -> TcM [TcTyCon] -- Kind check this group, kind generalize, and return the resulting local env -- This bindds the TyCons and Classes of the group, but not the DataCons -- See Note [Kind checking for type and class decls] @@ -303,24 +306,29 @@ kcTyClGroup (TyClGroup { group_tyclds = decls }) ; return res } where - generalise :: TcTypeEnv -> Name -> TcM (Name, Kind, Maybe Arity) + generalise :: TcTypeEnv -> Name -> TcM TcTyCon -- For polymorphic things this is a no-op generalise kind_env name - = do { let (kc_kind, kc_unsat) = case lookupNameEnv kind_env name of - Just (ATcTyCon tc) -> ( tyConKind tc - , if mightBeUnsaturatedTyCon tc - then Nothing - else Just $ tyConArity tc ) - _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env) - ; kvs <- kindGeneralize kc_kind - ; kc_kind' <- zonkTcTypeToType emptyZonkEnv kc_kind + = do { let tc = case lookupNameEnv kind_env name of + Just (ATcTyCon tc) -> tc + _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env) + kc_binders = tyConBinders tc + kc_res_kind = tyConResKind tc + ; kvs <- kindGeneralize (mkForAllTys kc_binders kc_res_kind) + ; (kc_binders', kc_res_kind') <- zonkTcKindToKind kc_binders kc_res_kind -- Make sure kc_kind' has the final, zonked kind variables - ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ]) - ; return (name, mkInvForAllTys kvs kc_kind', kc_unsat) } + ; traceTc "Generalise kind" $ + vcat [ ppr name, ppr kc_binders, ppr kc_res_kind + , ppr kvs, ppr kc_binders', ppr kc_res_kind' ] + + ; return (mkTcTyCon name + (map (mkNamedBinder Invisible) kvs ++ kc_binders') + kc_res_kind' + (mightBeUnsaturatedTyCon tc)) } generaliseTCD :: TcTypeEnv - -> LTyClDecl Name -> TcM [(Name, Kind, Maybe Arity)] + -> LTyClDecl Name -> TcM [TcTyCon] generaliseTCD kind_env (L _ decl) | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl = do { first <- generalise kind_env name @@ -336,19 +344,15 @@ kcTyClGroup (TyClGroup { group_tyclds = decls }) ; return [res] } generaliseFamDecl :: TcTypeEnv - -> FamilyDecl Name -> TcM (Name, Kind, Maybe Arity) + -> FamilyDecl Name -> TcM TcTyCon generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name }) = generalise kind_env name -mkTcTyConPair :: Name -> TcKind - -> Maybe Arity -- ^ Nothing <=> tycon can be unsaturated - -> (Name, TcTyThing) +mkTcTyConPair :: TcTyCon -> (Name, TcTyThing) -- Makes a binding to put in the local envt, binding --- a name to a TcTyCon with the specified kind -mkTcTyConPair name kind Nothing - = (name, ATcTyCon (mkTcTyCon name kind True 0)) -mkTcTyConPair name kind (Just arity) - = (name, ATcTyCon (mkTcTyCon name kind False arity)) +-- a name to a TcTyCon +mkTcTyConPair tc + = (getName tc, ATcTyCon tc) mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)] mk_thing_env [] = [] @@ -388,26 +392,28 @@ getInitialKind :: TyClDecl Name -- No family instances are passed to getInitialKinds getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) - = do { (cl_kind, inner_prs) <- + = do { (cl_binders, cl_kind, inner_prs) <- kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ -> do { inner_prs <- getFamDeclInitialKinds ats ; return (constraintKind, inner_prs) } - ; cl_kind <- zonkTcType cl_kind - ; let main_pr = mkTcTyConPair name cl_kind Nothing + ; cl_binders <- mapM zonkTcTyBinder cl_binders + ; cl_kind <- zonkTcType cl_kind + ; let main_pr = mkTcTyConPair (mkTcTyCon name cl_binders cl_kind True) ; return (main_pr : inner_prs) } getInitialKind decl@(DataDecl { tcdLName = L _ name , tcdTyVars = ktvs , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig , dd_cons = cons } }) - = do { (decl_kind, _) <- + = do { (decl_binders, decl_kind, _) <- kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ -> do { res_k <- case m_sig of Just ksig -> tcLHsKind ksig Nothing -> return liftedTypeKind ; return (res_k, ()) } - ; decl_kind <- zonkTcType decl_kind - ; let main_pr = mkTcTyConPair name decl_kind Nothing + ; decl_binders <- mapM zonkTcTyBinder decl_binders + ; decl_kind <- zonkTcType decl_kind + ; let main_pr = mkTcTyConPair (mkTcTyCon name decl_binders decl_kind True) inner_prs = [ (unLoc con, APromotionErr RecDataConPE) | L _ con' <- cons, con <- getConNames con' ] ; return (main_pr : inner_prs) } @@ -431,7 +437,7 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name , fdTyVars = ktvs , fdResultSig = L _ resultSig , fdInfo = info }) - = do { (fam_kind, _) <- + = do { (fam_binders, fam_kind, _) <- kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $ \_ _ -> do { res_k <- case resultSig of KindSig ki -> tcLHsKind ki @@ -442,42 +448,43 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name -- by default | otherwise -> newMetaKindVar ; return (res_k, ()) } - ; fam_kind <- zonkTcType fam_kind - ; return [ mkTcTyConPair name fam_kind m_arity ] } + ; fam_binders <- mapM zonkTcTyBinder fam_binders + ; fam_kind <- zonkTcType fam_kind + ; return [ mkTcTyConPair (mkTcTyCon name fam_binders fam_kind unsat) ] } where - m_arity = case info of - DataFamily -> Nothing - OpenTypeFamily -> Just (length $ hsQTvExplicit ktvs) - ClosedTypeFamily _ -> Just (length $ hsQTvExplicit ktvs) + unsat = case info of + DataFamily -> True + OpenTypeFamily -> False + ClosedTypeFamily _ -> False ---------------- kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM TcLclEnv -- Kind bindings kcSynDecls [] = getLclEnv kcSynDecls (group : groups) - = do { (n,k,arity) <- kcSynDecl1 group - ; tcExtendKindEnv2 [ mkTcTyConPair n k (Just arity) ] $ + = do { tc <- kcSynDecl1 group + ; tcExtendKindEnv2 [ mkTcTyConPair tc ] $ kcSynDecls groups } kcSynDecl1 :: SCC (LTyClDecl Name) - -> TcM (Name,TcKind,Arity) -- Kind bindings + -> TcM TcTyCon -- Kind bindings kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl kcSynDecl1 (CyclicSCC decls) = do { recSynErr decls; failM } -- Fail here to avoid error cascade -- of out-of-scope tycons -kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind, Arity) +kcSynDecl :: TyClDecl Name -> TcM TcTyCon kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name , tcdRhs = rhs }) -- Returns a possibly-unzonked kind = tcAddDeclCtxt decl $ - do { (syn_kind, _) <- + do { (syn_binders, syn_kind, _) <- kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $ \_ _ -> do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs)) ; (_, rhs_kind) <- tcLHsType rhs ; traceTc "kcd2" (ppr name) ; return (rhs_kind, ()) } - ; return (name, syn_kind, length $ hsQTvExplicit hs_tvs) } + ; return (mkTcTyCon name syn_binders syn_kind False) } kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl) ------------------------------------------------------------------------ @@ -525,10 +532,11 @@ kcTyClDecl (FamDecl (FamilyDecl { fdLName = L _ fam_tc_name -- do anything here = case fd_info of ClosedTypeFamily (Just eqns) -> - do { tc_kind <- kcLookupKind fam_tc_name + do { (tc_binders, tc_res_kind) <- kcLookupKind fam_tc_name ; let fam_tc_shape = ( fam_tc_name , length $ hsQTvExplicit hs_tvs - , tc_kind ) + , tc_binders + , tc_res_kind ) ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns } _ -> return () @@ -676,15 +684,15 @@ tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd }) tcTyClDecl1 _parent rec_info (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs }) = ASSERT( isNothing _parent ) - tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind res_kind -> - tcTySynRhs rec_info tc_name (kvs' ++ tvs') full_kind res_kind rhs + tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> + tcTySynRhs rec_info tc_name (kvs' ++ tvs') binders res_kind rhs -- "data/newtype" declaration tcTyClDecl1 _parent rec_info (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn }) = ASSERT( isNothing _parent ) - tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind -> - tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_kind res_kind defn + tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_binders res_kind -> + tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_binders res_kind defn tcTyClDecl1 _parent rec_info (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs @@ -693,13 +701,13 @@ tcTyClDecl1 _parent rec_info , tcdATs = ats, tcdATDefs = at_defs }) = ASSERT( isNothing _parent ) do { clas <- fixM $ \ clas -> - tcTyClTyVars class_name tvs $ \ kvs' tvs' full_kind res_kind -> + tcTyClTyVars class_name tvs $ \ kvs' tvs' binders res_kind -> do { MASSERT( isConstraintKind res_kind ) -- This little knot is just so we can get -- hold of the name of the class TyCon, which we -- need to look up its recursiveness ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$ - ppr tvs' $$ ppr full_kind) + ppr tvs' $$ ppr binders) ; let tycon_name = tyConName (classTyCon clas) tc_isrec = rti_is_rec rec_info tycon_name roles = rti_roles rec_info tycon_name @@ -712,7 +720,7 @@ tcTyClDecl1 _parent rec_info ; at_stuff <- tcClassATs class_name clas ats at_defs ; mindef <- tcClassMinimalDef class_name sigs sig_stuff ; clas <- buildClass - class_name (kvs' ++ tvs') roles ctxt' full_kind + class_name (kvs' ++ tvs') roles ctxt' binders fds' at_stuff sig_stuff mindef tc_isrec ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$ @@ -730,25 +738,26 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na , fdTyVars = tvs, fdResultSig = L _ sig , fdInjectivityAnn = inj }) | DataFamily <- fam_info - = tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind -> do + = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do { traceTc "data family:" (ppr tc_name) ; checkFamFlag tc_name - ; extra_tvs <- tcDataKindSig res_kind + ; (extra_tvs, extra_binders, real_res_kind) <- tcDataKindSig res_kind ; tc_rep_name <- newTyConRepName tc_name ; let final_tvs = (kvs' ++ tvs') `chkAppend` extra_tvs -- we may not need these - tycon = mkFamilyTyCon tc_name tycon_kind final_tvs + tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders) + real_res_kind final_tvs (resultVariableName sig) (DataFamilyTyCon tc_rep_name) parent NotInjective ; return tycon } | OpenTypeFamily <- fam_info - = tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind _res_kind -> do + = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do { traceTc "open type family:" (ppr tc_name) ; checkFamFlag tc_name ; let all_tvs = kvs' ++ tvs' ; inj' <- tcInjectivity all_tvs inj - ; let tycon = mkFamilyTyCon tc_name full_kind all_tvs + ; let tycon = mkFamilyTyCon tc_name binders res_kind all_tvs (resultVariableName sig) OpenSynFamilyTyCon parent inj' ; return tycon } @@ -759,11 +768,12 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na do { traceTc "Closed type family:" (ppr tc_name) -- the variables in the header scope only over the injectivity -- declaration but this is not involved here - ; (tvs', inj', kind) <- tcTyClTyVars tc_name tvs - $ \ kvs' tvs' full_kind _res_kind -> - do { let all_tvs = kvs' ++ tvs' - ; inj' <- tcInjectivity all_tvs inj - ; return (all_tvs, inj', full_kind) } + ; (tvs', inj', binders, res_kind) + <- tcTyClTyVars tc_name tvs + $ \ kvs' tvs' binders res_kind -> + do { let all_tvs = kvs' ++ tvs' + ; inj' <- tcInjectivity all_tvs inj + ; return (all_tvs, inj', binders, res_kind) } ; checkFamFlag tc_name -- make sure we have -XTypeFamilies @@ -771,14 +781,14 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na -- but eqns might be empty in the Just case as well ; case mb_eqns of Nothing -> - return $ mkFamilyTyCon tc_name kind tvs' + return $ mkFamilyTyCon tc_name binders res_kind tvs' (resultVariableName sig) AbstractClosedSynFamilyTyCon parent inj' Just eqns -> do { -- Process the equations, creating CoAxBranches - ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, kind) + ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, binders, res_kind) ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns -- Do not attempt to drop equations dominated by earlier @@ -800,7 +810,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) - fam_tc = mkFamilyTyCon tc_name kind tvs' (resultVariableName sig) + fam_tc = mkFamilyTyCon tc_name binders res_kind tvs' (resultVariableName sig) (ClosedSynFamilyTyCon mb_co_ax) parent inj' -- We check for instance validity later, when doing validity @@ -856,27 +866,27 @@ tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames))) tcTySynRhs :: RecTyInfo -> Name - -> [TyVar] -> Kind -> Kind + -> [TyVar] -> [TyBinder] -> Kind -> LHsType Name -> TcM TyCon -tcTySynRhs rec_info tc_name tvs full_kind res_kind hs_ty +tcTySynRhs rec_info tc_name tvs binders res_kind hs_ty = do { env <- getLclEnv ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env)) ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty ; let roles = rti_roles rec_info tc_name - tycon = mkSynonymTyCon tc_name full_kind tvs roles rhs_ty + tycon = mkSynonymTyCon tc_name binders res_kind tvs roles rhs_ty ; return tycon } tcDataDefn :: RecTyInfo -> Name - -> [TyVar] -> Kind -> Kind + -> [TyVar] -> [TyBinder] -> Kind -> HsDataDefn Name -> TcM TyCon -- NB: not used for newtype/data instances (whether associated or not) tcDataDefn rec_info -- Knot-tied; don't look at this eagerly - tc_name tvs tycon_kind res_kind + tc_name tvs tycon_binders res_kind (HsDataDefn { dd_ND = new_or_data, dd_cType = cType , dd_ctxt = ctxt, dd_kindSig = mb_ksig , dd_cons = cons }) - = do { extra_tvs <- tcDataKindSig res_kind + = do { (extra_tvs, extra_bndrs, real_res_kind) <- tcDataKindSig res_kind ; let final_tvs = tvs `chkAppend` extra_tvs roles = rti_roles rec_info tc_name @@ -897,7 +907,8 @@ tcDataDefn rec_info -- Knot-tied; don't look at this eagerly ; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons ; tc_rhs <- mk_tc_rhs is_boot tycon data_cons ; tc_rep_nm <- newTyConRepName tc_name - ; return (mkAlgTyCon tc_name tycon_kind final_tvs roles + ; return (mkAlgTyCon tc_name (tycon_binders `chkAppend` extra_bndrs) + real_res_kind final_tvs roles (fmap unLoc cType) stupid_theta tc_rhs (VanillaAlgTyCon tc_rep_nm) @@ -987,7 +998,7 @@ 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@(fam_tc_name, fam_arity, _, _) = famTyConShape fam_tc -- Kind of family check ; ASSERT( fam_tc_name == tc_name ) @@ -1053,7 +1064,7 @@ kcTyFamInstEqn fam_tc_shape tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInfo -> LTyFamInstEqn Name -> 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@(fam_tc_name,_,_,_) mb_clsinfo (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name , tfe_pats = pats , tfe_rhs = hs_ty })) @@ -1130,13 +1141,15 @@ two bad things could happen: -} ----------------- -type FamTyConShape = (Name, Arity, Kind) -- See Note [Type-checking type patterns] +type FamTyConShape = (Name, Arity, [TyBinder], Kind) + -- See Note [Type-checking type patterns] famTyConShape :: TyCon -> FamTyConShape famTyConShape fam_tc = ( tyConName fam_tc , length $ filterOutInvisibleTyVars fam_tc (tyConTyVars fam_tc) - , tyConKind fam_tc ) + , tyConBinders fam_tc + , tyConResKind fam_tc ) tc_fam_ty_pats :: FamTyConShape -> Maybe ClsInfo @@ -1155,21 +1168,24 @@ tc_fam_ty_pats :: FamTyConShape -- In that case, the type variable 'a' will *already be in scope* -- (and, if C is poly-kinded, so will its kind parameter). -tc_fam_ty_pats (name, _, kind) mb_clsinfo +tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo (HsIB { hsib_body = arg_pats, hsib_vars = tv_names }) kind_checker = do { -- Kind-check and quantify -- See Note [Quantifying over family patterns] - (_, (res_kind, typats)) <- tcImplicitTKBndrs tv_names $ - do { (res_kind, args, leftovers, n) - <- tcInferArgs name kind (snd <$> mb_clsinfo) arg_pats + (_, (insted_res_kind, typats)) <- tcImplicitTKBndrs tv_names $ + do { (insting_subst, _leftover_binders, args, leftovers, n) + <- tcInferArgs name binders (snd <$> mb_clsinfo) arg_pats ; case leftovers of hs_ty:_ -> addErrTc $ too_many_args hs_ty n _ -> return () - ; kind_checker res_kind - ; return ((res_kind, args), emptyVarSet) } + -- don't worry about leftover_binders; TcValidity catches them + + ; let insted_res_kind = substTyUnchecked insting_subst res_kind + ; kind_checker insted_res_kind + ; return ((insted_res_kind, args), emptyVarSet) } - ; return (typats, res_kind) } + ; return (typats, insted_res_kind) } where too_many_args hs_ty n = hang (text "Too many parameters to" <+> ppr name <> colon) @@ -1186,7 +1202,7 @@ tcFamTyPats :: FamTyConShape -> [TcType] -- Kind and type arguments -> Kind -> TcM a) -- NB: You can use solveEqualities here. -> TcM a -tcFamTyPats fam_shape@(name,_,_) mb_clsinfo pats kind_checker thing_inside +tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside = do { (typats, res_kind) <- solveEqualities $ -- See Note [Constraints in patterns] tc_fam_ty_pats fam_shape mb_clsinfo pats kind_checker |