diff options
23 files changed, 419 insertions, 245 deletions
diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs index b7aff18534..c35bcf3e13 100644 --- a/compiler/basicTypes/PatSyn.hs +++ b/compiler/basicTypes/PatSyn.hs @@ -159,8 +159,8 @@ so pattern P has type with the following typeclass constraints: - provides: (Show (Maybe t), Ord b) requires: (Eq t, Num t) + provides: (Show (Maybe t), Ord b) In this case, the fields of MkPatSyn will be set as follows: diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index f71c904454..502610fa0d 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -606,7 +606,7 @@ instTyVars :: [TyVar] -> TR (TCvSubst, [TcTyVar]) -- Instantiate fresh mutable type variables from some TyVars -- This function preserves the print-name, which helps error messages instTyVars tvs - = liftTcM $ fst <$> captureConstraints (tcInstTyVars tvs) + = liftTcM $ fst <$> captureConstraints (newMetaTyVars tvs) type RttiInstantiation = [(TcTyVar, TyVar)] -- Associates the typechecker-world meta type variables diff --git a/compiler/hsSyn/HsBinds.hs b/compiler/hsSyn/HsBinds.hs index 71d8dd2ed2..6acac76af6 100644 --- a/compiler/hsSyn/HsBinds.hs +++ b/compiler/hsSyn/HsBinds.hs @@ -892,13 +892,8 @@ ppr_sig (SpecInstSig _ ty) = pragBrackets (ptext (sLit "SPECIALIZE instance") <+> ppr ty) ppr_sig (MinimalSig _ bf) = pragBrackets (pprMinimalSig bf) ppr_sig (PatSynSig name sig_ty) - = pprPatSynSig (unLoc name) False -- TODO: is_bindir - (pprHsForAllTvs qtvs) - (pprHsContextMaybe (unLoc req)) - (pprHsContextMaybe (unLoc prov)) - (ppr ty) - where - (qtvs, req, prov, ty) = splitLHsPatSynTy (hsSigType sig_ty) + = ptext (sLit "pattern") <+> pprPrefixOcc (unLoc name) <+> dcolon + <+> ppr sig_ty pprPatSynSig :: (OutputableBndr name) => name -> Bool -> SDoc -> Maybe SDoc -> Maybe SDoc -> SDoc -> SDoc diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y index 2b4e779db6..be36b4ee2b 100644 --- a/compiler/parser/Parser.y +++ b/compiler/parser/Parser.y @@ -1191,29 +1191,10 @@ where_decls :: { Located ([AddAnn] ,sL1 $3 (snd $ unLoc $3)) } pattern_synonym_sig :: { LSig RdrName } - : 'pattern' con '::' ptype + : 'pattern' con '::' sigtype {% ams (sLL $1 $> $ PatSynSig $2 (mkLHsSigType $4)) [mj AnnPattern $1, mu AnnDcolon $3] } -ptype :: { LHsType RdrName } - : 'forall' tv_bndrs '.' ptype - {% hintExplicitForall (getLoc $1) >> - ams (sLL $1 $> $ - HsForAllTy { hst_bndrs = $2 - , hst_body = $4 }) - [mu AnnForall $1, mj AnnDot $3] } - - | context '=>' context '=>' type - {% ams (sLL $1 $> $ - HsQualTy { hst_ctxt = $1, hst_body = sLL $3 $> $ - HsQualTy { hst_ctxt = $3, hst_body = $5 } }) - [mu AnnDarrow $2, mu AnnDarrow $4] } - | context '=>' type - {% ams (sLL $1 $> $ - HsQualTy { hst_ctxt = $1, hst_body = $3 }) - [mu AnnDarrow $2] } - | type { $1 } - ----------------------------------------------------------------------------- -- Nested declarations diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index fba320c564..50c28db510 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -157,7 +157,7 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) deeplyInstantiate orig ty | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty - = do { (subst, tvs') <- tcInstTyVars tvs + = do { (subst, tvs') <- newMetaTyVars tvs ; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys) ; let theta' = substTheta subst theta ; wrap1 <- instCall orig (mkTyVarTys tvs') theta' @@ -248,7 +248,7 @@ instDFunType dfun_id dfun_inst_tys = do { (subst', tys) <- go (extendTCvSubst subst tv ty) tvs mb_tys ; return (subst', ty : tys) } go subst (tv:tvs) (Nothing : mb_tys) - = do { (subst', tv') <- tcInstTyVarX subst tv + = do { (subst', tv') <- newMetaTyVarX subst tv ; (subst'', tys) <- go subst' tvs mb_tys ; return (subst'', mkTyVarTy tv' : tys) } go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr dfun_inst_tys) diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index 56751d5349..be60056b4b 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -19,7 +19,8 @@ module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds, import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun ) import {-# SOURCE #-} TcExpr ( tcMonoExpr ) -import {-# SOURCE #-} TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl, tcPatSynBuilderBind ) +import {-# SOURCE #-} TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl + , tcPatSynBuilderBind, tcPatSynSig ) import DynFlags import HsSyn import HscTypes( isHsBootOrSig ) @@ -63,7 +64,6 @@ import TcValidity (checkValidType) import qualified GHC.LanguageExtensions as LangExt import Control.Monad -import Data.List (partition) #include "HsVersions.h" @@ -1684,46 +1684,8 @@ tcTySig (L loc (TypeSig names sig_ty)) ; return (map TcIdSig sigs) } tcTySig (L loc (PatSynSig (L _ name) sig_ty)) - | HsIB { hsib_vars = sig_vars - , hsib_body = hs_ty } <- sig_ty - , (tv_bndrs, req, prov, body_ty) <- splitLHsPatSynTy hs_ty = setSrcSpan loc $ - do { (tvs1, (req', prov', ty', tvs2)) - <- tcImplicitTKBndrs sig_vars $ - tcHsTyVarBndrs tv_bndrs $ \ tvs2 -> - do { req' <- tcHsContext req - ; prov' <- tcHsContext prov - ; ty' <- tcHsLiftedType body_ty - ; let bound_tvs - = unionVarSets [ allBoundVariabless req' - , allBoundVariabless prov' - , allBoundVariables ty' ] - ; return ((req', prov', ty', tvs2), bound_tvs) } - - -- These are /signatures/ so we zonk to squeeze out any kind - -- unification variables. ToDo: checkValidType? - ; qtvs' <- mapMaybeM zonkQuantifiedTyVar (tvs1 ++ tvs2) - ; req' <- zonkTcTypes req' - ; prov' <- zonkTcTypes prov' - ; ty' <- zonkTcType ty' - - ; let (_, pat_ty) = tcSplitFunTys ty' - univ_set = tyCoVarsOfType pat_ty - (univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs' - bad_tvs = varSetElems (tyCoVarsOfTypes req' `minusVarSet` univ_set) - - ; unless (null bad_tvs) $ addErr $ - hang (ptext (sLit "The 'required' context") <+> quotes (pprTheta req')) - 2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs - <+> pprQuotedList bad_tvs) - - ; traceTc "tcTySig }" $ ppr (ex_tvs, prov') $$ ppr (univ_tvs, req') $$ ppr ty' - ; let tpsi = TPSI{ patsig_name = name, - patsig_tau = ty', - patsig_ex = ex_tvs, - patsig_univ = univ_tvs, - patsig_prov = prov', - patsig_req = req' } + do { tpsi <- tcPatSynSig name sig_ty ; return [TcPatSynSig tpsi] } tcTySig _ = return [] diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 008b933e47..f299e9da9b 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -842,15 +842,15 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty mk_inst_ty :: TCvSubst -> (TyVar, TcType) -> TcM (TCvSubst, TcType) -- Deals with instantiation of kind variables - -- c.f. TcMType.tcInstTyVars + -- c.f. TcMType.newMetaTyVars mk_inst_ty subst (tv, result_inst_ty) | is_fixed_tv tv -- Same as result type = return (extendTCvSubst subst tv result_inst_ty, result_inst_ty) | otherwise -- Fresh type, of correct kind - = do { (subst', new_tv) <- tcInstTyVarX subst tv + = do { (subst', new_tv) <- newMetaTyVarX subst tv ; return (subst', mkTyVarTy new_tv) } - ; (result_subst, con1_tvs') <- tcInstTyVars con1_tvs + ; (result_subst, con1_tvs') <- newMetaTyVars con1_tvs ; let result_inst_tys = mkTyVarTys con1_tvs' ; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty emptyTCvSubst @@ -1327,7 +1327,7 @@ tc_infer_id orig lbl id_name -- * No need to deeply instantiate because type has all foralls at top = do { let wrap_id = dataConWrapId con (tvs, theta, rho) = tcSplitSigmaTy (idType wrap_id) - ; (subst, tvs') <- tcInstTyVars tvs + ; (subst, tvs') <- newMetaTyVars tvs ; let tys' = mkTyVarTys tvs' theta' = substTheta subst theta rho' = substTy subst rho diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index c7b208e80c..5ba86e12a9 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -827,7 +827,7 @@ tcInstBinderX mb_kind_info subst binder | Just tv <- binderVar_maybe binder = case lookup_tv tv of Just ki -> return (extendTCvSubst subst tv ki, ki) - Nothing -> do { (subst', tv') <- tcInstTyVarX subst tv + Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv ; return (subst', mkTyVarTy tv') } -- This is the *only* constraint currently handled in types. @@ -2055,7 +2055,7 @@ Here * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt - * Then unificaiton makes a_sig := a_sk + * Then unification makes a_sig := a_sk That's why we must make a_sig a MetaTv (albeit a SigTv), not a SkolemTv, so that it can unify to a_sk. diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index b0776f64e3..9285f9ae22 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -27,7 +27,7 @@ module TcMType ( cloneMetaTyVar, newFmvTyVar, newFskTyVar, - newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, + readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- @@ -47,7 +47,7 @@ module TcMType ( -------------------------------- -- Instantiation - tcInstTyVars, tcInstTyVarX, + newMetaTyVars, newMetaTyVarX, newMetaSigTyVars, newSigTyVar, tcInstType, tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX, @@ -437,19 +437,6 @@ mkMetaTyVarName :: Unique -> FastString -> Name -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2) mkMetaTyVarName uniq str = mkSysTvName uniq str -newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar --- Make a new meta tyvar out of thin air -newMetaTyVar meta_info kind - = do { uniq <- newUnique - ; let name = mkMetaTyVarName uniq s - s = case meta_info of - ReturnTv -> fsLit "r" - TauTv -> fsLit "t" - FlatMetaTv -> fsLit "fmv" - SigTv -> fsLit "a" - ; details <- newMetaDetails meta_info - ; return (mkTcTyVar name kind details) } - newSigTyVar :: Name -> Kind -> TcM TcTyVar newSigTyVar name kind = do { details <- newMetaDetails SigTv @@ -615,8 +602,21 @@ coercion variables, except for the special case of the promoted Eq#. But, that can't ever appear in user code, so we're safe! -} +newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar +-- Make a new meta tyvar out of thin air +newAnonMetaTyVar meta_info kind + = do { uniq <- newUnique + ; let name = mkMetaTyVarName uniq s + s = case meta_info of + ReturnTv -> fsLit "r" + TauTv -> fsLit "t" + FlatMetaTv -> fsLit "fmv" + SigTv -> fsLit "a" + ; details <- newMetaDetails meta_info + ; return (mkTcTyVar name kind details) } + newFlexiTyVar :: Kind -> TcM TcTyVar -newFlexiTyVar kind = newMetaTyVar TauTv kind +newFlexiTyVar kind = newAnonMetaTyVar TauTv kind newFlexiTyVarTy :: Kind -> TcM TcType newFlexiTyVarTy kind = do @@ -627,7 +627,7 @@ newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) newReturnTyVar :: Kind -> TcM TcTyVar -newReturnTyVar kind = newMetaTyVar ReturnTv kind +newReturnTyVar kind = newAnonMetaTyVar ReturnTv kind newReturnTyVarTy :: Kind -> TcM TcType newReturnTyVarTy kind = mkTyVarTy <$> newReturnTyVar kind @@ -652,20 +652,23 @@ newOpenReturnTyVar ; tv <- newReturnTyVar k ; return (tv, k) } -tcInstTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) +newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) +newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst + +newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Instantiate with META type variables -- Note that this works for a sequence of kind, type, and coercion variables -- variables. Eg [ (k:*), (a:k->k) ] -- Gives [ (k7:*), (a8:k7->k7) ] -tcInstTyVars = mapAccumLM tcInstTyVarX emptyTCvSubst +newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst -- emptyTCvSubst has an empty in-scope set, but that's fine here -- Since the tyvars are freshly made, they cannot possibly be -- captured by any existing for-alls. -tcInstTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) +newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) -- Make a new unification variable tyvar whose Name and Kind come from -- an existing TyVar. We substitute kind variables in the kind. -tcInstTyVarX subst tyvar +newMetaTyVarX subst tyvar = do { uniq <- newUnique -- See Note [Levity polymorphic variables accept foralls] ; let info = if isLevityPolymorphic (tyVarKind tyvar) @@ -678,6 +681,16 @@ tcInstTyVarX subst tyvar new_tv = mkTcTyVar name kind details ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) } +newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) +-- Just like newMetaTyVarX, but make a SigTv +newMetaSigTyVarX subst tyvar + = do { uniq <- newUnique + ; details <- newMetaDetails SigTv + ; let name = mkSystemName uniq (getOccName tyvar) + kind = substTy subst (tyVarKind tyvar) + new_tv = mkTcTyVar name kind details + ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) } + {- Note [Name of an instantiated type variable] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At the moment we give a unification variable a System Name, which diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index f76da5b0d5..b951ad2197 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -706,7 +706,7 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside = do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn - ; (subst, univ_tvs') <- tcInstTyVars univ_tvs + ; (subst, univ_tvs') <- newMetaTyVars univ_tvs ; let all_arg_tys = ty : prov_theta ++ arg_tys ; checkExistentials ex_tvs all_arg_tys penv @@ -776,7 +776,7 @@ matchExpectedPatTy inner_match pat_ty -- that is the other way round to matchExpectedPatTy | otherwise - = do { (subst, tvs') <- tcInstTyVars tvs + = do { (subst, tvs') <- newMetaTyVars tvs ; wrap1 <- instCall PatOrigin (mkTyVarTys tvs') (substTheta subst theta) ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau) ; return (wrap2 <.> wrap1, arg_tys) } @@ -800,7 +800,7 @@ matchExpectedConTy data_tc pat_ty | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc -- Comments refer to Note [Matching constructor patterns] -- co_tc :: forall a. T [a] ~ T7 a - = do { (subst, tvs') <- tcInstTyVars (tyConTyVars data_tc) + = do { (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc) -- tys = [ty1,ty2] ; traceTc "matchExpectedConTy" (vcat [ppr data_tc, diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 61b54fdb18..d7477eeb0d 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -7,19 +7,20 @@ {-# LANGUAGE CPP #-} -module TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl +module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr ) where import HsSyn import TcPat +import TcHsType( tcImplicitTKBndrs, tcHsTyVarBndrs + , tcHsContext, tcHsLiftedType, tcHsOpenType ) import TcRnMonad import TcEnv import TcMType import TysPrim import TysWiredIn ( levityTy ) import Name -import Coercion ( emptyCvSubstEnv ) import SrcLoc import PatSyn import NameSet @@ -38,21 +39,141 @@ import TcEvidence import BuildTyCl import VarSet import MkId -import VarEnv import Inst import TcTyDecls import ConLike import FieldLabel #if __GLASGOW_HASKELL__ < 709 -import Data.Monoid +import Data.Monoid( mconcat, mappend, mempty ) #endif import Bag import Util import Data.Maybe -import Control.Monad (forM) +import Control.Monad ( unless, zipWithM ) +import Data.List( partition ) +import Pair( Pair(..) ) #include "HsVersions.h" +{- ********************************************************************* +* * + Type checking a pattern synonym signature +* * +************************************************************************ + +Note [Pattern synonym signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example). +In general they look like this: + + pattern P :: forall univ_tvs. req + => forall ex_tvs. prov + => arg1 -> .. -> argn -> body_ty + +For parsing and renaming we treat the signature as an ordinary LHsSigType. + +Once we get to type checking, we decompose it into its parts, in tcPatSynSig. + +* Note that 'forall univ_tvs' and 'req =>' + and 'forall ex_tvs' and 'prov =>' + are all optional. We gather the pieces at the the top of tcPatSynSig + +* Initially the implicitly-bound tyvars (added by the renamer) include both + universal and existential vars. + +* After we kind-check the pieces and convert to Types, we do kind generalisation. + +* Note [Splitting the implicit tyvars in a pattern synonym] + Now the tricky bit: we must split + the implicitly-bound variables, and + the kind-generalised variables + into universal and existential. We do so as follows: + + Note [The pattern-synonym signature splitting rule] + the universals are the ones mentioned in + - univ_tvs (and the kinds thereof) + - prov + - body_ty + the existential are the rest + +* Moreover see Note +-} + +tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo +tcPatSynSig name sig_ty + | HsIB { hsib_vars = implicit_hs_tvs + , hsib_body = hs_ty } <- sig_ty + , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty + , (ex_hs_tvs, hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1 + , (hs_arg_tys, hs_body_ty) <- splitHsFunType hs_ty2 + = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)) + <- solveEqualities $ + tcImplicitTKBndrs implicit_hs_tvs $ + tcHsTyVarBndrs univ_hs_tvs $ \ univ_tvs -> + tcHsTyVarBndrs ex_hs_tvs $ \ ex_tvs -> + do { req <- tcHsContext hs_req + ; prov <- tcHsContext hs_prov + ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name]) + ; body_ty <- tcHsLiftedType hs_body_ty + ; let bound_tvs + = unionVarSets [ allBoundVariabless req + , allBoundVariabless prov + , allBoundVariabless (body_ty : arg_tys) + ] + ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty) + , bound_tvs) } + + -- These are /signatures/ so we zonk to squeeze out any kind + -- unification variables. + -- ToDo: checkValidType? + ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs + ; univ_tvs <- mapM zonkTcTyCoVarBndr univ_tvs + ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs + ; req <- zonkTcTypes req + ; prov <- zonkTcTypes prov + ; arg_tys <- zonkTcTypes arg_tys + ; body_ty <- zonkTcType body_ty + + -- Kind generalisation; c.f. kindGeneralise + ; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $ + tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys) + + ; kvs <- quantifyTyVars emptyVarSet (Pair free_kvs emptyVarSet) + + -- Complain about: pattern P :: () => forall x. x -> P x + -- The renamer thought it was fine, but the existential 'x' + -- should not appear in the result type + ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs + ; unless (null bad_tvs) $ addErr $ + hang (ptext (sLit "The result type") <+> quotes (ppr body_ty)) + 2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs + <+> pprQuotedList bad_tvs) + + -- Split [Splitting the implicit tyvars in a pattern synonym] + ; let univ_fvs = closeOverKinds $ + (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs) + (extra_univ, extra_ex) = partition (`elemVarSet` univ_fvs) $ + kvs ++ implicit_tvs + ; traceTc "tcTySig }" $ + vcat [ text "implicit_tvs" <+> ppr implicit_tvs + , text "kvs" <+> ppr kvs + , text "extra_univ" <+> ppr extra_univ + , text "univ_tvs" <+> ppr univ_tvs + , text "req" <+> ppr req + , text "extra_ex" <+> ppr extra_ex + , text "ex_tvs_" <+> ppr ex_tvs + , text "prov" <+> ppr prov + , text "arg_tys" <+> ppr arg_tys + , text "body_ty" <+> ppr body_ty ] + ; return (TPSI { patsig_name = name + , patsig_univ_tvs = extra_univ ++ univ_tvs + , patsig_req = req + , patsig_ex_tvs = extra_ex ++ ex_tvs + , patsig_prov = prov + , patsig_arg_tys = arg_tys + , patsig_body_ty = body_ty }) } + + {- ************************************************************************ * * @@ -63,9 +184,9 @@ import Control.Monad (forM) tcInferPatSynDecl :: PatSynBind Name Name -> TcM (LHsBinds Id, TcGblEnv) -tcInferPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details, +tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, psb_def = lpat, psb_dir = dir } - = setSrcSpan loc $ + = addPatSynCtxt lname $ do { traceTc "tcInferPatSynDecl {" $ ppr name ; tcCheckPatSynPat lpat @@ -81,93 +202,136 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details, ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted - ; (ex_vars, prov_dicts) <- tcCollectEx lpat' - ; let univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs + ; let (ex_vars, prov_dicts) = tcCollectEx lpat' + univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs ex_tvs = varSetElems ex_vars prov_theta = map evVarPred prov_dicts req_theta = map evVarPred req_dicts ; traceTc "tcInferPatSynDecl }" $ ppr name ; tc_patsyn_finish lname dir is_infix lpat' - (univ_tvs, req_theta, ev_binds, req_dicts) - (ex_tvs, mkTyVarTys ex_tvs, prov_theta, emptyTcEvBinds, map EvId prov_dicts) - (zip args $ repeat idHsWrapper) + (univ_tvs, req_theta, ev_binds, req_dicts) + (ex_tvs, mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts) + (map nlHsVar args, map idType args) pat_ty rec_fields } tcCheckPatSynDecl :: PatSynBind Name Name -> TcPatSynInfo -> TcM (LHsBinds Id, TcGblEnv) -tcCheckPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details, - psb_def = lpat, psb_dir = dir } - TPSI{ patsig_tau = tau, - patsig_ex = ex_tvs, patsig_univ = univ_tvs, - patsig_prov = prov_theta, patsig_req = req_theta } - = setSrcSpan loc $ - do { traceTc "tcCheckPatSynDecl" $ - ppr (ex_tvs, prov_theta) $$ - ppr (univ_tvs, req_theta) $$ - ppr arg_tys $$ - ppr tau +tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details + , psb_def = lpat, psb_dir = dir } + TPSI{ patsig_univ_tvs = univ_tvs, patsig_prov = prov_theta + , patsig_ex_tvs = ex_tvs, patsig_req = req_theta + , patsig_arg_tys = arg_tys, patsig_body_ty = pat_ty } + = addPatSynCtxt lname $ + do { let origin = PatOrigin -- TODO + skol_info = SigSkol (PatSynCtxt name) (mkFunTys arg_tys pat_ty) + decl_arity = length arg_names + ty_arity = length arg_tys + (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details + + ; traceTc "tcCheckPatSynDecl" $ + vcat [ ppr univ_tvs, ppr req_theta, ppr ex_tvs + , ppr prov_theta, ppr arg_tys, ppr pat_ty ] + + ; checkTc (decl_arity == ty_arity) + (wrongNumberOfParmsErr name decl_arity ty_arity) + ; tcCheckPatSynPat lpat + -- Right! Let's check the pattern against the signature + -- See Note [Checking against a pattern signature] ; req_dicts <- newEvVars req_theta - - -- TODO: find a better SkolInfo - ; let skol_info = SigSkol (PatSynCtxt name) (mkFunTys arg_tys pat_ty) - - ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details - - ; let ty_arity = length arg_tys - ; checkTc (length arg_names == ty_arity) - (wrongNumberOfParmsErr ty_arity) - - -- Typecheck the pattern against pat_ty, then unify the type of args - -- against arg_tys, with ex_tvs changed to SigTyVars. - -- We get out of this: - -- * The evidence bindings for the requested theta: req_ev_binds - -- * The typechecked pattern: lpat' - -- * The arguments, type-coerced to the SigTyVars: wrapped_args - -- * The instantiation of ex_tvs to pass to the success continuation: ex_tys - -- * The provided theta substituted with the SigTyVars: prov_theta' - ; (implic1, req_ev_binds, (lpat', (ex_tys, prov_theta', wrapped_args))) <- - buildImplication skol_info univ_tvs req_dicts $ - tcPat PatSyn lpat pat_ty $ do - { ex_sigtvs <- mapM (\tv -> newSigTyVar (getName tv) (tyVarKind tv)) ex_tvs - ; let subst = mkTCvSubst (mkInScopeSet (zipVarEnv ex_sigtvs ex_sigtvs)) $ - ( zipTyEnv ex_tvs (mkTyVarTys ex_sigtvs) - , emptyCvSubstEnv ) - ; let ex_tys = substTys subst $ mkTyVarTys ex_tvs - prov_theta' = substTheta subst prov_theta - ; wrapped_args <- forM (zipEqual "tcCheckPatSynDecl" arg_names arg_tys) $ \(arg_name, arg_ty) -> do - { arg <- tcLookupId arg_name - ; let arg_ty' = substTy subst arg_ty - ; coi <- unifyType (Just arg) (varType arg) arg_ty' - ; return (setVarType arg arg_ty, mkWpCastN coi) } - ; return (ex_tys, prov_theta', wrapped_args) } - - ; (ex_vars_rhs, prov_dicts_rhs) <- tcCollectEx lpat' - ; let ex_tvs_rhs = varSetElems ex_vars_rhs - - -- Check that prov_theta' can be satisfied with the dicts from the pattern - ; (implic2, prov_ev_binds, prov_dicts) <- - buildImplication skol_info ex_tvs_rhs prov_dicts_rhs $ do - { let origin = PatOrigin -- TODO - ; mapM (emitWanted origin) prov_theta' } + ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <- + ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys ) + pushLevelAndCaptureConstraints $ + tcPat PatSyn lpat pat_ty $ + do { (subst, ex_tvs') <- if isUnidirectional dir + then newMetaTyVars ex_tvs + else newMetaSigTyVars ex_tvs + -- See the "Existential type variables part of + -- Note [Checking against a pattern signature] + ; prov_dicts <- mapM (emitWanted origin) (substTheta subst prov_theta) + ; args' <- zipWithM (tc_arg subst) arg_names arg_tys + ; return (ex_tvs', prov_dicts, args') } + + ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info 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 (Trac #10997) -- Since all the inputs are implications the returned bindings will be empty - ; _ <- simplifyTop (emptyWC `addImplics` (implic1 `unionBags` implic2)) + ; _ <- simplifyTop (emptyWC `addImplics` implics) + + -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct + -- Otherwise we may get a type error when typechecking the builder, + -- when that should be impossible ; traceTc "tcCheckPatSynDecl }" $ ppr name ; tc_patsyn_finish lname dir is_infix lpat' - (univ_tvs, req_theta, req_ev_binds, req_dicts) - (ex_tvs, ex_tys, prov_theta, prov_ev_binds, prov_dicts) - wrapped_args + (univ_tvs, req_theta, ev_binds, req_dicts) + (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts) + (args', arg_tys) pat_ty rec_fields } where - (arg_tys, pat_ty) = tcSplitFunTys tau + tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId) + tc_arg subst arg_name arg_ty + = do { -- Look up the variable actually bound by lpat + -- and check that it has the expected type + arg_id <- tcLookupId arg_name + ; coi <- unifyType (Just arg_id) + (idType arg_id) + (substTy subst arg_ty) + ; return (mkLHsWrapCo coi $ nlHsVar arg_id) } + +{- Note [Checking against a pattern signature] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When checking the actual supplied pattern against the pattern synonym +signature, we need to be quite careful. + +----- Provided constraints +Example + + data T a where + MkT :: Ord a => a -> T a + + pattern P :: () => Eq a => a -> [T a] + pattern P x = [MkT x] + +We must check that the (Eq a) that P claims to bind (and to +make available to matches against P, is derivable from the +acutal pattern. For example: + f (P (x::a)) = ...here (Eq a) should be available... +And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs. + +----- Existential type variables +Unusually, we instantiate the existential tyvars of the pattern with +*meta* type variables. For example + + data S where + MkS :: Eq a => [a] -> S + + pattern P :: () => Eq x => x -> S + pattern P x <- MkS x + +The pattern synonym conceals from its client the fact that MkS has a +list inside it. The client just thinks it's a type 'x'. So we must +unify x := [a] during type checking, and then use the instantiating type +[a] (called ex_tys) when building the matcher. In this case we'll get + + $mP :: S -> (forall x. Ex x => x -> r) -> r -> r + $mP x k = case x of + MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a] + dl = $dfunEqList d + in k [a] dl ys + +This "concealing" story works for /uni-directional/ pattern synonmys, +but obviously not for bidirectional ones. So in the bidirectional case +we use SigTv, rather than a generic TauTv, meta-tyvar so that. And +we should really check that those SigTvs don't get unified with each +other. + +-} collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool) collectPatSynArgInfo details = @@ -184,10 +348,18 @@ collectPatSynArgInfo details = , recordPatSynSelectorId = L _ selId }) = (patVar, selId) -wrongNumberOfParmsErr :: Arity -> SDoc -wrongNumberOfParmsErr ty_arity - = ptext (sLit "Number of pattern synonym arguments doesn't match type; expected") - <+> ppr ty_arity +addPatSynCtxt :: Located Name -> TcM a -> TcM a +addPatSynCtxt (L loc name) thing_inside + = setSrcSpan loc $ + addErrCtxt (ptext (sLit "In the declaration for pattern synonym") + <+> quotes (ppr name)) $ + thing_inside + +wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc +wrongNumberOfParmsErr name decl_arity ty_arity + = hang (ptext (sLit "Patten synonym") <+> quotes (ppr name) <+> ptext (sLit "has") + <+> speakNOf decl_arity (ptext (sLit "argument"))) + 2 (ptext (sLit "but its type signature has") <+> speakN ty_arity) ------------------------- -- Shared by both tcInferPatSyn and tcCheckPatSyn @@ -196,16 +368,16 @@ tc_patsyn_finish :: Located Name -- ^ PatSyn Name -> Bool -- ^ Whether infix -> LPat Id -- ^ Pattern of the PatSyn -> ([TcTyVar], [PredType], TcEvBinds, [EvVar]) - -> ([TcTyVar], [TcType], [PredType], TcEvBinds, [EvTerm]) - -> [(Var, HsWrapper)] -- ^ Pattern arguments + -> ([TcTyVar], [TcType], [PredType], [EvTerm]) + -> ([LHsExpr TcId], [TcType]) -- ^ Pattern arguments and types -> TcType -- ^ Pattern type -> [Name] -- ^ Selector names -- ^ Whether fields, empty if not record PatSyn -> TcM (LHsBinds Id, TcGblEnv) tc_patsyn_finish lname dir is_infix lpat' (univ_tvs, req_theta, req_ev_binds, req_dicts) - (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts) - wrapped_args + (ex_tvs, ex_tys, prov_theta, prov_dicts) + (args, arg_tys) pat_ty field_labels = do { -- Zonk everything. We are about to build a final PatSyn -- so there had better be no unification variables in there @@ -214,26 +386,26 @@ tc_patsyn_finish lname dir is_infix lpat' ; prov_theta <- zonkTcTypes prov_theta ; req_theta <- zonkTcTypes req_theta ; pat_ty <- zonkTcType pat_ty - ; wrapped_args <- mapM zonk_wrapped_arg wrapped_args + ; arg_tys <- zonkTcTypes arg_tys ; let qtvs = univ_tvs ++ ex_tvs -- See Note [Record PatSyn Desugaring] theta = prov_theta ++ req_theta - arg_tys = map (varType . fst) wrapped_args ; traceTc "tc_patsyn_finish {" $ ppr (unLoc lname) $$ ppr (unLoc lpat') $$ ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$ - ppr (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts) $$ - ppr wrapped_args $$ + ppr (ex_tvs, prov_theta, prov_dicts) $$ + ppr args $$ + ppr arg_tys $$ ppr pat_ty -- Make the 'matcher' ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat' (univ_tvs, req_theta, req_ev_binds, req_dicts) - (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts) - wrapped_args -- Not necessarily zonked + (ex_tvs, ex_tys, prov_theta, prov_dicts) + (args, arg_tys) pat_ty @@ -264,14 +436,9 @@ tc_patsyn_finish lname dir is_infix lpat' tcRecSelBinds (ValBindsOut (zip (repeat NonRecursive) selector_binds) sigs) + ; traceTc "tc_patsyn_finish }" empty ; return (matcher_bind, tcg_env) } - where - zonk_wrapped_arg :: (Var, HsWrapper) -> TcM (Var, HsWrapper) - -- The HsWrapper will get zonked later, as part of the LHsBinds - zonk_wrapped_arg (arg_id, wrap) = do { arg_id <- zonkId arg_id - ; return (arg_id, wrap) } - {- ************************************************************************ * * @@ -283,15 +450,15 @@ tc_patsyn_finish lname dir is_infix lpat' tcPatSynMatcher :: Located Name -> LPat Id -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar]) - -> ([TcTyVar], [TcType], ThetaType, TcEvBinds, [EvTerm]) - -> [(Var, HsWrapper)] + -> ([TcTyVar], [TcType], ThetaType, [EvTerm]) + -> ([LHsExpr TcId], [TcType]) -> TcType -> TcM ((Id, Bool), LHsBinds Id) -- See Note [Matchers and builders for pattern synonyms] in PatSyn tcPatSynMatcher (L loc name) lpat (univ_tvs, req_theta, req_ev_binds, req_dicts) - (ex_tvs, ex_tys, prov_theta, prov_ev_binds, prov_dicts) - wrapped_args pat_ty + (ex_tvs, ex_tys, prov_theta, prov_dicts) + (args, arg_tys) pat_ty = do { lev_uniq <- newUnique ; tv_uniq <- newUnique ; let lev_name = mkInternalName lev_uniq (mkTyVarOcc "rlev") loc @@ -299,13 +466,11 @@ tcPatSynMatcher (L loc name) lpat lev_tv = mkTcTyVar lev_name levityTy (SkolemTv False) lev = mkTyVarTy lev_tv res_tv = mkTcTyVar tv_name (tYPE lev) (SkolemTv False) - is_unlifted = null wrapped_args && null prov_dicts + is_unlifted = null args && null prov_dicts res_ty = mkTyVarTy res_tv - (cont_arg_tys, cont_args) - | is_unlifted = ([voidPrimTy], [nlHsVar voidPrimId]) - | otherwise = unzip [ (varType arg, mkLHsWrap wrap $ nlHsVar arg) - | (arg, wrap) <- wrapped_args - ] + (cont_args, cont_arg_tys) + | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy]) + | otherwise = (args, arg_tys) cont_ty = mkInvSigmaTy ex_tvs prov_theta $ mkFunTys cont_arg_tys res_ty @@ -321,10 +486,8 @@ tcPatSynMatcher (L loc name) lpat matcher_id = mkExportedLocalId PatSynId matcher_name matcher_sigma -- See Note [Exported LocalIds] in Id - cont' = mkLHsWrap (mkWpLet prov_ev_binds) $ - foldl nlHsApp - (mkLHsWrap (mkWpEvApps prov_dicts) - (nlHsTyApp cont ex_tys)) cont_args + inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys + cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args fail' = nlHsApps fail [nlHsVar voidPrimId] @@ -425,6 +588,7 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat | otherwise -- Bidirectional = do { patsyn <- tcLookupPatSyn name + ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn -- Bidirectional, so patSynBuilder returns Just @@ -540,7 +704,6 @@ simply discard the signature. Note [Record PatSyn Desugaring] ------------------------------- - It is important that prov_theta comes before req_theta as this ordering is used when desugaring record pattern synonym updates. @@ -645,8 +808,8 @@ tcPatToExpr args = go -- These are used in computing the type of a pattern synonym and also -- in generating matcher functions, since success continuations need -- to be passed these pattern-bound evidences. -tcCollectEx :: LPat Id -> TcM (TyVarSet, [EvVar]) -tcCollectEx = return . go +tcCollectEx :: LPat Id -> (TyVarSet, [EvVar]) +tcCollectEx pat = go pat where go :: LPat Id -> (TyVarSet, [EvVar]) go = go1 . unLoc @@ -676,3 +839,4 @@ tcCollectEx = return . go goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar]) goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p + diff --git a/compiler/typecheck/TcPatSyn.hs-boot b/compiler/typecheck/TcPatSyn.hs-boot index 11c1bc19a2..af5aec7cbc 100644 --- a/compiler/typecheck/TcPatSyn.hs-boot +++ b/compiler/typecheck/TcPatSyn.hs-boot @@ -2,11 +2,14 @@ module TcPatSyn where import Name ( Name ) import Id ( Id ) -import HsSyn ( PatSynBind, LHsBinds ) +import HsSyn ( PatSynBind, LHsBinds, LHsSigType ) import TcRnTypes ( TcM, TcPatSynInfo ) import TcRnMonad ( TcGblEnv) import Outputable ( Outputable ) +tcPatSynSig :: Name -> LHsSigType Name + -> TcM TcPatSynInfo + tcInferPatSynDecl :: PatSynBind Name Name -> TcM (LHsBinds Id, TcGblEnv) diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 9316d433f9..8489512424 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1178,12 +1178,13 @@ data TcIdSigBndr -- See Note [Complete and partial type signatures] data TcPatSynInfo = TPSI { - patsig_name :: Name, - patsig_tau :: TcSigmaType, - patsig_ex :: [TcTyVar], - patsig_prov :: TcThetaType, - patsig_univ :: [TcTyVar], - patsig_req :: TcThetaType + patsig_name :: Name, + patsig_univ_tvs :: [TcTyVar], + patsig_req :: TcThetaType, + patsig_ex_tvs :: [TcTyVar], + patsig_prov :: TcThetaType, + patsig_arg_tys :: [TcSigmaType], + patsig_body_ty :: TcSigmaType } findScopedTyVars -- See Note [Binding scoped type variables] diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 1257dbf077..51a1eee695 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -267,7 +267,7 @@ matchExpectedTyConApp tc orig_ty -- This happened in Trac #7368 defer is_return = ASSERT2( classifiesTypeWithValues res_kind, ppr tc ) - do { (k_subst, kvs') <- tcInstTyVars kvs + do { (k_subst, kvs') <- newMetaTyVars kvs ; let arg_kinds' = substTys k_subst arg_kinds kappa_tys = mkTyVarTys kvs' ; tau_tys <- mapM (newMaybeReturnTyVarTy is_return) arg_kinds' @@ -482,7 +482,7 @@ tc_sub_type_ds origin ctxt ty_actual ty_expected | (tvs, theta, in_rho) <- tcSplitSigmaTy ty_actual , not (null tvs && null theta) - = do { (subst, tvs') <- tcInstTyVars tvs + = do { (subst, tvs') <- newMetaTyVars tvs ; let tys' = mkTyVarTys tvs' theta' = substTheta subst theta in_rho' = substTy subst in_rho diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index b15ac126a2..c53a0128b4 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -57,7 +57,7 @@ module TyCoRep ( -- Free variables tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, - tyCoVarsOfTypeAcc, tyCoVarsOfTypeList, + tyCoVarsBndrAcc, tyCoVarsOfTypeAcc, tyCoVarsOfTypeList, tyCoVarsOfTypesAcc, tyCoVarsOfTypesList, closeOverKindsDSet, closeOverKindsAcc, coVarsOfType, coVarsOfTypes, @@ -1049,19 +1049,24 @@ tyCoVarsOfTypeList ty = runFVList $ tyCoVarsOfTypeAcc ty -- | The worker for `tyVarsOfType` and `tyVarsOfTypeList`. -- The previous implementation used `unionVarSet` which is O(n+m) and can -- make the function quadratic. --- It's exported, so that it can be composed with other functions that compute --- free variables. +-- It's exported, so that it can be composed with +-- other functions that compute free variables. -- See Note [FV naming conventions] in FV. +-- +-- Eta-expanded because that makes it run faster (apparently) tyCoVarsOfTypeAcc :: Type -> FV -tyCoVarsOfTypeAcc (TyVarTy v) fv_cand in_scope acc = (oneVar v `unionFV` tyCoVarsOfTypeAcc (tyVarKind v)) fv_cand in_scope acc -tyCoVarsOfTypeAcc (TyConApp _ tys) fv_cand in_scope acc = tyCoVarsOfTypesAcc tys fv_cand in_scope acc -tyCoVarsOfTypeAcc (LitTy {}) fv_cand in_scope acc = noVars fv_cand in_scope acc -tyCoVarsOfTypeAcc (AppTy fun arg) fv_cand in_scope acc = (tyCoVarsOfTypeAcc fun `unionFV` tyCoVarsOfTypeAcc arg) fv_cand in_scope acc -tyCoVarsOfTypeAcc (ForAllTy bndr ty) fv_cand in_scope acc - = (delBinderVarFV bndr (tyCoVarsOfTypeAcc ty) - `unionFV` tyCoVarsOfTypeAcc (binderType bndr)) fv_cand in_scope acc -tyCoVarsOfTypeAcc (CastTy ty co) fv_cand in_scope acc = (tyCoVarsOfTypeAcc ty `unionFV` tyCoVarsOfCoAcc co) fv_cand in_scope acc -tyCoVarsOfTypeAcc (CoercionTy co) fv_cand in_scope acc = tyCoVarsOfCoAcc co fv_cand in_scope acc +tyCoVarsOfTypeAcc (TyVarTy v) a b c = (oneVar v `unionFV` tyCoVarsOfTypeAcc (tyVarKind v)) a b c +tyCoVarsOfTypeAcc (TyConApp _ tys) a b c = tyCoVarsOfTypesAcc tys a b c +tyCoVarsOfTypeAcc (LitTy {}) a b c = noVars a b c +tyCoVarsOfTypeAcc (AppTy fun arg) a b c = (tyCoVarsOfTypeAcc fun `unionFV` tyCoVarsOfTypeAcc arg) a b c +tyCoVarsOfTypeAcc (ForAllTy bndr ty) a b c = tyCoVarsBndrAcc bndr (tyCoVarsOfTypeAcc ty) a b c +tyCoVarsOfTypeAcc (CastTy ty co) a b c = (tyCoVarsOfTypeAcc ty `unionFV` tyCoVarsOfCoAcc co) a b c +tyCoVarsOfTypeAcc (CoercionTy co) a b c = tyCoVarsOfCoAcc co a b c + +tyCoVarsBndrAcc :: TyBinder -> FV -> FV +-- Free vars of (forall b. <thing with fvs>) +tyCoVarsBndrAcc bndr fvs = delBinderVarFV bndr fvs + `unionFV` tyCoVarsOfTypeAcc (binderType bndr) -- | Returns free variables of types, including kind variables as -- a non-deterministic set. For type synonyms it does /not/ expand the diff --git a/testsuite/tests/patsyn/should_compile/MoreEx.hs b/testsuite/tests/patsyn/should_compile/MoreEx.hs new file mode 100644 index 0000000000..ed5e097ee2 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/MoreEx.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE GADTs, PatternSynonyms #-} + +-- Tests that for unidirectional pattern synonyms +-- the pattern synonym can be more existential +-- (i.e. lose information) wrt the original + +module MoreEx where + +pattern ExCons :: a -> [a] -> [b] +pattern ExCons x xs <- x : xs + +data T where + MkT1 :: ([a] -> Int) -> [a] -> T + MkT2 :: (a -> Int) -> a -> T + +pattern ExT1 :: b -> (b -> Int) -> T +pattern ExT1 x f <- MkT1 f x + +pattern ExT2 :: b -> (c -> Int) -> T +pattern ExT2 x f <- MkT2 f x diff --git a/testsuite/tests/patsyn/should_compile/T11224b.hs b/testsuite/tests/patsyn/should_compile/T11224b.hs new file mode 100644 index 0000000000..89fb764005 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T11224b.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE PatternSynonyms, GADTs, RankNTypes #-} + +module T11224b where + +data T b where + MkT :: a -> b -> T b + +-- Should be fine! +-- pattern P :: c -> d -> T d +pattern P :: forall d. forall c. c -> d -> T d +pattern P x y <- MkT x y + + + + + + diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 3793c0d322..f3d90aceae 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -24,6 +24,7 @@ test('T9889', normal, compile, ['']) test('T9867', normal, compile, ['']) test('T9975a', normal, compile_fail, ['']) test('T9975b', normal, compile, ['']) +test('T10426', [expect_broken(10426)], compile, ['']) test('T10747', normal, compile, ['']) test('T10997', [extra_clean(['T10997a.hi', 'T10997a.o'])], multimod_compile, ['T10997', '-v0']) test('T10997_1', [extra_clean(['T10997_1a.hi', 'T10997_1a.o'])], multimod_compile, ['T10997_1', '-v0']) @@ -45,3 +46,5 @@ test('T10897', expect_broken(10897), multi_compile, ['T10897', [ ('T10897a.hs','-c') ,('T10897b.hs', '-c')], '']) test('T9793', normal, compile, ['']) +test('T11224b', normal, compile, ['']) +test('MoreEx', normal, compile, ['']) diff --git a/testsuite/tests/patsyn/should_fail/T11010.stderr b/testsuite/tests/patsyn/should_fail/T11010.stderr index 5f62b1357e..47492cde3a 100644 --- a/testsuite/tests/patsyn/should_fail/T11010.stderr +++ b/testsuite/tests/patsyn/should_fail/T11010.stderr @@ -1,8 +1,14 @@ -T11010.hs:8:1: error: - The 'required' context ‘a ~ Int’ - mentions existential type variable ‘a’ - -T11010.hs:16:1: error: - The 'required' context ‘a ~ Int’ - mentions existential type variable ‘a’ +T11010.hs:9:36: error: + • Couldn't match type ‘a1’ with ‘Int’ + ‘a1’ is a rigid type variable bound by + a pattern with constructor: + Fun :: forall b a. String -> (a -> b) -> Expr a -> Expr b, + in a pattern synonym declaration + at T11010.hs:9:26 + Expected type: a -> b + Actual type: a1 -> b + • In the declaration for pattern synonym ‘IntFun’ + • Relevant bindings include + x :: Expr a1 (bound at T11010.hs:9:36) + f :: a1 -> b (bound at T11010.hs:9:34) diff --git a/testsuite/tests/patsyn/should_fail/T9793-fail.stderr b/testsuite/tests/patsyn/should_fail/T9793-fail.stderr index 62713dcd4c..23122f9ea7 100644 --- a/testsuite/tests/patsyn/should_fail/T9793-fail.stderr +++ b/testsuite/tests/patsyn/should_fail/T9793-fail.stderr @@ -1,4 +1,5 @@ T9793-fail.hs:6:16: error: - Pattern synonym definition cannot contain as-patterns (@) which contain free variables: - x@(y : _) + • Pattern synonym definition cannot contain as-patterns (@) which contain free variables: + x@(y : _) + • In the declaration for pattern synonym ‘P’ diff --git a/testsuite/tests/patsyn/should_fail/as-pattern.stderr b/testsuite/tests/patsyn/should_fail/as-pattern.stderr index caabd47090..00ea6c8091 100644 --- a/testsuite/tests/patsyn/should_fail/as-pattern.stderr +++ b/testsuite/tests/patsyn/should_fail/as-pattern.stderr @@ -1,4 +1,5 @@ as-pattern.hs:4:18: error: - Pattern synonym definition cannot contain as-patterns (@) which contain free variables: - x@(Just y) + • Pattern synonym definition cannot contain as-patterns (@) which contain free variables: + x@(Just y) + • In the declaration for pattern synonym ‘P’ diff --git a/testsuite/tests/patsyn/should_run/T11224.hs b/testsuite/tests/patsyn/should_run/T11224.hs index f834e9b47e..39c744cb5f 100644 --- a/testsuite/tests/patsyn/should_run/T11224.hs +++ b/testsuite/tests/patsyn/should_run/T11224.hs @@ -1,10 +1,10 @@ -{-# LANGUAGE PatternSynonyms , ViewPatterns #-} +{-# LANGUAGE PatternSynonyms, ViewPatterns #-} --- inlining a pattern synonym shouldn't change semantics +module Main where import Text.Read --- pattern PRead :: () => Read a => a -> String +pattern PRead :: Read a => () => a -> String pattern PRead a <- (readMaybe -> Just a) foo :: String -> Int @@ -26,3 +26,4 @@ main = do print $ bar "1" -- 1 print $ bar "[1,2,3]" -- 6 print $ bar "xxx" -- 666 + diff --git a/testsuite/tests/patsyn/should_run/all.T b/testsuite/tests/patsyn/should_run/all.T index c12bfc6cb2..618dd69536 100644 --- a/testsuite/tests/patsyn/should_run/all.T +++ b/testsuite/tests/patsyn/should_run/all.T @@ -12,4 +12,5 @@ test('match-unboxed', normal, compile_and_run, ['']) test('unboxed-wrapper', normal, compile_and_run, ['']) test('records-run', normal, compile_and_run, ['']) test('ghci', just_ghci, ghci_script, ['ghci.script']) -test('T11224', [expect_broken(11224)], compile_and_run, [''])
\ No newline at end of file +test('T11224', [expect_broken(11224)], compile_and_run, ['']) +test('T11224', normal, compile_and_run, ['']) |