[Git][ghc/ghc][wip/ghc-281-proposal-visible-foralls-proto] (proto) visible foralls in terms
Danya Rogozin
gitlab at gitlab.haskell.org
Mon Oct 19 11:12:03 UTC 2020
Danya Rogozin pushed to branch wip/ghc-281-proposal-visible-foralls-proto at Glasgow Haskell Compiler / GHC
Commits:
6f1489c6 by Daniel Rogozin at 2020-10-19T14:10:09+03:00
(proto) visible foralls in terms
- - - - -
15 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/HsToCore/Arrows.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Arrow.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/TyCl/PatSyn.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Utils/Zonk.hs
- compiler/GHC/Tc/Validity.hs
Changes:
=====================================
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
=====================================
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
=====================================
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 at MG { mg_ext = MatchGroupTc [Scaled arg_mult arg_ty] _ }) env_ids = do
+ (HsCmdLamCase _ mg at 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
=====================================
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
=====================================
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/.
=====================================
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.
--
=====================================
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 )
@@ -312,6 +313,16 @@ tcValArgs quick_look fun args
tc_arg n (EWrap wrap) = return (n, EWrap wrap)
tc_arg n (ETypeArg l hs_ty ty) = return (n+1, ETypeArg l hs_ty ty)
+ tc_arg n (EValArg { eva_loc = loc
+ , eva_arg = ValArg (L l (HsVar noExtField tvname@(L l' name)))
+ , eva_arg_ty = ty })
+ = return (n + 1, (ETypeArg loc arg' (irrelevantMult ty)))
+ where
+ arg' = HsWC { hswc_body = (L l ty_arg)
+ , hswc_ext = [name]
+ }
+ ty_arg = HsTyVar NoExtField IsPromoted tvname
+
tc_arg n eva@(EValArg { eva_arg = arg, eva_arg_ty = Scaled mult arg_ty })
= do { -- Crucial step: expose QL results before checking arg_ty
-- So far as the paper is concerned, this step applies
@@ -579,6 +590,26 @@ tcVTA fun_ty hs_ty
, debugPprType insted_ty ])
; return (ty_arg, insted_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) }
+
| otherwise
= do { (_, fun_ty) <- zonkTidyTcType emptyTidyEnv fun_ty
; failWith $
@@ -1087,5 +1118,3 @@ tcTagToEnum expr fun args app_res_ty res_ty
tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
-
-
=====================================
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
=====================================
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
=====================================
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'
=====================================
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)) []
=====================================
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 at s
-- as possible. For example, given this type synonym:
=====================================
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
=====================================
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
=====================================
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 =
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6f1489c62741b56c252e571678becd407a906c6b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6f1489c62741b56c252e571678becd407a906c6b
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201019/d0ea9932/attachment-0001.html>
More information about the ghc-commits
mailing list