diff options
-rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 24 | ||||
-rw-r--r-- | compiler/GHC/Hs/Expr.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Arrows.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Expr.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Match.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Iface/Ext/Ast.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 25 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Arrow.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Expr.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Match.hs | 18 | ||||
-rw-r--r-- | compiler/GHC/Tc/TyCl/PatSyn.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 15 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 35 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/Zonk.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Tc/Validity.hs | 22 |
15 files changed, 119 insertions, 56 deletions
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 9503ba4ccf..caac8e6784 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -72,7 +72,10 @@ module GHC.Core.TyCo.Rep ( typeSize, coercionSize, provSize, -- * Multiplicities - Scaled(..), scaledMult, scaledThing, mapScaledType, Mult + Scaled(..), scaledMult, scaledThing, mapScaledType, Mult, + + -- * visible foralls related definitions + ArgType(..), mkVisFunForallTys, normalArgTys ) where #include "HsVersions.h" @@ -2071,3 +2074,22 @@ So that Mult feels a bit more structured, we provide pattern synonyms and smart constructors for these. -} type Mult = Type + +data ArgType + = NormalArgType (Scaled Type) + | ForallArgType ReqTVBinder + deriving Data.Data + +mkVisFunForallTy :: ArgType -> Type -> Type +mkVisFunForallTy (NormalArgType m) ty = mkScaledFunTy VisArg m ty +mkVisFunForallTy (ForallArgType (Bndr var _)) ty = ForAllTy (Bndr var Required) ty + +mkVisFunForallTys :: [ArgType] -> Type -> Type +mkVisFunForallTys tys ty = foldr mkVisFunForallTy ty tys + +normalArgTys :: [ArgType] -> [Scaled Type] +normalArgTys [] = [] +normalArgTys (arg_ty : arg_tys) + = case arg_ty of + NormalArgType ty -> ty : normalArgTys arg_tys + _ -> normalArgTys arg_tys diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs index 724f37cbd7..e32cf11737 100644 --- a/compiler/GHC/Hs/Expr.hs +++ b/compiler/GHC/Hs/Expr.hs @@ -50,6 +50,7 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Data.FastString import GHC.Core.Type +import GHC.Core.TyCo.Rep (ArgType) import GHC.Builtin.Types (mkTupleStr) import GHC.Tc.Utils.TcType (TcType) import {-# SOURCE #-} GHC.Tc.Types (TcLclEnv) @@ -1710,7 +1711,7 @@ data MatchGroup p body data MatchGroupTc = MatchGroupTc - { mg_arg_tys :: [Scaled Type] -- Types of the arguments, t1..tn + { mg_arg_tys :: [ArgType] -- Types of the arguments, t1..tn , mg_res_ty :: Type -- Type of the result, tr } deriving Data diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs index 52de5f6fb5..02e5869f08 100644 --- a/compiler/GHC/HsToCore/Arrows.hs +++ b/compiler/GHC/HsToCore/Arrows.hs @@ -43,6 +43,7 @@ import GHC.Core import GHC.Core.FVs import GHC.Core.Utils import GHC.Core.Make +import GHC.Core.TyCo.Rep import GHC.HsToCore.Binds (dsHsWrapper) import GHC.Types.Id @@ -595,7 +596,7 @@ dsCmd ids local_vars stack_ty res_ty exprFreeIdsDSet core_body `uniqDSetIntersectUniqSet` local_vars) dsCmd ids local_vars stack_ty res_ty - (HsCmdLamCase _ mg@MG { mg_ext = MatchGroupTc [Scaled arg_mult arg_ty] _ }) env_ids = do + (HsCmdLamCase _ mg@MG { mg_ext = MatchGroupTc [NormalArgType (Scaled arg_mult arg_ty)] _ }) env_ids = do arg_id <- newSysLocalDs arg_mult arg_ty let case_cmd = noLoc $Â HsCmdCase noExtField (nlHsVar arg_id) mg dsCmdLam ids local_vars stack_ty res_ty [nlVarPat arg_id] case_cmd env_ids diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index 24b4a76892..d585cd9456 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -48,6 +48,7 @@ import GHC.Core.Coercion( Coercion ) import GHC.Core import GHC.Core.Utils import GHC.Core.Make +import GHC.Core.TyCo.Rep( ArgType (..) ) import GHC.Driver.Session import GHC.Types.CostCentre @@ -721,7 +722,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields ; ([discrim_var], matching_code) <- matchWrapper RecUpd (Just record_expr) -- See Note [Scrutinee in Record updates] (MG { mg_alts = noLoc alts - , mg_ext = MatchGroupTc [unrestricted in_ty] out_ty + , mg_ext = MatchGroupTc [NormalArgType (unrestricted in_ty)] out_ty , mg_origin = FromSource }) -- FromSource is not strictly right, but we @@ -1119,7 +1120,7 @@ dsDo ctx stmts (MG { mg_alts = noLoc [mkSimpleMatch LambdaExpr [mfix_pat] body] - , mg_ext = MatchGroupTc [unrestricted tup_ty] body_ty + , mg_ext = MatchGroupTc [NormalArgType (unrestricted tup_ty)] body_ty , mg_origin = Generated }) mfix_pat = noLoc $ LazyPat noExtField $ mkBigLHsPatTupId rec_tup_pats body = noLoc $ HsDo body_ty diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs index 491191d6a7..6377af10ac 100644 --- a/compiler/GHC/HsToCore/Match.hs +++ b/compiler/GHC/HsToCore/Match.hs @@ -36,6 +36,7 @@ import GHC.Tc.Utils.Monad import GHC.HsToCore.Pmc import GHC.HsToCore.Pmc.Types ( Nablas, initNablas ) import GHC.Core +import GHC.Core.TyCo.Rep (normalArgTys) import GHC.Types.Literal import GHC.Core.Utils import GHC.Core.Make @@ -757,11 +758,11 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches ; locn <- getSrcSpanDs ; new_vars <- case matches of - [] -> newSysLocalsDsNoLP arg_tys + [] -> newSysLocalsDsNoLP (normalArgTys arg_tys) (m:_) -> selectMatchVars (zipWithEqual "matchWrapper" (\a b -> (scaledMult a, unLoc b)) - arg_tys + (normalArgTys arg_tys) (hsLMatchPats m)) -- Pattern match check warnings for /this match-group/. diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs index 01c5b6102f..9148fa1876 100644 --- a/compiler/GHC/Iface/Ext/Ast.hs +++ b/compiler/GHC/Iface/Ext/Ast.hs @@ -34,6 +34,7 @@ import GHC.Core.ConLike ( conLikeName, ConLike(RealDataCon) ) import GHC.Core.TyCon ( TyCon, tyConClass_maybe ) import GHC.Core.FVs import GHC.Core.DataCon ( dataConNonlinearType ) +import GHC.Core.TyCo.Rep ( mkVisFunForallTys ) import GHC.HsToCore ( deSugarExpr ) import GHC.Types.FieldLabel import GHC.Hs @@ -45,7 +46,7 @@ import GHC.Types.Name ( Name, nameSrcSpan, nameUnique ) import GHC.Types.Name.Env ( NameEnv, emptyNameEnv, extendNameEnv, lookupNameEnv ) import GHC.Types.SrcLoc import GHC.Tc.Utils.Zonk ( hsLitType, hsPatType ) -import GHC.Core.Type ( mkVisFunTys, Type ) +import GHC.Core.Type ( Type ) import GHC.Core.Predicate import GHC.Core.InstEnv import GHC.Builtin.Types ( mkListTy, mkSumTy ) @@ -747,7 +748,7 @@ instance HiePass p => HasType (Located (HsExpr (GhcPass p))) where fallback = makeNode e' spn matchGroupType :: MatchGroupTc -> Type - matchGroupType (MatchGroupTc args res) = mkVisFunTys args res + matchGroupType (MatchGroupTc args res) = mkVisFunForallTys args res -- | Skip desugaring of these expressions for performance reasons. -- diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index ab8c3c7247..d53d3a2d76 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -39,6 +39,7 @@ import GHC.Core.TyCo.Ppr import GHC.Core.TyCo.Subst (substTyWithInScope) import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType ) import GHC.Core.Type +import GHC.Types.Basic ( PromotionFlag (..) ) import GHC.Tc.Types.Evidence import GHC.Types.Var.Set import GHC.Builtin.PrimOps( tagToEnumKey ) @@ -442,6 +443,9 @@ tcInstFun do_ql inst_final rn_fun fun_sigma rn_args ; case cts of Indirect fun_ty' -> go delta acc so_far fun_ty' args Flexi -> go1 delta acc so_far fun_ty args } + | (bndrs, _) <- splitForAllTysReq fun_ty + , not (null bndrs) + = go1 delta acc so_far fun_ty args | otherwise = go1 delta acc so_far fun_ty args @@ -556,6 +560,25 @@ tcVTA :: TcType -- Function type -- Deal with a visible type application -- The function type has already had its Inferred binders instantiated tcVTA fun_ty hs_ty + | (bndr : _, ty) <- splitForAllTysReq fun_ty + = do { let tv = binderVar bndr + kind = tyVarKind tv + ; ty_arg <- tcHsTypeApp hs_ty kind + ; traceTc "ty_arg is" (ppr ty_arg) + + ; inner_ty <- zonkTcType ty + -- See Note [Visible type application zonk] + + ; let in_scope = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg]) + insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty + -- NB: tv and ty_arg have the same kind, so this + -- substitution is kind-respecting + ; traceTc "VTA" (vcat [ppr tv, debugPprType kind + , debugPprType ty_arg + , debugPprType (tcTypeKind ty_arg) + , debugPprType inner_ty + , debugPprType insted_ty ]) + ; return (ty_arg, insted_ty) } | Just (tvb, inner_ty) <- tcSplitForAllTy_maybe fun_ty , binderArgFlag tvb == Specified -- It really can't be Inferred, because we've just @@ -1087,5 +1110,3 @@ tcTagToEnum expr fun args app_res_ty res_ty tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann - - diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index ed30afa893..4434c8d2a8 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -31,6 +31,7 @@ import GHC.Tc.Utils.Env import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence import GHC.Core.Multiplicity +import GHC.Core.TyCo.Rep ( ArgType(..) ) import GHC.Types.Id( mkLocalId ) import GHC.Tc.Utils.Instantiate import GHC.Builtin.Types @@ -265,7 +266,7 @@ tc_cmd env , m_grhss = grhss' }) arg_tys = map (unrestricted . hsLPatType) pats' cmd' = HsCmdLam x (MG { mg_alts = L l [match'] - , mg_ext = MatchGroupTc arg_tys res_ty + , mg_ext = MatchGroupTc (NormalArgType <$> arg_tys) res_ty , mg_origin = origin }) ; return (mkHsCmdWrap (mkWpCastN co) cmd') } where diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index a64154facf..d7937ab965 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -1124,7 +1124,7 @@ tcSynArgE orig sigma_ty syn_ty thing_inside , res_wrapper ) -- :: res_ty_out "->" res_ty , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $ - \ [arg_ty] res_ty -> + \ [NormalArgTy arg_ty] res_ty -> do { arg_tc_ty <- expTypeToType (scaledThing arg_ty) ; res_tc_ty <- expTypeToType res_ty diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index ff01093a34..3d65a93320 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -57,6 +57,7 @@ import GHC.Types.Name import GHC.Builtin.Types import GHC.Types.Id import GHC.Core.TyCon +import GHC.Core.TyCo.Rep ( ArgType(..) ) import GHC.Builtin.Types.Prim import GHC.Tc.Types.Evidence import GHC.Utils.Outputable @@ -141,7 +142,7 @@ tcMatchesCase :: (Outputable (body GhcRn)) => -- wrapper goes from MatchGroup's ty to expected ty tcMatchesCase ctxt (Scaled scrut_mult scrut_ty) matches res_ty - = tcMatches ctxt [Scaled scrut_mult (mkCheckExpType scrut_ty)] res_ty matches + = tcMatches ctxt [NormalArgTy (Scaled scrut_mult (mkCheckExpType scrut_ty))] res_ty matches tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify -> TcMatchCtxt HsExpr @@ -187,7 +188,7 @@ data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module -- | Type-check a MatchGroup. tcMatches :: (Outputable (body GhcRn)) => TcMatchCtxt body - -> [Scaled ExpSigmaType] -- Expected pattern types + -> [ArgTy] -- Expected pattern types -> ExpRhoType -- Expected result-type of the Match. -> MatchGroup GhcRn (Located (body GhcRn)) -> TcM (MatchGroup GhcTc (Located (body GhcTc))) @@ -199,7 +200,7 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches -- when in inference mode, so we must do it ourselves, -- here, using expTypeToType = do { tcEmitBindingUsage bottomUE - ; pat_tys <- mapM scaledExpTypeToType pat_tys + ; pat_tys <- mapM argTyToArgType pat_tys ; rhs_ty <- expTypeToType rhs_ty ; return (MG { mg_alts = L l [] , mg_ext = MatchGroupTc pat_tys rhs_ty @@ -209,15 +210,20 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches ; let (usages,matches') = unzip umatches ; tcEmitBindingUsage $ supUEs usages - ; pat_tys <- mapM readScaledExpType pat_tys + ; pat_tys <- mapM argTyToArgType pat_tys ; rhs_ty <- readExpType rhs_ty ; return (MG { mg_alts = L l matches' , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } + where + argTyToArgType (NormalArgTy (Scaled m t)) = fmap (NormalArgType . Scaled m) (readExpType t) + argTyToArgType (ForallArgTy p) = return (ForallArgType p) + + ------------- tcMatch :: (Outputable (body GhcRn)) => TcMatchCtxt body - -> [Scaled ExpSigmaType] -- Expected pattern types + -> [ArgTy] -- Expected pattern types -> ExpRhoType -- Expected result-type of the Match. -> LMatch GhcRn (Located (body GhcRn)) -> TcM (LMatch GhcTc (Located (body GhcTc))) @@ -228,7 +234,7 @@ tcMatch ctxt pat_tys rhs_ty match tc_match ctxt pat_tys rhs_ty match@(Match { m_pats = pats, m_grhss = grhss }) = add_match_ctxt match $ - do { (pats', grhss') <- tcPats (mc_what ctxt) pats pat_tys $ + do { (pats', grhss') <- tcPats (mc_what ctxt) pats (scaledExpTypes pat_tys) $ tcGRHSs ctxt grhss rhs_ty ; return (Match { m_ext = noExtField , m_ctxt = mc_what ctxt, m_pats = pats' diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 79d3f97077..69f355b01d 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -46,6 +46,7 @@ import GHC.Types.Basic import GHC.Tc.Solver import GHC.Tc.Utils.Unify import GHC.Core.Predicate +import GHC.Core.TyCo.Rep ( ArgType(..) ) import GHC.Builtin.Types import GHC.Tc.Utils.TcType import GHC.Tc.Types.Evidence @@ -728,14 +729,14 @@ tcPatSynMatcher (L loc name) lpat L (getLoc lpat) $ HsCase noExtField (nlHsVar scrutinee) $ MG{ mg_alts = L (getLoc lpat) cases - , mg_ext = MatchGroupTc [unrestricted pat_ty] res_ty + , mg_ext = MatchGroupTc [NormalArgType (unrestricted pat_ty)] res_ty , mg_origin = Generated } body' = noLoc $ HsLam noExtField $ MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr args body] - , mg_ext = MatchGroupTc (map unrestricted [pat_ty, cont_ty, fail_ty]) res_ty + , mg_ext = MatchGroupTc (map (NormalArgType . unrestricted) [pat_ty, cont_ty, fail_ty]) res_ty , mg_origin = Generated } match = mkMatch (mkPrefixFunRhs (L loc name)) [] diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 54258c7e52..1a661bc7cd 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -28,6 +28,7 @@ module GHC.Tc.Utils.TcType ( TcTyCon, KnotTied, ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType, + ArgTy(..), scaledExpTypes, SyntaxOpType(..), synKnownType, mkSynFunTys, @@ -398,6 +399,16 @@ instance Outputable InferResult where mkCheckExpType :: TcType -> ExpType mkCheckExpType = Check +data ArgTy + = NormalArgTy (Scaled ExpSigmaType) + | ForallArgTy ReqTVBinder + +scaledExpTypes :: [ArgTy] -> [Scaled ExpSigmaType] +scaledExpTypes [] = [] +scaledExpTypes (arg_ty : arg_tys) + = case arg_ty of + NormalArgTy ty -> ty : scaledExpTypes arg_tys + _ -> scaledExpTypes arg_tys {- ********************************************************************* * * @@ -1286,9 +1297,9 @@ tcSplitPhiTy ty -- | Split a sigma type into its parts. tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type) -tcSplitSigmaTy ty = case tcSplitForAllTys ty of +tcSplitSigmaTy ty = case tcSplitForAllTysInvis ty of (tvs, rho) -> case tcSplitPhiTy rho of - (theta, tau) -> (tvs, theta, tau) + (theta, tau) -> (binderVar <$> tvs, theta, tau) -- | Split a sigma type into its parts, going underneath as many @ForAllTy@s -- as possible. For example, given this type synonym: diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index c1202f02d7..add76764f8 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -156,7 +156,7 @@ matchActualFunTySigma herald mb_thing err_info fun_ty ------------ mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) - mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far) + mk_ctxt res_ty env = mkFunTysMsg env herald (reverse (NormalArgType <$> arg_tys_so_far)) res_ty n_val_args_in_call (n_val_args_in_call, arg_tys_so_far) = err_info @@ -290,7 +290,7 @@ matchExpectedFunTys :: forall a. -> UserTypeCtxt -> Arity -> ExpRhoType -- Skolemised - -> ([Scaled ExpSigmaType] -> ExpRhoType -> TcM a) + -> ([ArgTy] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a) -- If matchExpectedFunTys n ty = (_, wrap) -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, @@ -320,7 +320,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys) + do { (wrap_res, result) <- go ((NormalArgTy . Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys) (n-1) res_ty ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty doc ; return ( fun_wrap, result ) } @@ -328,6 +328,16 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside doc = text "When inferring the argument type of a function with type" <+> quotes (ppr orig_ty) + go acc_arg_tys n ty + | (bndrs, ty') <- tcSplitForAllTysReq ty + , not (null bndrs) + = do { let forall_args = ForallArgTy <$> bndrs + ; let req_arg_tys = forall_args ++ acc_arg_tys + ; let arg_num = n - (length forall_args) + ; (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty' $ \ty' -> + go req_arg_tys arg_num ty' + ; return (wrap_gen <.> wrap_res, result) } + go acc_arg_tys n ty@(TyVarTy tv) | isMetaTyVar tv = do { cts <- readMetaTyVar tv @@ -354,11 +364,11 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside defer acc_arg_tys n (mkCheckExpType ty) ------------ - defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) + defer :: [ArgTy] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) defer acc_arg_tys n fun_ty = do { more_arg_tys <- replicateM n newInferExpType ; res_ty <- newInferExpType - ; result <- thing_inside (reverse acc_arg_tys ++ (map unrestricted more_arg_tys)) res_ty + ; result <- thing_inside (reverse acc_arg_tys ++ (map (NormalArgTy . unrestricted) more_arg_tys)) res_ty ; more_arg_tys <- mapM readExpType more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkVisFunTysMany more_arg_tys res_ty @@ -367,19 +377,24 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside ; return (wrap, result) } ------------ - mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt :: [ArgTy] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) mk_ctxt arg_tys res_ty env = mkFunTysMsg env herald arg_tys' res_ty arity where - arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $ - reverse arg_tys + arg_tys' = map toArgType (reverse arg_tys) + + toArgType (NormalArgTy (Scaled u v)) + = NormalArgType (Scaled u (checkingExpType "matchExpectedFunTys" v)) + toArgType (ForallArgTy bndr) + = ForallArgType bndr + -- this is safe b/c we're called from "go" -mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity +mkFunTysMsg :: TidyEnv -> SDoc -> [ArgType] -> TcType -> Arity -> TcM (TidyEnv, MsgDoc) mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call = do { (env', fun_rho) <- zonkTidyTcType env $ - mkVisFunTys arg_tys res_ty + mkVisFunForallTys arg_tys res_ty ; let (all_arg_tys, _) = splitFunTys fun_rho n_fun_args = length all_arg_tys diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index a47b75adc2..7285bc3f9d 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -82,6 +82,7 @@ import GHC.Utils.Panic import GHC.Types.Unique.FM import GHC.Core.Multiplicity import GHC.Core +import GHC.Core.TyCo.Rep (ArgType(..), normalArgTys) import {-# SOURCE #-} GHC.Tc.Gen.Splice (runTopSplice) @@ -671,10 +672,10 @@ zonkMatchGroup env zBody (MG { mg_alts = L l ms , mg_ext = MatchGroupTc arg_tys res_ty , mg_origin = origin }) = do { ms' <- mapM (zonkMatch env zBody) ms - ; arg_tys' <- zonkScaledTcTypesToTypesX env arg_tys + ; arg_tys' <- zonkScaledTcTypesToTypesX env (normalArgTys arg_tys) ; res_ty' <- zonkTcTypeToTypeX env res_ty ; return (MG { mg_alts = L l ms' - , mg_ext = MatchGroupTc arg_tys' res_ty' + , mg_ext = MatchGroupTc (NormalArgType <$> arg_tys') res_ty' , mg_origin = origin }) } zonkMatch :: ZonkEnv diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 5f08249e38..7c38d217c9 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -567,11 +567,6 @@ linearityAllowed = typeLevelUserTypeCtxt -- where VDQ is permitted) and -- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where -- VDQ is disallowed). -vdqAllowed :: UserTypeCtxt -> Bool -vdqAllowed ctxt = case typeOrKindCtxt ctxt of - OnlyTypeCtxt -> False - OnlyKindCtxt -> True - BothTypeAndKindCtxt -> True {- Note [Correctness and performance of type synonym validity checking] @@ -724,7 +719,7 @@ check_type ve (CastTy ty _) = check_type ve ty -- -- Critically, this case must come *after* the case for TyConApp. -- See Note [Liberal type synonyms]. -check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt +check_type ve@(ValidityEnv{ ve_tidy_env = env , ve_rank = rank, ve_expand = expand }) ty | not (null tvbs && null theta) = do { traceTc "check_type" (ppr ty $$ ppr rank) @@ -736,12 +731,6 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt -- Reject forall (a :: Eq b => b). blah -- In a kind signature we don't allow constraints - ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs - || vdqAllowed ctxt) - (illegalVDQTyErr env ty) - -- Reject visible, dependent quantification in the type of a - -- term (e.g., `f :: forall a -> a -> Maybe a`) - ; check_valid_theta env' SigmaCtxt expand theta -- Allow type T = ?x::Int => Int -> Int -- but not type T = ?x::Int @@ -999,15 +988,6 @@ constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) constraintTyErr env ty = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty) --- | Reject a use of visible, dependent quantification in the type of a term. -illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) -illegalVDQTyErr env ty = - (env, vcat - [ hang (text "Illegal visible, dependent quantification" <+> - text "in the type of a term:") - 2 (ppr_tidy env ty) - , text "(GHC does not yet support this)" ] ) - -- | Reject uses of linear function arrows in kinds. linearFunKindErr :: TidyEnv -> Type -> (TidyEnv, SDoc) linearFunKindErr env ty = |