diff options
Diffstat (limited to 'compiler/GHC/Tc/TyCl')
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Class.hs | 10 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Instance.hs | 39 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/PatSyn.hs | 104 |
3 files changed, 103 insertions, 50 deletions
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs index 92be85fa06..8e637a1a32 100644 --- a/compiler/GHC/Tc/TyCl/Class.hs +++ b/compiler/GHC/Tc/TyCl/Class.hs @@ -157,16 +157,14 @@ tcClassSigs clas sigs def_methods dm_bind_names :: [Name] -- These ones have a value binding in the class decl dm_bind_names = [op | L _ (FunBind {fun_id = L _ op}) <- bagToList def_methods] - skol_info = TyConSkol ClassFlavour clas - tc_sig :: NameEnv (SrcSpan, Type) -> ([Located Name], LHsSigType GhcRn) -> TcM [TcMethInfo] tc_sig gen_dm_env (op_names, op_hs_ty) = do { traceTc "ClsSig 1" (ppr op_names) - ; op_ty <- tcClassSigType skol_info op_names op_hs_ty + ; op_ty <- tcClassSigType op_names op_hs_ty -- Class tyvars already in scope - ; traceTc "ClsSig 2" (ppr op_names) + ; traceTc "ClsSig 2" (ppr op_names $$ ppr op_ty) ; return [ (op_name, op_ty, f op_name) | L _ op_name <- op_names ] } where f nm | Just lty <- lookupNameEnv gen_dm_env nm = Just (GenericDM lty) @@ -174,7 +172,7 @@ tcClassSigs clas sigs def_methods | otherwise = Nothing tc_gen_sig (op_names, gen_hs_ty) - = do { gen_op_ty <- tcClassSigType skol_info op_names gen_hs_ty + = do { gen_op_ty <- tcClassSigType op_names gen_hs_ty ; return [ (op_name, (loc, gen_op_ty)) | L loc op_name <- op_names ] } {- @@ -290,7 +288,7 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn ; let local_dm_id = mkLocalId local_dm_name Many local_dm_ty local_dm_sig = CompleteSig { sig_bndr = local_dm_id , sig_ctxt = ctxt - , sig_loc = getLoc (hsSigType hs_ty) } + , sig_loc = getLoc hs_ty } ; (ev_binds, (tc_bind, _)) <- checkConstraints skol_info tyvars [this_dict] $ diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index cc47d1e348..2c52a89248 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -531,7 +531,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds -- Finally, construct the Core representation of the instance. -- (This no longer includes the associated types.) - ; dfun_name <- newDFunName clas inst_tys (getLoc (hsSigType hs_ty)) + ; dfun_name <- newDFunName clas inst_tys (getLoc hs_ty) -- Dfun location is that of instance *header* ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name @@ -559,7 +559,6 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats) `unionNameSet` mkNameSet (map (unLoc . feqn_tycon - . hsib_body . dfid_eqn . unLoc) adts) @@ -583,7 +582,7 @@ tcTyFamInstDecl :: AssocInstInfo tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn })) = setSrcSpan loc $ tcAddTyFamInstCtxt decl $ - do { let fam_lname = feqn_tycon (hsib_body eqn) + do { let fam_lname = feqn_tycon eqn ; fam_tc <- tcLookupLocatedTyCon fam_lname ; tcFamInstDeclChecks mb_clsinfo fam_tc @@ -592,10 +591,11 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn })) ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc) -- (1) do the work of verifying the synonym group + -- For some reason we don't have a location for the equation + -- itself, so we make do with the location of family name ; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo (L (getLoc fam_lname) eqn) - -- (2) check for validity ; checkConsistentFamInst mb_clsinfo fam_tc co_ax_branch ; checkValidCoAxBranch fam_tc co_ax_branch @@ -665,9 +665,8 @@ tcDataFamInstDecl :: -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo) -- "newtype instance" and "data instance" tcDataFamInstDecl mb_clsinfo tv_skol_env - (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext = imp_vars - , hsib_body = - FamEqn { feqn_bndrs = mb_bndrs + (L loc decl@(DataFamInstDecl { dfid_eqn = + FamEqn { feqn_bndrs = outer_bndrs , feqn_pats = hs_pats , feqn_tycon = lfam_name@(L _ fam_name) , feqn_fixity = fixity @@ -676,7 +675,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env , dd_ctxt = hs_ctxt , dd_cons = hs_cons , dd_kindSig = m_ksig - , dd_derivs = derivs } }}})) + , dd_derivs = derivs } }})) = setSrcSpan loc $ tcAddDataFamInstCtxt decl $ do { fam_tc <- tcLookupLocatedTyCon lfam_name @@ -689,7 +688,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env -- Do /not/ check that the number of patterns = tyConArity fam_tc -- See [Arity of data families] in GHC.Core.FamInstEnv ; (qtvs, pats, res_kind, stupid_theta) - <- tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs + <- tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons new_or_data @@ -856,7 +855,7 @@ TyVarEnv will simply be empty, and there is nothing to worry about. ----------------------- tcDataFamInstHeader - :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr () GhcRn] + :: AssocInstInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn -> LexicalFixity -> LHsContext GhcRn -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn] -> NewOrData @@ -865,13 +864,12 @@ tcDataFamInstHeader -- the data constructors themselves -- e.g. data instance D [a] :: * -> * where ... -- Here the "header" is the bit before the "where" -tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity +tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons new_or_data = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats) - ; (tclvl, wanted, (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))) + ; (tclvl, wanted, (scoped_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind))) <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $ - bindImplicitTKBndrs_Q_Skol imp_vars $ - bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ + bindOuterFamEqnTKBndrs outer_bndrs $ do { stupid_theta <- tcHsContext hs_ctxt ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats ; (lhs_applied_ty, lhs_applied_kind) @@ -909,7 +907,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity -- check there too! -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts] - ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs)) + ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs) ; qtvs <- quantifyTyVars dvs ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted @@ -937,9 +935,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; return (qtvs, pats, master_res_kind, stupid_theta) } where - fam_name = tyConName fam_tc - data_ctxt = DataKindCtxt fam_name - exp_bndrs = mb_bndrs `orElse` [] + fam_name = tyConName fam_tc + data_ctxt = DataKindCtxt fam_name -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2). tc_kind_sig Nothing @@ -952,8 +949,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity -- See Note [Result kind signature for a data family instance] tc_kind_sig (Just hs_kind) = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind - ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind ; lvl <- getTcLevel + ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs -- Perhaps surprisingly, we don't need the skolemised tvs themselves ; return (substTy subst inner_kind) } @@ -1802,7 +1799,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind -- There is a signature in the instance -- See Note [Instance method signatures] = do { (sig_ty, hs_wrap) - <- setSrcSpan (getLoc (hsSigType hs_sig_ty)) $ + <- setSrcSpan (getLoc hs_sig_ty) $ do { inst_sigs <- xoptM LangExt.InstanceSigs ; checkTc inst_sigs (misplacedInstSig sel_name hs_sig_ty) ; sig_ty <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty @@ -1823,7 +1820,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind inner_meth_id = mkLocalId inner_meth_name Many sig_ty inner_meth_sig = CompleteSig { sig_bndr = inner_meth_id , sig_ctxt = ctxt - , sig_loc = getLoc (hsSigType hs_sig_ty) } + , sig_loc = getLoc hs_sig_ty } ; (tc_bind, [inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 014a5027a4..3f5b10f343 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -24,6 +24,7 @@ import GHC.Hs import GHC.Tc.Gen.Pat import GHC.Core.Multiplicity import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType ) +import GHC.Core.TyCo.Subst( extendTvSubstWithClone ) import GHC.Tc.Utils.Monad import GHC.Tc.Gen.Sig( emptyPragEnv, completeSigFromId ) import GHC.Tc.Utils.Env @@ -61,7 +62,7 @@ import GHC.Utils.Misc import GHC.Utils.Error import Data.Maybe( mapMaybe ) import Control.Monad ( zipWithM ) -import Data.List( partition ) +import Data.List( partition, mapAccumL ) #include "HsVersions.h" @@ -345,24 +346,24 @@ tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details , psb_def = lpat, psb_dir = dir } TPSI{ patsig_implicit_bndrs = implicit_bndrs - , patsig_univ_bndrs = explicit_univ_bndrs, patsig_prov = prov_theta - , patsig_ex_bndrs = explicit_ex_bndrs, patsig_req = req_theta + , patsig_univ_bndrs = explicit_univ_bndrs, patsig_req = req_theta + , patsig_ex_bndrs = explicit_ex_bndrs, patsig_prov = prov_theta , patsig_body_ty = sig_body_ty } = addPatSynCtxt lname $ - do { let decl_arity = length arg_names - (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details - - ; traceTc "tcCheckPatSynDecl" $ + do { traceTc "tcCheckPatSynDecl" $ vcat [ ppr implicit_bndrs, ppr explicit_univ_bndrs, ppr req_theta , ppr explicit_ex_bndrs, ppr prov_theta, ppr sig_body_ty ] + ; let decl_arity = length arg_names + (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details + ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of Right stuff -> return stuff Left missing -> wrongNumberOfParmsErr name decl_arity missing -- Complain about: pattern P :: () => forall x. x -> P x -- The existential 'x' should not appear in the result type - -- Can't check this until we know P's arity + -- Can't check this until we know P's arity (decl_arity above) ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) $ binderVars explicit_ex_bndrs ; checkTc (null bad_tvs) $ hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma @@ -379,36 +380,55 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details univ_tvs = binderVars univ_bndrs ex_tvs = binderVars ex_bndrs + -- Skolemise the quantified type variables. This is necessary + -- in order to check the actual pattern type against the + -- expected type. Even though the tyvars in the type are + -- already skolems, this step changes their TcLevels, + -- avoiding level-check errors when unifying. + ; (skol_subst0, skol_univ_bndrs) <- skolemiseTvBndrsX emptyTCvSubst univ_bndrs + ; (skol_subst, skol_ex_bndrs) <- skolemiseTvBndrsX skol_subst0 ex_bndrs + ; let skol_univ_tvs = binderVars skol_univ_bndrs + skol_ex_tvs = binderVars skol_ex_bndrs + skol_req_theta = substTheta skol_subst0 req_theta + skol_prov_theta = substTheta skol_subst prov_theta + skol_arg_tys = substTys skol_subst (map scaledThing arg_tys) + skol_pat_ty = substTy skol_subst pat_ty + + univ_tv_prs = [ (getName orig_univ_tv, skol_univ_tv) + | (orig_univ_tv, skol_univ_tv) <- univ_tvs `zip` skol_univ_tvs ] + -- Right! Let's check the pattern against the signature -- See Note [Checking against a pattern signature] - ; req_dicts <- newEvVars req_theta + ; req_dicts <- newEvVars skol_req_theta ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <- ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys ) pushLevelAndCaptureConstraints $ - tcExtendTyVarEnv univ_tvs $ - tcCheckPat PatSyn lpat (unrestricted pat_ty) $ - do { let in_scope = mkInScopeSet (mkVarSet univ_tvs) + tcExtendNameTyVarEnv univ_tv_prs $ + tcCheckPat PatSyn lpat (unrestricted skol_pat_ty) $ + do { let in_scope = mkInScopeSet (mkVarSet skol_univ_tvs) empty_subst = mkEmptyTCvSubst in_scope - ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs + ; (inst_subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst skol_ex_tvs -- newMetaTyVarX: see the "Existential type variables" -- part of Note [Checking against a pattern signature] ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs]) ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs']) - ; let prov_theta' = substTheta subst prov_theta + ; let prov_theta' = substTheta inst_subst skol_prov_theta -- Add univ_tvs to the in_scope set to -- satisfy the substitution invariant. There's no need to -- add 'ex_tvs' as they are already in the domain of the -- substitution. -- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst. ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta' - ; args' <- zipWithM (tc_arg subst) arg_names (map scaledThing arg_tys) + ; args' <- zipWithM (tc_arg inst_subst) arg_names + skol_arg_tys ; return (ex_tvs', prov_dicts, args') } ; let skol_info = SigSkol (PatSynCtxt name) pat_ty [] -- The type here is a bit bogus, but we do not print -- the type for PatSynCtxt, so it doesn't matter -- See Note [Skolem info for pattern synonyms] in "GHC.Tc.Types.Origin" - ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted + ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_univ_tvs + req_dicts wanted -- Solve the constraints now, because we are about to make a PatSyn, -- which should not contain unification variables and the like (#10997) @@ -419,11 +439,12 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details -- when that should be impossible ; traceTc "tcCheckPatSynDecl }" $ ppr name + ; tc_patsyn_finish lname dir is_infix lpat' - (univ_bndrs, req_theta, ev_binds, req_dicts) - (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts) - (args', map scaledThing arg_tys) - pat_ty rec_fields } + (skol_univ_bndrs, skol_req_theta, ev_binds, req_dicts) + (skol_ex_bndrs, mkTyVarTys ex_tvs', skol_prov_theta, prov_dicts) + (args', skol_arg_tys) + skol_pat_ty rec_fields } where tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTc) -- Look up the variable actually bound by lpat @@ -440,13 +461,50 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details do { arg_id <- tcLookupId arg_name ; wrap <- tcSubTypeSigma GenSigCtxt (idType arg_id) - (substTyUnchecked subst arg_ty) + (substTy subst arg_ty) -- Why do we need tcSubType here? -- See Note [Pattern synonyms and higher rank types] ; return (mkLHsWrap wrap $ nlHsVar arg_id) } -{- [Pattern synonyms and higher rank types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +skolemiseTvBndrsX :: TCvSubst -> [VarBndr TyVar flag] + -> TcM (TCvSubst, [VarBndr TcTyVar flag]) +-- Make new TcTyVars, all skolems with levels, but do not clone +-- The level is one level deeper than the current level +-- See Note [Skolemising when checking a pattern synonym] +skolemiseTvBndrsX orig_subst tvs + = do { tc_lvl <- getTcLevel + ; let pushed_lvl = pushTcLevel tc_lvl + details = SkolemTv pushed_lvl False + + mk_skol_tv_x :: TCvSubst -> VarBndr TyVar flag + -> (TCvSubst, VarBndr TcTyVar flag) + mk_skol_tv_x subst (Bndr tv flag) + = (subst', Bndr new_tv flag) + where + new_kind = substTyUnchecked subst (tyVarKind tv) + new_tv = mkTcTyVar (tyVarName tv) new_kind details + subst' = extendTvSubstWithClone subst tv new_tv + + ; return (mapAccumL mk_skol_tv_x orig_subst tvs) } + +{- Note [Skolemising when checking a pattern synonym] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + pattern P1 :: forall a. a -> Maybe a + pattern P1 x <- Just x where + P1 x = Just (x :: a) + +The scoped type variable 'a' scopes over the builder RHS, Just (x::a). +But the builder RHS is typechecked much later in tcPatSynBuilderBind, +and gets its scoped type variables from the type of the builder_id. +The easiest way to achieve this is not to clone when skolemising. + +Hence a special-purpose skolemiseTvBndrX here, similar to +GHC.Tc.Utils.Instantiate.tcInstSkolTyVarsX except that the latter +does cloning. + +[Pattern synonyms and higher rank types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider data T = MkT (forall a. a->a) |