[Git][ghc/ghc][wip/ghc-281-proposal-visible-foralls-proto] (proto) visible foralls in terms

Danya Rogozin gitlab at gitlab.haskell.org
Tue Oct 20 12:33:42 UTC 2020



Danya Rogozin pushed to branch wip/ghc-281-proposal-visible-foralls-proto at Glasgow Haskell Compiler / GHC


Commits:
ea1d5fb5 by Daniel Rogozin at 2020-10-20T15:33:17+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 )
@@ -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
-
-


=====================================
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/ea1d5fb5512dcc7cbd7ee385f6bb51320875bc16

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ea1d5fb5512dcc7cbd7ee385f6bb51320875bc16
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/20201020/799d80c7/attachment-0001.html>


More information about the ghc-commits mailing list