[Git][ghc/ghc][wip/sand-witch/lazy-skol] Lazy skolemisation for @a-binders (17594)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Tue Sep 12 11:26:38 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC
Commits:
2329ee2a by Andrei Borzenkov at 2023-09-12T15:25:53+04:00
Lazy skolemisation for @a-binders (17594)
This patch is a preparation for @a-binders implementation.
We have to accept SigmaType in matchExpectedFunTys function
to implement them. To achieve that, I made skolemization more
lazy. This leads to
- Changing tcPolyCheck function. Now skolemisation is performed only in
case ScopedTypeVariables extension enabled.
- Changing tcExprSig function in the same way as tcPolyCheck
- Changing tcPolyExpr function. Now it goes dipper into type if type
actually is
1) HsPar
2) HsLam
3) HsLamCase
In all other cases tcPolyExpr immediately skolemises a type as it was
previously.
These changes would allow lambdas to accept invisible type arguments
in the most interesting contexts.
- - - - -
16 changed files:
- compiler/GHC/Tc/Deriv.hs
- 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/Utils/Unify.hs
- testsuite/tests/indexed-types/should_compile/Simple14.stderr
- testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr
- testsuite/tests/typecheck/should_fail/T14618.stderr
- testsuite/tests/typecheck/should_fail/T16414.stderr
- testsuite/tests/typecheck/should_fail/T19977a.stderr
- testsuite/tests/typecheck/should_fail/T19977b.stderr
- testsuite/tests/typecheck/should_fail/T3950.stderr
- testsuite/tests/typecheck/should_fail/tcfail068.stderr
- testsuite/tests/typecheck/should_fail/tcfail076.stderr
Changes:
=====================================
compiler/GHC/Tc/Deriv.hs
=====================================
@@ -1893,6 +1893,8 @@ genInstBinds spec@(DS { ds_tvs = tyvars, ds_mechanism = mechanism
-- Skip unboxed tuples checking for derived instances when imported
-- in a different module, see #20524
, LangExt.UnboxedTuples
+ -- Enable eager skolemisation to bring type variable into scope
+ , LangExt.ScopedTypeVariables
]
| otherwise
= []
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -4,6 +4,7 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiWayIf #-}
{-
(c) The University of Glasgow 2006
@@ -610,27 +611,14 @@ tcPolyCheck prag_fn
(CompleteSig { sig_bndr = poly_id
, sig_ctxt = ctxt
, sig_loc = sig_loc })
- (L bind_loc (FunBind { fun_id = L nm_loc name
+ (L bind_loc (FunBind { fun_id = lname@(L nm_loc name)
, fun_matches = matches }))
= do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
; mono_name <- newNameAt (nameOccName name) (locA nm_loc)
; (wrap_gen, (wrap_res, matches'))
<- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
- tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
- -- Unwraps multiple layers; e.g
- -- f :: forall a. Eq a => forall b. Ord b => blah
- -- NB: tcSkolemiseScoped makes fresh type variables
- -- See Note [Instantiate sig with fresh variables]
-
- let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
- tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
- -- Why mono_id in the BinderStack?
- -- See Note [Relevant bindings and the binder stack]
-
- setSrcSpanA bind_loc $
- tcMatchesFun (L nm_loc (idName mono_id)) matches
- (mkCheckExpType rho_ty)
+ tc_matches_fun_check ctxt bind_loc lname poly_id matches
-- We make a funny AbsBinds, abstracting over nothing,
-- just so we have somewhere to put the SpecPrags.
@@ -669,6 +657,42 @@ tcPolyCheck prag_fn
tcPolyCheck _prag_fn sig bind
= pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)
+
+tc_matches_fun_check :: UserTypeCtxt
+ -> SrcSpanAnnA
+ -> LocatedN Name
+ -> TcId
+ -> MatchGroup GhcRn (LHsExpr GhcRn)
+ -> TcM (HsWrapper, (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc)))
+tc_matches_fun_check ctxt bind_loc (L nm_loc name) poly_id matches = do
+ scope_forall <- xoptM LangExt.ScopedTypeVariables
+ if | not scope_forall -> lazy_skolemisation_way
+ | otherwise -> eager_skolemisation_way
+ where
+ lazy_skolemisation_way = do
+ new_poly_name <- newNameAt (nameOccName name) (locA nm_loc)
+ res <- setSrcSpanA bind_loc $
+ tcMatchesFun (L nm_loc new_poly_name) matches
+ (mkCheckExpType (idType poly_id))
+ pure (idHsWrapper, res)
+
+ eager_skolemisation_way = do
+ mono_name <- newNameAt (nameOccName name) (locA nm_loc)
+ tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
+ -- Unwraps multiple layers; e.g
+ -- f :: forall a. Eq a => forall b. Ord b => blah
+ -- NB: tcSkolemiseScoped makes fresh type variables
+ -- See Note [Instantiate sig with fresh variables]
+
+ let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
+ tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
+ -- Why mono_id in the BinderStack?
+ -- See Note [Relevant bindings and the binder stack]
+
+ setSrcSpanA bind_loc $
+ tcMatchesFun (L nm_loc mono_name) matches
+ (mkCheckExpType rho_ty)
+
funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]
-> TcM [CoreTickish]
funBindTicks loc fun_id mod sigs
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -20,7 +20,7 @@ module GHC.Tc.Gen.Expr
tcCheckMonoExpr, tcCheckMonoExprNC,
tcMonoExpr, tcMonoExprNC,
tcInferRho, tcInferRhoNC,
- tcPolyExpr, tcExpr,
+ tcPolyLExpr, tcPolyExpr, tcExpr,
tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
tcCheckId,
) where
@@ -177,6 +177,25 @@ tcInferRhoNC (L loc expr)
********************************************************************* -}
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
+tcPolyExpr (HsPar x lpar expr rpar) res_ty
+ = do { expr' <- tcPolyLExprNC expr res_ty
+ ; return (HsPar x lpar expr' rpar) }
+
+tcPolyExpr (HsLam _ match) res_ty
+ = do { (wrap, match') <- tcMatchLambda herald match_ctxt match res_ty
+ ; return (mkHsWrap wrap (HsLam noExtField match')) }
+ where
+ match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody }
+ herald = ExpectedFunTyLam match
+
+tcPolyExpr e@(HsLamCase x lc_variant matches) res_ty
+ = do { (wrap, matches')
+ <- tcMatchLambda herald match_ctxt matches res_ty
+ ; return (mkHsWrap wrap $ HsLamCase x lc_variant matches') }
+ where
+ match_ctxt = MC { mc_what = LamCaseAlt lc_variant, mc_body = tcBody }
+ herald = ExpectedFunTyLamCase lc_variant e
+
tcPolyExpr expr res_ty
= do { traceTc "tcPolyExpr" (ppr res_ty)
; (wrap, expr') <- tcSkolemiseExpType GenSigCtxt res_ty $ \ res_ty ->
=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -23,6 +23,8 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
-> TcRhoType
-> TcM (LHsExpr GhcTc)
+tcPolyLExpr :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
+
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
@@ -42,4 +44,3 @@ tcSyntaxOpGen :: CtOrigin
-> SyntaxOpType
-> ([TcSigmaTypeFRR] -> [Mult] -> TcM a)
-> TcM (a, SyntaxExprTc)
-
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -86,6 +86,7 @@ import GHC.Utils.Panic.Plain
import GHC.Data.Maybe
import Control.Monad
+import qualified GHC.LanguageExtensions as LangExt
@@ -984,9 +985,17 @@ 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') <- tcSkolemiseScoped ctxt poly_ty $ \rho_ty ->
- tcCheckMonoExprNC expr rho_ty
+ ; (wrap, expr') <- check_expr poly_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
=====================================
@@ -38,9 +38,9 @@ where
import GHC.Prelude
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC
- , tcMonoExpr, tcMonoExprNC, tcExpr
+ , tcMonoExprNC, tcExpr
, tcCheckMonoExpr, tcCheckMonoExprNC
- , tcCheckPolyExpr )
+ , tcCheckPolyExpr, tcPolyLExpr )
import GHC.Rename.Utils ( bindLocalNames, isIrrefutableHsPatRn )
import GHC.Tc.Errors.Types
@@ -97,7 +97,7 @@ same number of arguments before using @tcMatches@ to do the work.
tcMatchesFun :: LocatedN Name -- MatchContext Id
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> ExpRhoType -- Expected type of function
+ -> ExpSigmaType -- Expected type of function
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
-- Returns type of body
tcMatchesFun fun_name matches exp_ty
@@ -155,7 +155,7 @@ 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)
- -> ExpRhoType
+ -> ExpSigmaType
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
tcMatchLambda herald match_ctxt match res_ty
= do { checkArgCounts (mc_what match_ctxt) match
@@ -350,10 +350,10 @@ 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 -> ExpRhoType -> TcM (LHsExpr GhcTc)
+tcBody :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
tcBody body res_ty
= do { traceTc "tcBody" (ppr res_ty)
- ; tcMonoExpr body res_ty
+ ; tcPolyLExpr body res_ty
}
{-
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -375,8 +375,8 @@ matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
-> UserTypeCtxt
-> Arity
- -> ExpRhoType -- Skolemised
- -> ([ExpPatType] -> ExpRhoType -> TcM a)
+ -> ExpSigmaType
+ -> ([ExpPatType] -> ExpSigmaType -> TcM a)
-> TcM (HsWrapper, a)
-- If matchExpectedFunTys n ty = (wrap, _)
-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
@@ -386,8 +386,8 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
Check ty -> go [] arity ty
_ -> defer [] arity orig_ty
where
- -- Skolemise any /invisible/ foralls /before/ the zero-arg case
- -- so that we guarantee to return a rho-type
+
+ -- Skolemise any /invisible/ foralls, before 0-arity case
go acc_arg_tys n ty
| (tvs, theta, _) <- tcSplitSigmaTy ty -- Invisible binders only!
, not (null tvs && null theta) -- Visible ones handled below
@@ -1525,7 +1525,7 @@ tcSkolemiseScoped ctxt expected_ty thing_inside
; let skol_tvs = map snd tv_prs
; (ev_binds, res)
<- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- tcExtendNameTyVarEnv tv_prs $
+ tcExtendNameTyVarEnv tv_prs $
thing_inside rho_ty
; return (wrap <.> mkWpLet ev_binds, res) }
=====================================
testsuite/tests/indexed-types/should_compile/Simple14.stderr
=====================================
@@ -7,7 +7,7 @@ Simple14.hs:22:27: error: [GHC-83865]
inside the constraints: Maybe m ~ Maybe n
bound by a type expected by the context:
(Maybe m ~ Maybe n) => EQ_ z0 z0
- at Simple14.hs:22:26-41
+ at Simple14.hs:22:27-40
‘n’ is a rigid type variable bound by
the type signature for:
foo :: forall m n. EQ_ (Maybe m) (Maybe n)
=====================================
testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr
=====================================
@@ -2,23 +2,20 @@
NamedWildcardsNotEnabled.hs:5:9: error: [GHC-25897]
• Couldn't match expected type ‘_b’ with actual type ‘Bool’
‘_b’ is a rigid type variable bound by
- the type signature for:
- foo :: forall _a _b. _a -> _b
- at NamedWildcardsNotEnabled.hs:4:1-15
+ a type expected by the context:
+ forall _a _b. _a -> _b
+ at NamedWildcardsNotEnabled.hs:5:1-13
• In the expression: not x
In an equation for ‘foo’: foo x = not x
- • Relevant bindings include
- foo :: _a -> _b (bound at NamedWildcardsNotEnabled.hs:5:1)
NamedWildcardsNotEnabled.hs:5:13: error: [GHC-25897]
• Couldn't match expected type ‘Bool’ with actual type ‘_a’
‘_a’ is a rigid type variable bound by
- the type signature for:
- foo :: forall _a _b. _a -> _b
- at NamedWildcardsNotEnabled.hs:4:1-15
+ a type expected by the context:
+ forall _a _b. _a -> _b
+ at NamedWildcardsNotEnabled.hs:5:1-13
• In the first argument of ‘not’, namely ‘x’
In the expression: not x
In an equation for ‘foo’: foo x = not x
• Relevant bindings include
x :: _a (bound at NamedWildcardsNotEnabled.hs:5:5)
- foo :: _a -> _b (bound at NamedWildcardsNotEnabled.hs:5:1)
=====================================
testsuite/tests/typecheck/should_fail/T14618.stderr
=====================================
@@ -2,13 +2,13 @@
T14618.hs:7:14: error: [GHC-25897]
• Couldn't match expected type ‘b’ with actual type ‘a’
‘a’ is a rigid type variable bound by
- the type signature for:
- safeCoerce :: forall a b. a -> b
- at T14618.hs:6:1-20
+ a type expected by the context:
+ forall a b. a -> b
+ at T14618.hs:(7,1)-(12,14)
‘b’ is a rigid type variable bound by
- the type signature for:
- safeCoerce :: forall a b. a -> b
- at T14618.hs:6:1-20
+ a type expected by the context:
+ forall a b. a -> b
+ at T14618.hs:(7,1)-(12,14)
• In the expression: f'
In an equation for ‘safeCoerce’:
safeCoerce
@@ -17,5 +17,3 @@ T14618.hs:7:14: error: [GHC-25897]
f :: d -> forall c. d
f x = x
f' = f
- • Relevant bindings include
- safeCoerce :: a -> b (bound at T14618.hs:7:1)
=====================================
testsuite/tests/typecheck/should_fail/T16414.stderr
=====================================
@@ -3,9 +3,9 @@ T16414.hs:15:6: error: [GHC-43085]
• Overlapping instances for AllZip2 f0 arising from a use of ‘f2’
Matching givens (or their superclasses):
AllZip2 I
- bound by the type signature for:
- f1 :: forall x. (All x, AllZip2 I) => x -> ()
- at T16414.hs:14:1-35
+ bound by a type expected by the context:
+ forall x. (All x, AllZip2 I) => x -> ()
+ at T16414.hs:15:1-7
Matching instance:
instance AllZip2 f -- Defined at T16414.hs:12:10
(The choice depends on the instantiation of ‘f0’)
=====================================
testsuite/tests/typecheck/should_fail/T19977a.stderr
=====================================
@@ -2,12 +2,12 @@
T19977a.hs:11:7: error: [GHC-39999]
• Could not deduce ‘Show a’ arising from a use of ‘f’
from the context: Show [a]
- bound by the type signature for:
- g :: forall a. Show [a] => a -> String
- at T19977a.hs:10:1-28
+ bound by a type expected by the context:
+ forall a. Show [a] => a -> String
+ at T19977a.hs:11:1-9
Possible fix:
add (Show a) to the context of
- the type signature for:
- g :: forall a. Show [a] => a -> String
+ a type expected by the context:
+ forall a. Show [a] => a -> String
• In the expression: f x
In an equation for ‘g’: g x = f x
=====================================
testsuite/tests/typecheck/should_fail/T19977b.stderr
=====================================
@@ -2,12 +2,12 @@
T19977b.hs:21:5: error: [GHC-39999]
• Could not deduce ‘C a’ arising from a use of ‘h’
from the context: D a
- bound by the type signature for:
- g :: forall a. D a => a
- at T19977b.hs:20:1-13
+ bound by a type expected by the context:
+ forall a. D a => a
+ at T19977b.hs:21:1-5
Possible fix:
add (C a) to the context of
- the type signature for:
- g :: forall a. D a => a
+ a type expected by the context:
+ forall a. D a => a
• In the expression: h
In an equation for ‘g’: g = h
=====================================
testsuite/tests/typecheck/should_fail/T3950.stderr
=====================================
@@ -12,5 +12,3 @@ T3950.hs:16:13: error: [GHC-83865]
where
rp' :: Sealed (Id p x)
rp' = undefined
- • Relevant bindings include
- rp :: Bool -> Maybe (w (Id p)) (bound at T3950.hs:16:1)
=====================================
testsuite/tests/typecheck/should_fail/tcfail068.stderr
=====================================
@@ -6,7 +6,7 @@ tcfail068.hs:14:9: error: [GHC-25897]
‘s1’ is a rigid type variable bound by
a type expected by the context:
forall s1. GHC.ST.ST s1 (IndTree s a)
- at tcfail068.hs:(13,15)-(14,31)
+ at tcfail068.hs:14:9-30
‘s’ is a rigid type variable bound by
the type signature for:
itgen :: forall a s.
@@ -29,7 +29,7 @@ tcfail068.hs:19:21: error: [GHC-25897]
‘s1’ is a rigid type variable bound by
a type expected by the context:
forall s1. GHC.ST.ST s1 (IndTree s a)
- at tcfail068.hs:(18,15)-(21,19)
+ at tcfail068.hs:(19,9)-(21,18)
‘s’ is a rigid type variable bound by
the type signature for:
itiap :: forall a s.
@@ -53,7 +53,7 @@ tcfail068.hs:24:36: error: [GHC-25897]
‘s1’ is a rigid type variable bound by
a type expected by the context:
forall s1. GHC.ST.ST s1 (IndTree s a)
- at tcfail068.hs:24:35-46
+ at tcfail068.hs:24:36-45
‘s’ is a rigid type variable bound by
the type signature for:
itrap :: forall a s.
@@ -90,7 +90,7 @@ tcfail068.hs:36:46: error: [GHC-25897]
‘s1’ is a rigid type variable bound by
a type expected by the context:
forall s1. GHC.ST.ST s1 (c, IndTree s b)
- at tcfail068.hs:36:45-63
+ at tcfail068.hs:36:46-62
‘s’ is a rigid type variable bound by
the type signature for:
itrapstate :: forall b a c s.
=====================================
testsuite/tests/typecheck/should_fail/tcfail076.stderr
=====================================
@@ -6,11 +6,11 @@ tcfail076.hs:19:82: error: [GHC-25897]
‘res1’ is a rigid type variable bound by
a type expected by the context:
forall res1. (b -> m res1) -> m res1
- at tcfail076.hs:19:71-88
+ at tcfail076.hs:19:72-87
‘res’ is a rigid type variable bound by
a type expected by the context:
forall res. (a -> m res) -> m res
- at tcfail076.hs:19:35-96
+ at tcfail076.hs:19:36-95
• In the expression: cont a
In the first argument of ‘KContT’, namely ‘(\ cont' -> cont a)’
In the expression: KContT (\ cont' -> cont a)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2329ee2a62fce6b0b9002109d355b1cdfa25f532
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2329ee2a62fce6b0b9002109d355b1cdfa25f532
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/20230912/862f622c/attachment-0001.html>
More information about the ghc-commits
mailing list