[Git][ghc/ghc][wip/sand-witch/check- at -binders] fixup! Lazy skolemisation for @a-binders (17594)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Fri Dec 15 17:36:57 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/check- at -binders at Glasgow Haskell Compiler / GHC
Commits:
ca8c4869 by Andrei Borzenkov at 2023-12-15T21:36:44+04:00
fixup! Lazy skolemisation for @a-binders (17594)
- - - - -
9 changed files:
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Expr.hs-boot
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Match.hs-boot
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/Var.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -633,7 +633,7 @@ tcPolyCheck prag_fn
; mult <- tcMultAnn (HsNoMultAnn noExtField)
; (wrap_gen, (wrap_res, matches'))
<- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
- tcSkolemiseScoped ctxt (idType poly_id) $ \imp_ty_vars rho_ty ->
+ tcSkolemiseScoped ctxt (idType poly_id) $ \ty_vars rho_ty ->
-- Unwraps multiple layers; e.g
-- f :: forall a. Eq a => forall b. Ord b => blah
-- NB: tcSkolemiseScoped makes fresh type variables
@@ -646,7 +646,7 @@ tcPolyCheck prag_fn
setSrcSpanA bind_loc $
tc_matches_fun (L nm_loc (idName mono_id)) mult matches
- (map mkInvisExpPatType imp_ty_vars) (Check rho_ty)
+ (filterInvisInferredTyBndrs ty_vars) (Check rho_ty)
-- We make a funny AbsBinds, abstracting over nothing,
-- just so we have somewhere to put the SpecPrags.
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -20,7 +20,7 @@ module GHC.Tc.Gen.Expr
tcCheckMonoExpr, tcCheckMonoExprNC,
tcMonoExpr, tcMonoExprNC,
tcInferRho, tcInferRhoNC,
- tcPolyLExpr, tcPolyExpr, tcExpr,
+ tcPolyLExpr, tcPolyExpr, tcLExprWithTyVarsNC, tcExpr,
tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
tcCheckId,
) where
@@ -90,6 +90,7 @@ import GHC.Utils.Panic
import Control.Monad
import qualified Data.List.NonEmpty as NE
+import GHC.Types.Var (filterInvisInferredTyBndrs)
{-
************************************************************************
@@ -176,11 +177,24 @@ tcInferRhoNC (L loc expr)
********************************************************************* -}
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
-tcPolyExpr (HsPar x expr) res_ty
- = do { expr' <- tcPolyLExprNC expr res_ty
+tcPolyExpr expr res_ty
+ = do { traceTc "tcPolyExpr" (ppr res_ty)
+ ; (wrap, expr') <- tcSkolemiseExpType GenSigCtxt res_ty $ \bndrs res_ty ->
+ tcExprWithTyVars expr (filterInvisInferredTyBndrs bndrs) res_ty
+ ; return $ mkHsWrap wrap expr' }
+
+tcLExprWithTyVarsNC :: LHsExpr GhcRn -> [TcTyVar] -> ExpRhoType -> TcM (LHsExpr GhcTc)
+tcLExprWithTyVarsNC (L loc expr) ty_vars res_ty
+ = setSrcSpanA loc $
+ do { expr' <- tcExprWithTyVars expr ty_vars res_ty
+ ; return (L loc expr') }
+
+tcExprWithTyVars :: HsExpr GhcRn -> [TcTyVar] -> ExpRhoType -> TcM (HsExpr GhcTc)
+tcExprWithTyVars (HsPar x expr) ty_vars res_ty
+ = do { expr' <- tcLExprWithTyVarsNC expr ty_vars res_ty
; return (HsPar x expr') }
-tcPolyExpr e@(HsLam x lam_variant matches) res_ty
+tcExprWithTyVars e@(HsLam x lam_variant matches) _ res_ty
= do { (wrap, matches')
<- tcMatchLambda herald match_ctxt matches res_ty
; return (mkHsWrap wrap $ HsLam x lam_variant matches') }
@@ -188,11 +202,9 @@ tcPolyExpr e@(HsLam x lam_variant matches) res_ty
match_ctxt = MC { mc_what = LamAlt lam_variant, mc_body = tcBody }
herald = ExpectedFunTyLam lam_variant e
-tcPolyExpr expr res_ty
- = do { traceTc "tcPolyExpr" (ppr res_ty)
- ; (wrap, expr') <- tcSkolemiseExpType GenSigCtxt res_ty $ \ res_ty ->
- tcExpr expr res_ty
- ; return $ mkHsWrap wrap expr' }
+tcExprWithTyVars expr _ res_ty
+ = tcExpr expr res_ty
+
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -3,7 +3,7 @@ import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn
, SyntaxExprTc )
import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR
, SyntaxOpType
- , ExpType, ExpRhoType, ExpSigmaType )
+ , ExpType, ExpRhoType, ExpSigmaType, TcTyVar )
import GHC.Tc.Types ( TcM )
import GHC.Tc.Types.Origin ( CtOrigin )
import GHC.Core.Type ( Mult )
@@ -25,6 +25,8 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
tcPolyLExpr :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
+tcLExprWithTyVarsNC :: LHsExpr GhcRn -> [TcTyVar] -> ExpRhoType -> TcM (LHsExpr GhcTc)
+
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -30,7 +30,7 @@ module GHC.Tc.Gen.Head
, addHeadCtxt, addExprCtxt, addFunResCtxt ) where
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckMonoExprNC, tcCheckPolyExprNC )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckPolyExprNC, tcLExprWithTyVarsNC )
import GHC.Prelude
import GHC.Hs
@@ -87,6 +87,7 @@ import qualified GHC.LanguageExtensions as LangExt
import GHC.Data.Maybe
import Control.Monad
+import GHC.Types.Var (filterInvisInferredTyBndrs)
@@ -984,17 +985,9 @@ tcExprSig :: UserTypeCtxt -> LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc,
tcExprSig ctxt expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Sets the location for the implication constraint
do { let poly_ty = idType poly_id
- ; (wrap, expr') <- check_expr poly_ty
+ ; (wrap, expr') <- tcSkolemiseScoped ctxt poly_ty $ \ty_vars rho_ty ->
+ tcLExprWithTyVarsNC expr (filterInvisInferredTyBndrs ty_vars) (Check rho_ty)
; return (mkLHsWrap wrap expr', poly_ty) }
- where
- check_expr poly_ty = do
- stv <- xoptM LangExt.ScopedTypeVariables
- if stv then
- tcSkolemiseScoped ctxt poly_ty $ \_ rho_ty ->
- tcCheckMonoExprNC expr rho_ty
- else
- do { res <- tcCheckPolyExprNC expr poly_ty
- ; pure (idHsWrapper, res)}
tcExprSig _ expr sig@(PartialSig { psig_name = name, sig_loc = loc })
= setSrcSpan loc $ -- Sets the location for the implication constraint
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -106,11 +106,11 @@ tcMatchesFun fun_name mult matches = tc_matches_fun fun_name mult matches []
tc_matches_fun :: LocatedN Name -- MatchContext Id
-> Mult -- The multiplicity of the binder
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> [ExpPatType]
+ -> [TcTyVar]
-> ExpRhoType -- Expected type of function
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
-- Returns type of body
-tc_matches_fun fun_name mult matches implicit_pat_tys exp_ty
+tc_matches_fun fun_name mult matches ty_vars exp_ty
= do { -- Check that they all have the same no of arguments
-- Location is in the monad, set the caller so that
-- any inter-equation error messages get some vaguely
@@ -121,7 +121,7 @@ tc_matches_fun fun_name mult matches implicit_pat_tys exp_ty
; checkArgCounts what matches
; (wrapper, (mult_co_wrap, r)) <-
- match_expected_fun_tys herald ctxt arity implicit_pat_tys exp_ty $ \ pat_tys rhs_ty ->
+ match_expected_fun_tys herald ctxt arity ty_vars exp_ty $ \ pat_tys rhs_ty ->
-- NB: exp_type may be polymorphic, but
-- matchExpectedFunTys can cope with that
tcScalingUsage mult $
@@ -163,11 +163,21 @@ tcMatchesCase ctxt (Scaled scrut_mult scrut_ty) matches res_ty
tcMatchLambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
-> TcMatchCtxt HsExpr
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> ExpSigmaType
+ -> ExpRhoType
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
tcMatchLambda herald match_ctxt match res_ty
+ = tc_match_lambda herald match_ctxt match [] res_ty
+
+tc_match_lambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
+ -> TcMatchCtxt HsExpr
+ -> MatchGroup GhcRn (LHsExpr GhcRn)
+ -> [TcTyVar]
+ -> ExpRhoType
+ -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
+tc_match_lambda herald match_ctxt match ty_vars res_ty
= do { checkArgCounts (mc_what match_ctxt) match
- ; (wrapper, (mult_co_wrap, r)) <- matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty ->
+ ; (wrapper, (mult_co_wrap, r)) <- match_expected_fun_tys herald GenSigCtxt n_pats ty_vars res_ty $
+ \ pat_tys rhs_ty ->
-- checking argument counts since this is also used for \cases
tcMatches match_ctxt pat_tys rhs_ty match
; return (wrapper <.> mult_co_wrap, r) }
=====================================
compiler/GHC/Tc/Gen/Match.hs-boot
=====================================
@@ -1,7 +1,7 @@
module GHC.Tc.Gen.Match where
import GHC.Hs ( GRHSs, MatchGroup, LHsExpr, Mult )
import GHC.Tc.Types.Evidence ( HsWrapper )
-import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType, ExpPatType )
+import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType, TcTyVar )
import GHC.Tc.Types ( TcM )
import GHC.Hs.Extension ( GhcRn, GhcTc )
import GHC.Parser.Annotation ( LocatedN )
@@ -21,6 +21,6 @@ tcMatchesFun :: LocatedN Name
tc_matches_fun :: LocatedN Name
-> Mult
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> [ExpPatType]
+ -> [TcTyVar]
-> ExpRhoType
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -32,7 +32,8 @@ module GHC.Tc.Utils.TcType (
ExpRhoType,
checkingExpType_maybe, checkingExpType,
- ExpPatType(..), mkInvisExpPatType, isExpForAllPatTyInvis, isExpFunPatTy,
+ ExpPatType(..), mkInvisExpPatType, mkForAllPatTysFromSkolemised,
+ isExpForAllPatTyInvis, isExpFunPatTy,
SyntaxOpType(..), synKnownType, mkSynFunTys,
@@ -459,8 +460,11 @@ data ExpPatType =
ExpFunPatTy (Scaled ExpSigmaTypeFRR) -- the type A of a function A -> B
| ExpForAllPatTy ForAllTyBinder -- the binder (a::A) of forall (a::A) -> B or forall (a :: A). B
-mkInvisExpPatType :: InvisTyBinder -> ExpPatType
-mkInvisExpPatType = ExpForAllPatTy . fmap Invisible
+mkInvisExpPatType :: TcTyVar -> ExpPatType
+mkInvisExpPatType = ExpForAllPatTy . mkForAllTyBinder (Invisible SpecifiedSpec)
+
+mkForAllPatTysFromSkolemised :: [InvisTyBinder] -> [ExpPatType]
+mkForAllPatTysFromSkolemised = map mkInvisExpPatType . filterInvisInferredTyBndrs
isExpForAllPatTyInvis :: ExpPatType -> Bool
isExpForAllPatTyInvis (ExpForAllPatTy (Bndr _ Invisible{})) = True
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -383,25 +383,26 @@ match_expected_fun_tys :: forall a.
ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
-> UserTypeCtxt
-> Arity
- -> [ExpPatType] -- implicit, previously skolemised pattern types
+ -> [TcTyVar] -- implicit, previously skolemised pattern types
-> ExpRhoType
-> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- If matchExpectedFunTys n ty = (wrap, _)
-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
-- where [t1, ..., tn], ty_r are passed to the thing_inside
-match_expected_fun_tys herald ctx arity imp_pat_tys orig_ty thing_inside
+match_expected_fun_tys herald ctx arity tv_vars orig_ty thing_inside
= case orig_ty of -- go collects pat tys in reversed order
- Check ty -> go (reverse imp_pat_tys) arity ty
- _ -> defer (reverse imp_pat_tys) arity orig_ty
+ Check ty -> go imp_pat_tys arity ty
+ _ -> defer imp_pat_tys arity orig_ty
where
+ imp_pat_tys = reverse $ map mkInvisExpPatType tv_vars
-- Skolemise any /invisible/ foralls /before/ the zero-arg case
-- so that we guarantee to return a rho-type
go acc_arg_tys n ty
| (tvs, theta, _) <- tcSplitSigmaTy ty -- Invisible binders only!
, not (null tvs && null theta) -- Visible ones handled below
= do { (wrap_gen, (wrap_res, result)) <- tcTopSkolemise ctx ty $ \imp_ty_pats ty' ->
- go (reverse (map mkInvisExpPatType imp_ty_pats) ++ acc_arg_tys) n ty'
+ go (reverse (mkForAllPatTysFromSkolemised imp_ty_pats) ++ acc_arg_tys) n ty'
; return (wrap_gen <.> wrap_res, result) }
-- No more args; do this /before/ coreView, so
@@ -1560,16 +1561,16 @@ tcTopSkolemise ctxt expected_ty thing_inside
-- | Variant of 'tcTopSkolemise' that takes an ExpType
tcSkolemiseExpType :: UserTypeCtxt -> ExpSigmaType
- -> (ExpRhoType -> TcM result)
+ -> ([TcInvisTVBinder] -> ExpRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseExpType _ et@(Infer {}) thing_inside
- = (idHsWrapper, ) <$> thing_inside et
+ = (idHsWrapper, ) <$> thing_inside [] et
tcSkolemiseExpType ctxt (Check ty) thing_inside
= do { deep_subsumption <- xoptM LangExt.DeepSubsumption
; let skolemise | deep_subsumption = tcDeeplySkolemise
| otherwise = tcTopSkolemise
- ; skolemise ctxt ty $ \_ rho_ty ->
- thing_inside (Check rho_ty) }
+ ; skolemise ctxt ty $ \ty_bndrs rho_ty ->
+ thing_inside ty_bndrs (Check rho_ty) }
checkConstraints :: SkolemInfoAnon
-> [TcTyVar] -- Skolems
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -94,7 +94,8 @@ module GHC.Types.Var (
mkForAllTyBinder, mkForAllTyBinders,
mkTyVarBinder, mkTyVarBinders,
isTyVarBinder,
- tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders,
+ tyVarSpecToBinder, tyVarSpecToBinders, filterInvisInferredTyBndrs,
+ tyVarReqToBinder, tyVarReqToBinders,
mapVarBndr, mapVarBndrs,
-- ** ExportFlag
@@ -741,6 +742,9 @@ type ReqTVBinder = VarBndr TyVar ()
tyVarSpecToBinders :: [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag]
tyVarSpecToBinders = map tyVarSpecToBinder
+filterInvisInferredTyBndrs :: [InvisTyBinder] -> [TcTyVar]
+filterInvisInferredTyBndrs = binderVars . filterOut (\bndr -> binderFlag bndr == InferredSpec)
+
tyVarSpecToBinder :: VarBndr a Specificity -> VarBndr a ForAllTyFlag
tyVarSpecToBinder (Bndr tv vis) = Bndr tv (Invisible vis)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ca8c4869a22c678f81231cfa49cd82ec2fc84ee8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ca8c4869a22c678f81231cfa49cd82ec2fc84ee8
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/20231215/d3626b47/attachment-0001.html>
More information about the ghc-commits
mailing list