[Git][ghc/ghc][wip/sand-witch/lazy-skol] Wibbles in response to reviews
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Jan 26 13:32:39 UTC 2024
Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC
Commits:
82b49c61 by Simon Peyton Jones at 2024-01-26T13:32:19+00:00
Wibbles in response to reviews
...still incomplete
- - - - -
9 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/BasicTypes.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/Var.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -801,7 +801,7 @@ mkNakedTyConTy :: TyCon -> Type
mkNakedTyConTy tycon = TyConApp tycon []
tcMkVisFunTy :: Mult -> Type -> Type -> Type
--- Always TypeLike, user-specified multiplicity.
+-- Always TypeLike result, user-specified multiplicity.
-- Does not have the assert-checking in mkFunTy: used by the typechecker
-- to avoid looking at the result kind, which may not be zonked
tcMkVisFunTy mult arg res
=====================================
compiler/GHC/Iface/Ext/Ast.hs
=====================================
@@ -953,25 +953,6 @@ toHieHsStmtContext ctxt
TransStmtCtxt a -> toHieHsStmtContext @p a
_ -> pure []
-{-
-instance HiePass p => ToHie (HsMatchContext (GhcPass p)) where
- toHie (FunRhs{mc_fun=name}) = toHie $ C MatchBind name'
- where
- -- See a paragraph about Haddock in #20415.
- name' :: LocatedN Name
- name' = case hiePass @p of
- HieRn -> name
- HieTc -> name
- toHie (StmtCtxt a) = toHie a
- toHie _ = pure []
-
-instance HiePass p => ToHie (HsStmtContext (GhcPass p)) where
- toHie (PatGuard a) = toHie a
- toHie (ParStmtCtxt a) = toHie a
- toHie (TransStmtCtxt a) = toHie a
- toHie _ = pure []
--}
-
instance HiePass p => ToHie (PScoped (LocatedA (Pat (GhcPass p)))) where
toHie (PS rsp scope pscope lpat@(L ospan opat)) =
concatM $ getTypeNode lpat : case opat of
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -157,7 +157,9 @@ tcPolyExprCheck :: HsExpr GhcRn
-- The (Either TcSigmaType TcCompleteSig) deals with:
-- Left ty: (f e) pushes f's argument type `ty` into `e`
-- Right sig: (e :: sig) pushes `sig` into `e`
--- The Either stuff is entirely local to this function and its immeidate callers.
+-- The Either stuff is entirely local to this function and its immediate callers.
+--
+-- See Note [Skolemisation overview] in GHC.Tc.Utils.Unify
tcPolyExprCheck expr res_ty
= outer_skolemise res_ty $ \pat_tys rho_ty ->
@@ -168,11 +170,11 @@ tcPolyExprCheck expr res_ty
do { e' <- tc_body e
; return (HsPar x (L loc e')) }
- -- The special case for lambda: go to tcLambdaPatches, passing pat_tys
+ -- The special case for lambda: go to tcLambdaMatches, passing pat_tys
tc_body e@(HsLam x lam_variant matches)
= do { (wrap, matches') <- tcLambdaMatches e lam_variant matches pat_tys
(mkCheckExpType rho_ty)
- -- NB: tcLamdaMatches concludes with deep skolemisation,
+ -- NB: tcLambdaMatches concludes with deep skolemisation,
-- if DeepSubsumption is on; hence no need to do that here
; return (mkHsWrap wrap $ HsLam x lam_variant matches') }
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -295,9 +295,9 @@ tcMatch ctxt pat_tys rhs_ty match
-- We filter out type patterns because we have no use for them in HsToCore.
-- Type variable bindings have already been converted to HsWrappers.
filter_out_type_pats :: [LPat GhcTc] -> [LPat GhcTc]
- filter_out_type_pats = filterByList (map isExpFunPatTy vis_pat_tys)
+ filter_out_type_pats = filterByList (map isExpFunPatType vis_pat_tys)
where
- vis_pat_tys = filterOut isExpForAllPatTyInvis pat_tys
+ vis_pat_tys = filter isVisibleExpPatType pat_tys
-------------
tcGRHSs :: AnnoBody body
@@ -367,7 +367,7 @@ tcDoStmts MonadComp (L l stmts) res_ty
; return (HsDo res_ty MonadComp (L l stmts')) }
tcDoStmts ctxt at GhciStmtCtxt _ _ = pprPanic "tcDoStmts" (pprHsDoFlavour ctxt)
-tcBody :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
+tcBody :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTc)
tcBody body res_ty
= do { traceTc "tcBody" (ppr res_ty)
; tcPolyLExpr body res_ty
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -137,13 +137,22 @@ tcMatchPats :: forall a.
-- discharge parts of the returning LIE, and deal with pattern type
-- signatures
+-- PRECONDITION:
+-- number of visible Pats in pats (@a is invisible)
+-- =
+-- number of visible ExpPatTypes in pat_tys (ExpForAllPatTy v is visible iff b is Required)
+
-- 1. Initialise the PatState
-- 2. Check the patterns
-- 3. Check the body
-- 4. Check that no existentials escape
tcMatchPats match_ctxt pats pat_tys thing_inside
- = do { err_ctxt <- getErrCtxt
+ = assertPpr (count isVisibleExpPatType pat_tys == length pats)
+ (ppr pats $$ ppr pat_tys) $
+ -- Check PRECONDITION
+ -- When we get @patterns the (length pats) will change
+ do { err_ctxt <- getErrCtxt
; let loop :: [LPat GhcRn] -> [ExpPatType] -> TcM ([LPat GhcTc], a)
-- No more patterns; discard excess type patterns;
@@ -154,7 +163,7 @@ tcMatchPats match_ctxt pats pat_tys thing_inside
-- pats = [x, @p]
-- pat_tys = [Int, @a, @b]
loop [] pat_tys
- = assertPpr (all isExpForAllPatTyInvis pat_tys) (ppr pats $$ ppr pat_tys) $
+ = assertPpr (not (any isVisibleExpPatType pat_tys)) (ppr pats $$ ppr pat_tys) $
do { res <- setErrCtxt err_ctxt thing_inside
; return ([], res) }
@@ -167,18 +176,23 @@ tcMatchPats match_ctxt pats pat_tys thing_inside
-- ExpForAllPat: expecting a type pattern
loop (pat : pats) (ExpForAllPatTy bndr : pat_tys)
- | Bndr tv vis <- bndr, isVisibleForAllTyFlag vis
+ | Bndr tv vis <- bndr
+ , isVisibleForAllTyFlag vis
= do { (p, (ps, res)) <- tc_forall_lpat tv penv pat $
loop pats pat_tys
- ; return (p:ps, res) }
+ ; return (ps, res) }
- -- Invisible forall in type, and an @a type patters
+ -- Invisible forall in type, and an @a type pattern
-- Add an equation here when we have these
+ -- E.g. f :: forall a. Bool -> a -> blah
+ -- f @b True x = rhs1 -- b is bound to skolem a
+ -- f @c False y = rhs2 -- c is bound to skolem a
| otherwise -- Discard invisible pat_ty
= loop (pat:pats) pat_tys
loop pats@(_:_) [] = pprPanic "tcMatchPats" (ppr pats)
+ -- Failure of PRECONDITION
; loop pats pat_tys }
where
=====================================
compiler/GHC/Tc/Types/BasicTypes.hs
=====================================
@@ -99,7 +99,7 @@ instance HasOccName TcBinder where
type TcSigFun = Name -> Maybe TcSigInfo
--- TcSigInfo is simply the domain of TcSigFun
+-- TcSigInfo is simply the range of TcSigFun
data TcSigInfo = TcPatSynSig TcPatSynSig -- For a pattern synonym
| TcIdSig TcIdSig
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -33,7 +33,7 @@ module GHC.Tc.Utils.TcType (
mkCheckExpType, reconstructCheckType,
checkingExpType_maybe, checkingExpType,
- ExpPatType(..), mkInvisExpPatType, isExpForAllPatTyInvis, isExpFunPatTy,
+ ExpPatType(..), mkInvisExpPatType, isVisibleExpPatType, isExpFunPatType,
SyntaxOpType(..), synKnownType, mkSynFunTys,
@@ -465,15 +465,15 @@ data ExpPatType =
| ExpForAllPatTy ForAllTyBinder -- the binder (a::A) of forall (a::A) -> B or forall (a :: A). B
mkInvisExpPatType :: InvisTyBinder -> ExpPatType
-mkInvisExpPatType = ExpForAllPatTy . fmap Invisible
+mkInvisExpPatType (Bndr tv spec) = ExpForAllPatTy (Bndr tv (Invisible spec))
-isExpForAllPatTyInvis :: ExpPatType -> Bool
-isExpForAllPatTyInvis (ExpForAllPatTy (Bndr _ Invisible{})) = True
-isExpForAllPatTyInvis _ = False
+isVisibleExpPatType :: ExpPatType -> Bool
+isVisibleExpPatType (ExpForAllPatTy (Bndr _ vis)) = isVisibleForAllTyFlag vis
+isVisibleExpPatType _ = True
-isExpFunPatTy :: ExpPatType -> Bool
-isExpFunPatTy ExpFunPatTy{} = True
-isExpFunPatTy ExpForAllPatTy{} = False
+isExpFunPatType :: ExpPatType -> Bool
+isExpFunPatType ExpFunPatTy{} = True
+isExpFunPatType ExpForAllPatTy{} = False
reconstructCheckType :: [ExpPatType] -> ExpType -> TcType
-- Precondition: all the arguments are Check{}
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -299,10 +299,13 @@ Both ultimately handled by matchExpectedFunTys.
* For the Lambda case there are two sub-cases:
* An expression with a type signature: (\@a x y -> blah) :: hs_ty
This is handled by `GHC.Tc.Gen.Head.tcExprWithSig`, which kind-checks
- the signature and hands off `tcExprPolyCheck`.
+ the signature and hands off to `tcExprPolyCheck` vai `tcPolyLExprSig`
+ Note that the foralls at the top of hs_ty scope over the expression.
+
* A higher order call: h e, where h :: poly_ty -> blah
This is handlded by `GHC.Tc.Gen.Expr.tcPolyExpr`, which (in the
- checking case) again hands off to `tcExprPolyCheck`.
+ checking case) again hands off to `tcExprPolyCheck`. Here there is
+ no type-variable scoping to worry about.
So both sub-cases end up in `GHC.Tc.Gen.Expr.tcPolyExprCheck`
* This skolemises the /top-level/ invisible binders, but remembers
@@ -332,7 +335,7 @@ Both ultimately handled by matchExpectedFunTys.
if DeepSubsumption is on.
This corresponds to the plan: "skolemise at the '=' of a function binding or
- at the '->' of a lambda binding"
+ at the '->' of a lambda binding". (See #17594 and "Plan B2".)
Some wrinkles
@@ -727,19 +730,13 @@ matchExpectedFunTys :: forall a.
-- If exp_ty is Check {}, then [ExpPatType] and ExpRhoType results are all Check{}
-- If exp_ty is Infer {}, then [ExpPatType] and ExpRhoType results are all Infer{}
matchExpectedFunTys herald _ arity (Infer inf_res) thing_inside
- = do { arg_tys <- mapM new_infer_arg_ty [1 .. arity]
+ = do { arg_tys <- mapM (new_infer_arg_ty herald) [1 .. arity]
; res_ty <- newInferExpType
; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty
; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys
; res_ty <- readExpType res_ty
; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res
; return (mkWpCastN co, result) }
- where
- new_infer_arg_ty :: Int -> TcM (Scaled ExpSigmaTypeFRR)
- new_infer_arg_ty arg_pos -- position for error messages only
- = do { mult <- newFlexiTyVarTy multiplicityTy
- ; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
- ; return (mkScaled mult inf_hole) }
matchExpectedFunTys herald ctx arity (Check ty) thing_inside
= check 0 [] ty
@@ -775,7 +772,7 @@ matchExpectedFunTys herald ctx arity (Check ty) thing_inside
-- They do not line up with binders in the Match
thing_inside pat_tys (mkCheckExpType rho_ty) }
- -- NOW do coreView. We did do it before, so that we do not unnecessarily unwrap
+ -- NOW do coreView. We didn't do it before, so that we do not unnecessarily unwrap
-- a synonyms in the returned rho_ty
check n_so_far rev_pat_tys ty
| Just ty' <- coreView ty = check n_so_far rev_pat_tys ty'
@@ -852,6 +849,12 @@ matchExpectedFunTys herald ctx arity (Check ty) thing_inside
; co <- unifyType Nothing (mkScaledFunTys more_arg_tys res_ty) fun_ty
; return (mkWpCastN co, result) }
+new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpSigmaTypeFRR)
+new_infer_arg_ty herald arg_pos -- position for error messages only
+ = do { mult <- newFlexiTyVarTy multiplicityTy
+ ; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
+ ; return (mkScaled mult inf_hole) }
+
new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
new_check_arg_ty herald arg_pos -- Position for error messages only
= do { mult <- newFlexiTyVarTy multiplicityTy
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -714,7 +714,7 @@ Currently there are nine different uses of 'VarBndr':
data VarBndr var argf = Bndr var argf
-- See Note [The VarBndr type and its uses]
- deriving( Data, Functor )
+ deriving( Data )
-- | Variable Binder
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/82b49c619678ff946421b76a4af062b4231ab75c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/82b49c619678ff946421b76a4af062b4231ab75c
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/20240126/c6c751c4/attachment-0001.html>
More information about the ghc-commits
mailing list