[Git][ghc/ghc][wip/sand-witch/lazy-skol-exp-pat-tys] Lazy skolemisation for @a-binders (17594)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Thu Dec 14 10:36:14 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/lazy-skol-exp-pat-tys at Glasgow Haskell Compiler / GHC
Commits:
1218bfa7 by Andrei Borzenkov at 2023-12-14T14:35:56+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.
- - - - -
17 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/Gen/Pat.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/Var.hs
- testsuite/tests/indexed-types/should_compile/Simple14.stderr
- testsuite/tests/rep-poly/RepPolyBackpack1.stderr
- testsuite/tests/typecheck/should_fail/tcfail068.stderr
- testsuite/tests/typecheck/should_fail/tcfail076.stderr
Changes:
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -23,7 +23,7 @@ where
import GHC.Prelude
-import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun )
+import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun, tc_matches_fun )
import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckMonoExpr )
import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind )
@@ -625,7 +625,7 @@ 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 = (L nm_loc name)
, fun_matches = matches }))
= do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
@@ -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) $ \rho_ty ->
+ tcSkolemiseScoped ctxt (idType poly_id) $ \imp_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
@@ -645,8 +645,8 @@ tcPolyCheck prag_fn
-- See Note [Relevant bindings and the binder stack]
setSrcSpanA bind_loc $
- tcMatchesFun (L nm_loc (idName mono_id)) mult matches
- (mkCheckExpType rho_ty)
+ tc_matches_fun (L nm_loc (idName mono_id)) mult matches
+ (map mkInvisExpPatType imp_ty_vars) (mkCheckExpType 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,
- tcPolyExpr, tcExpr,
+ tcPolyLExpr, tcPolyExpr, tcExpr,
tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
tcCheckId,
) where
@@ -176,6 +176,18 @@ tcInferRhoNC (L loc expr)
********************************************************************* -}
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
+tcPolyExpr (HsPar x expr) res_ty
+ = do { expr' <- tcPolyLExprNC expr res_ty
+ ; return (HsPar x expr') }
+
+tcPolyExpr 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') }
+ where
+ 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 ->
@@ -793,7 +805,7 @@ tcSynArgE :: CtOrigin
tcSynArgE orig op sigma_ty syn_ty thing_inside
= do { (skol_wrap, (result, ty_wrapper))
<- tcTopSkolemise GenSigCtxt sigma_ty
- (\ rho_ty -> go rho_ty syn_ty)
+ (\_ rho_ty -> go rho_ty syn_ty)
; return (result, skol_wrap <.> ty_wrapper) }
where
go rho_ty SynAny
=====================================
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
=====================================
@@ -984,9 +984,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
=====================================
@@ -17,6 +17,7 @@
-- | Typecheck some @Matches@
module GHC.Tc.Gen.Match
( tcMatchesFun
+ , tc_matches_fun
, tcGRHS
, tcGRHSsPat
, tcMatchesCase
@@ -38,9 +39,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
@@ -81,6 +82,7 @@ import Control.Monad
import Control.Arrow ( second )
import qualified Data.List.NonEmpty as NE
import Data.Maybe (mapMaybe)
+import GHC.Types.Var
{-
************************************************************************
@@ -99,9 +101,17 @@ tcMatchesFun :: LocatedN Name -- MatchContext Id
-> Mult -- The multiplicity of the binder
-> MatchGroup GhcRn (LHsExpr GhcRn)
-> ExpRhoType -- Expected type of function
+ -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
+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]
+ -> ExpRhoType -- Expected type of function
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
-- Returns type of body
-tcMatchesFun fun_name mult matches exp_ty
+tc_matches_fun fun_name mult matches implicit_pat_tys 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
@@ -111,7 +121,8 @@ tcMatchesFun fun_name mult matches exp_ty
traceTc "tcMatchesFun" (ppr fun_name $$ ppr mult $$ ppr exp_ty $$ ppr arity)
; checkArgCounts what matches
- ; (wrapper, (mult_co_wrap, r)) <- matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
+ ; (wrapper, (mult_co_wrap, r)) <-
+ match_expected_fun_tys herald ctxt arity implicit_pat_tys exp_ty $ \ pat_tys rhs_ty ->
-- NB: exp_type may be polymorphic, but
-- matchExpectedFunTys can cope with that
tcScalingUsage mult $
@@ -153,7 +164,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
@@ -288,8 +299,13 @@ 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 is_fun_pat_ty pat_tys)
+ filter_out_type_pats = filterByList (map is_fun_pat_ty vis_pat_tys)
where
+ vis_pat_tys = filterOut is_inv_pat_ty pat_tys
+
+ is_inv_pat_ty (ExpForAllPatTy (Bndr _ Invisible{})) = True
+ is_inv_pat_ty _ = False
+
is_fun_pat_ty ExpFunPatTy{} = True
is_fun_pat_ty ExpForAllPatTy{} = False
@@ -361,10 +377,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/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 )
+import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType, ExpPatType )
import GHC.Tc.Types ( TcM )
import GHC.Hs.Extension ( GhcRn, GhcTc )
import GHC.Parser.Annotation ( LocatedN )
@@ -17,3 +17,10 @@ tcMatchesFun :: LocatedN Name
-> MatchGroup GhcRn (LHsExpr GhcRn)
-> ExpSigmaType
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
+
+tc_matches_fun :: LocatedN Name
+ -> Mult
+ -> MatchGroup GhcRn (LHsExpr GhcRn)
+ -> [ExpPatType]
+ -> ExpRhoType
+ -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -138,11 +138,32 @@ tcPats :: HsMatchContext GhcTc
-- 3. Check the body
-- 4. Check that no existentials escape
-tcPats ctxt pats pat_tys thing_inside
- = tc_tt_lpats pat_tys penv pats thing_inside
+tcPats ctxt pats pat_tys thing_inside = do
+ pat_tys' <- filter_exp_tys pats pat_tys
+ tc_tt_lpats pat_tys' penv pats thing_inside
where
penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
+ filter_exp_tys :: [LPat GhcRn] -> [ExpPatType] -> TcM ([ExpPatType])
+
+ filter_exp_tys [] rest = pure (drop_invis_pats rest)
+
+ -- visible patterns
+ filter_exp_tys pats@(L _ _ : _) (ExpForAllPatTy (Bndr _ Invisible{}) : pat_tys) =
+ filter_exp_tys pats (drop_invis_pats pat_tys)
+ filter_exp_tys (L _ _ : pats) (p : pat_tys) = do
+ (pat_tys') <- filter_exp_tys pats pat_tys
+ pure (p : pat_tys')
+
+ -- invisible patterns
+ -- There are no at the moment
+
+ filter_exp_tys (L _ _ :_) [] =
+ panic "filter_exp_tys: expected patterns more then expected pattern types"
+
+ drop_invis_pats (ExpForAllPatTy (Bndr _ Invisible{}) : pat_tys) = drop_invis_pats pat_tys
+ drop_invis_pats pat_tys = pat_tys
+
tcInferPat :: FixedRuntimeRepContext
-> HsMatchContext GhcTc
-> LPat GhcRn
@@ -406,7 +427,9 @@ tc_tt_pat pat_ty penv (ParPat x pat) thing_inside = do
{ (pat', res) <- tc_tt_lpat pat_ty penv pat thing_inside
; return (ParPat x pat', res) }
tc_tt_pat (ExpFunPatTy pat_ty) penv pat thing_inside = tc_pat pat_ty penv pat thing_inside
-tc_tt_pat (ExpForAllPatTy tv) penv pat thing_inside = tc_forall_pat penv (pat, tv) thing_inside
+tc_tt_pat (ExpForAllPatTy (Bndr tv Required)) penv pat thing_inside = tc_forall_pat penv (pat, tv) thing_inside
+tc_tt_pat (ExpForAllPatTy (Bndr _tv Invisible{})) _penv _pat _thing_inside
+ = panic "Patterns for invisible type binders aren't supported yet"
tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
tc_forall_pat _ (EmbTyPat _ tp, tv) thing_inside
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -831,7 +831,7 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
-- See Note [Handling SPECIALISE pragmas], wrinkle 1
tcSpecWrapper ctxt poly_ty spec_ty
= do { (sk_wrap, inst_wrap)
- <- tcTopSkolemise ctxt spec_ty $ \ spec_tau ->
+ <- tcTopSkolemise ctxt spec_ty $ \_ spec_tau ->
do { (inst_wrap, tau) <- topInstantiate orig poly_ty
; _ <- unifyType Nothing spec_tau tau
-- Deliberately ignore the evidence
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Tc.Utils.Instantiate (
tcInstType, tcInstTypeBndrs,
tcSkolemiseInvisibleBndrs,
- tcInstSkolTyVars, tcInstSkolTyVarsX,
+ tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyBindrVarsX,
tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
freshenTyVarBndrs, freshenCoVarBndrsX,
@@ -172,8 +172,8 @@ In general,
topSkolemise :: SkolemInfo
-> TcSigmaType
-> TcM ( HsWrapper
- , [(Name,TyVar)] -- All skolemised variables
- , [EvVar] -- All "given"s
+ , [(Name,TcInvisTVBinder)] -- All skolemised variables
+ , [EvVar] -- All "given"s
, TcRhoType )
-- See Note [Skolemisation]
topSkolemise skolem_info ty
@@ -183,13 +183,13 @@ topSkolemise skolem_info ty
-- Why recursive? See Note [Skolemisation]
go subst wrap tv_prs ev_vars ty
- | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty
+ | (tvs, theta, inner_ty) <- tcSplitSigmaTyBindr ty
, not (null tvs && null theta)
- = do { (subst', tvs1) <- tcInstSkolTyVarsX skolem_info subst tvs
+ = do { (subst', tvs1) <- tcInstSkolTyBindrVarsX skolem_info subst tvs
; ev_vars1 <- newEvVars (substTheta subst' theta)
; go subst'
- (wrap <.> mkWpTyLams tvs1 <.> mkWpEvLams ev_vars1)
- (tv_prs ++ (map tyVarName tvs `zip` tvs1))
+ (wrap <.> mkWpTyLams (binderVars tvs1) <.> mkWpEvLams ev_vars1)
+ (tv_prs ++ (map (tyVarName . binderVar) tvs `zip` tvs1))
(ev_vars ++ ev_vars1)
inner_ty }
@@ -514,6 +514,13 @@ tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSkolTyVarsX skol_info = tcInstSkolTyVarsPushLevel skol_info False
+tcInstSkolTyBindrVarsX :: SkolemInfo -> Subst -> [VarBndr TyCoVar vis] -> TcM (Subst, [VarBndr TyCoVar vis])
+tcInstSkolTyBindrVarsX skol_info subs bndrs = do
+ (subst', bndrs') <- tcInstSkolTyVarsX skol_info subs (binderVars bndrs)
+ pure (subst', zipWith mkForAllTyBinder flags bndrs')
+ where
+ flags = binderFlags bndrs
+
tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
-- This version freshens the names and creates "super skolems";
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -55,7 +55,7 @@ module GHC.Tc.Utils.TcMType (
--------------------------------
-- Instantiation
- newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
+ newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, newMetaTyVarBndrsX,
newMetaTyVarTyVarX,
newTyVarTyVar, cloneTyVarTyVar,
newConcreteTyVarX,
@@ -1022,6 +1022,13 @@ newMetaTyVarsX :: Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
+newMetaTyVarBndrsX :: Subst -> [VarBndr TyVar vis] -> TcM (Subst, [VarBndr TcTyVar vis])
+newMetaTyVarBndrsX subst bndrs = do
+ (subst, bndrs') <- newMetaTyVarsX subst (binderVars bndrs)
+ pure (subst, zipWith mkForAllTyBinder flags bndrs')
+ where
+ flags = binderFlags bndrs
+
newMetaTyVarX :: Subst -> TyVar -> TcM (Subst, TcTyVar)
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -33,7 +33,7 @@ module GHC.Tc.Utils.TcType (
mkCheckExpType,
checkingExpType_maybe, checkingExpType,
- ExpPatType(..),
+ ExpPatType(..), mkInvisExpPatType,
SyntaxOpType(..), synKnownType, mkSynFunTys,
@@ -76,7 +76,7 @@ module GHC.Tc.Utils.TcType (
tcSplitTyConApp, tcSplitTyConApp_maybe,
tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitAppTyNoView_maybe,
- tcSplitSigmaTy, tcSplitNestedSigmaTys, tcSplitIOType_maybe,
+ tcSplitSigmaTy, tcSplitSigmaTyBindr, tcSplitNestedSigmaTys, tcSplitIOType_maybe,
---------------------------------
-- Predicates.
@@ -462,7 +462,10 @@ checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
-- Expected type of a pattern in a lambda or a function left-hand side.
data ExpPatType =
ExpFunPatTy (Scaled ExpSigmaTypeFRR) -- the type A of a function A -> B
- | ExpForAllPatTy TcTyVar -- the binder (a::A) of forall (a::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
instance Outputable ExpPatType where
ppr (ExpFunPatTy t) = ppr t
@@ -1435,6 +1438,11 @@ tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
+tcSplitSigmaTyBindr :: Type -> ([TcInvisTVBinder], ThetaType, Type)
+tcSplitSigmaTyBindr ty = case tcSplitForAllInvisTVBinders ty of
+ (tvs, rho) -> case tcSplitPhiTy rho of
+ (theta, tau) -> (tvs, theta, tau)
+
-- | Split a sigma type into its parts, going underneath as many arrows
-- and foralls as possible. See Note [tcSplitNestedSigmaTys]
tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -32,7 +32,7 @@ module GHC.Tc.Utils.Unify (
matchExpectedListTy,
matchExpectedTyConApp,
matchExpectedAppTy,
- matchExpectedFunTys,
+ matchExpectedFunTys, match_expected_fun_tys,
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
@@ -361,6 +361,15 @@ Example:
with the type signature.
-}
+matchExpectedFunTys :: forall a.
+ ExpectedFunTyOrigin
+ -> UserTypeCtxt
+ -> Arity
+ -> ExpRhoType
+ -> ([ExpPatType] -> ExpRhoType -> TcM a)
+ -> TcM (HsWrapper, a)
+matchExpectedFunTys herald ctx arity = match_expected_fun_tys herald ctx arity []
+
-- | Use this function to split off arguments types when you have an
-- \"expected\" type.
--
@@ -370,28 +379,29 @@ Example:
-- to a list of argument types which all have a syntactically fixed RuntimeRep
-- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
-- See Note [Return arguments with a fixed RuntimeRep].
-matchExpectedFunTys :: forall a.
- ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
+match_expected_fun_tys :: forall a.
+ ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
-> UserTypeCtxt
-> Arity
- -> ExpRhoType -- Skolemised
+ -> [ExpPatType] -- 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
-matchExpectedFunTys herald ctx arity orig_ty thing_inside
- = case orig_ty of
- Check ty -> go [] arity ty
- _ -> defer [] arity orig_ty
+match_expected_fun_tys herald ctx arity imp_pat_tys 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
where
-- 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 $ \ty' ->
- go acc_arg_tys n ty'
+ = do { (wrap_gen, (wrap_res, result)) <- tcTopSkolemise ctx ty $ \imp_ty_pats ty' ->
+ go (acc_arg_tys ++ reverse (map mkInvisExpPatType imp_ty_pats)) n ty'
; return (wrap_gen <.> wrap_res, result) }
-- No more args; do this /before/ coreView, so
@@ -416,7 +426,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
go acc_arg_tys n (FunTy { ft_af = af, ft_mult = mult, ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
- do { let arg_pos = 1 + length acc_arg_tys -- for error messages only
+ do { let arg_pos = 1 + length (filterOut is_invis_pat_ty acc_arg_tys) -- for error messages only
; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
; (wrap_res, result) <- go ((ExpFunPatTy $ Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
(n-1) res_ty
@@ -456,14 +466,14 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
; let ty' = substTy subst' ty
; (ev_binds, (wrap_res, result)) <-
checkConstraints (getSkolemInfo skol_info) [tv'] [] $
- go (ExpForAllPatTy tv' : acc_arg_tys) (n - 1) ty'
+ go (ExpForAllPatTy (mkForAllTyBinder Required tv') : acc_arg_tys) (n - 1) ty'
; let wrap_gen = mkWpVisTyLam tv' ty' <.> mkWpLet ev_binds
; return (wrap_gen <.> wrap_res, result) }
------------
defer :: [ExpPatType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer acc_arg_tys n fun_ty
- = do { let last_acc_arg_pos = length acc_arg_tys
+ = do { let last_acc_arg_pos = length (filterOut is_invis_pat_ty acc_arg_tys)
; more_arg_tys <- mapM new_exp_arg_ty [last_acc_arg_pos + 1 .. last_acc_arg_pos + n]
; res_ty <- newInferExpType
; result <- thing_inside (reverse acc_arg_tys ++ map ExpFunPatTy more_arg_tys) res_ty
@@ -479,14 +489,17 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
= mkScaled <$> newFlexiTyVarTy multiplicityTy
<*> newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
+ is_invis_pat_ty (ExpForAllPatTy (Bndr _ Invisible{})) = True
+ is_invis_pat_ty _ = False
+
------------
mk_ctxt :: [ExpPatType] -> TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_ctxt arg_tys res_ty env
= mkFunTysMsg env herald arg_tys' res_ty arity
where
- arg_tys' = map prepare_arg_ty (reverse arg_tys)
+ arg_tys' = map prepare_arg_ty (reverse (filterOut is_invis_pat_ty arg_tys))
prepare_arg_ty (ExpFunPatTy (Scaled u v)) = Anon (Scaled u (checkingExpType "matchExpectedFunTys" v)) visArgTypeLike
- prepare_arg_ty (ExpForAllPatTy tv) = Named (Bndr tv Required)
+ prepare_arg_ty (ExpForAllPatTy tv) = Named tv
-- this is safe b/c we're called from "go"
mkFunTysMsg :: TidyEnv
@@ -1046,7 +1059,7 @@ tc_sub_type_shallow unify inst_orig ctxt ty_actual ty_expected
, text "ty_expected =" <+> ppr ty_expected ]
; (sk_wrap, inner_wrap)
- <- tcTopSkolemise ctxt ty_expected $ \ sk_rho ->
+ <- tcTopSkolemise ctxt ty_expected $ \_ sk_rho ->
do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
; cow <- unify rho_a sk_rho
; return (mkWpCastN cow <.> wrap) }
@@ -1069,7 +1082,7 @@ tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
, text "ty_expected =" <+> ppr ty_expected ]
; (sk_wrap, inner_wrap)
- <- tcDeeplySkolemise ctxt ty_expected $ \ sk_rho ->
+ <- tcDeeplySkolemise ctxt ty_expected $ \_ sk_rho ->
-- See Note [Deep subsumption]
tc_sub_type_ds unify inst_orig ctxt ty_actual sk_rho
@@ -1372,7 +1385,7 @@ tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
tcDeeplySkolemise
:: UserTypeCtxt -> TcSigmaType
- -> (TcType -> TcM result)
+ -> ([TcInvisTVBinder] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
-- ^ The wrapper has type: spec_ty ~> expected_ty
-- Just like tcTopSkolemise, but calls
@@ -1380,29 +1393,16 @@ tcDeeplySkolemise
-- See Note [Deep skolemisation]
tcDeeplySkolemise ctxt expected_ty thing_inside
| isTauTy expected_ty -- Short cut for common case
- = do { res <- thing_inside expected_ty
+ = do { res <- thing_inside [] expected_ty
; return (idHsWrapper, res) }
| otherwise
- = do { -- This (unpleasant) rec block allows us to pass skol_info to deeplySkolemise;
- -- but skol_info can't be built until we have tv_prs
- rec { (wrap, tv_prs, given, rho_ty) <- deeplySkolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
-
- ; traceTc "tcDeeplySkolemise" (ppr expected_ty $$ ppr rho_ty $$ ppr tv_prs)
-
- ; let skol_tvs = map snd tv_prs
- ; (ev_binds, result)
- <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- thing_inside rho_ty
-
- ; return (wrap <.> mkWpLet ev_binds, result) }
- -- The ev_binds returned by checkConstraints is very
- -- often empty, in which case mkWpLet is a no-op
+ = tcSkolemiseGeneral deeplySkolemise ctxt expected_ty (\tv_prs tc_ty ->
+ thing_inside (map snd tv_prs) tc_ty)
deeplySkolemise :: SkolemInfo -> TcSigmaType
-> TcM ( HsWrapper
- , [(Name,TyVar)] -- All skolemised variables
- , [EvVar] -- All "given"s
+ , [(Name,TcInvisTVBinder)] -- All skolemised variables
+ , [EvVar] -- All "given"s
, TcRhoType )
-- See Note [Deep skolemisation]
deeplySkolemise skol_info ty
@@ -1411,14 +1411,14 @@ deeplySkolemise skol_info ty
init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
go subst ty
- | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
+ | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTyBndr_maybe ty
= do { let arg_tys' = substScaledTys subst arg_tys
; ids1 <- newSysLocalIds (fsLit "dk") arg_tys'
- ; (subst', tvs1) <- tcInstSkolTyVarsX skol_info subst tvs
+ ; (subst', tvs1) <- tcInstSkolTyBindrVarsX skol_info subst tvs
; ev_vars1 <- newEvVars (substTheta subst' theta)
; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty'
- ; let tv_prs1 = map tyVarName tvs `zip` tvs1
- ; return ( mkWpEta ids1 (mkWpTyLams tvs1
+ ; let tv_prs1 = map (tyVarName . binderVar) tvs `zip` tvs1
+ ; return ( mkWpEta ids1 (mkWpTyLams (binderVars tvs1)
<.> mkWpEvLams ev_vars1
<.> wrap)
, tv_prs1 ++ tvs_prs2
@@ -1450,21 +1450,31 @@ deeplyInstantiate orig ty
= do { let ty' = substTy subst ty
; return (idHsWrapper, ty') }
-tcDeepSplitSigmaTy_maybe
- :: TcSigmaType -> Maybe ([Scaled TcType], [TyVar], ThetaType, TcSigmaType)
+
+
+tcDeepSplit_maybe :: (Type -> ([a], ThetaType, Type)) -> TcSigmaType -> Maybe ([Scaled TcType], [a], ThetaType, TcSigmaType)
-- Looks for a *non-trivial* quantified type, under zero or more function arrows
-- By "non-trivial" we mean either tyvars or constraints are non-empty
-tcDeepSplitSigmaTy_maybe ty
- | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
- , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
- = Just (arg_ty:arg_tys, tvs, theta, rho)
+tcDeepSplit_maybe splitter = go where
+ go ty
+ | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
+ , Just (arg_tys, tvs, theta, rho) <- go res_ty
+ = Just (arg_ty:arg_tys, tvs, theta, rho)
+
+ | (tvs, theta, rho) <- splitter ty
+ , not (null tvs && null theta)
+ = Just ([], tvs, theta, rho)
- | (tvs, theta, rho) <- tcSplitSigmaTy ty
- , not (null tvs && null theta)
- = Just ([], tvs, theta, rho)
+ | otherwise = Nothing
- | otherwise = Nothing
+tcDeepSplitSigmaTy_maybe
+ :: TcSigmaType -> Maybe ([Scaled TcType], [TyVar], ThetaType, TcSigmaType)
+tcDeepSplitSigmaTy_maybe = tcDeepSplit_maybe tcSplitSigmaTy
+
+tcDeepSplitSigmaTyBndr_maybe
+ :: TcSigmaType -> Maybe ([Scaled TcType], [TcInvisTVBinder], ThetaType, TcSigmaType)
+tcDeepSplitSigmaTyBndr_maybe = tcDeepSplit_maybe tcSplitSigmaTyBindr
{- *********************************************************************
@@ -1504,9 +1514,30 @@ tcSkolemiseScoped is very similar, but differs in two ways:
See Note [When to build an implication] below.
-}
+tcSkolemiseGeneral ::
+ (SkolemInfo -> TcType -> TcM (HsWrapper, [(Name, VarBndr TcTyVar vis)], [EvVar], TcType))
+ -> UserTypeCtxt
+ -> TcType
+ -> ([(Name, VarBndr TcTyVar vis)] -> TcType -> IOEnv (Env TcGblEnv TcLclEnv) result)
+ -> TcM (HsWrapper, result)
+tcSkolemiseGeneral skolemise ctxt expected_ty thing_inside
+ = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty
+ ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty (map (fmap binderVar) tv_prs)) }
+
+ ; let skol_tvs = map (binderVar . snd) tv_prs
+ ; (ev_binds, result)
+ <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
+ thing_inside tv_prs rho_ty
+
+ ; return (wrap <.> mkWpLet ev_binds, result) }
+ -- The ev_binds returned by checkConstraints is very
+ -- often empty, in which case mkWpLet is a no-op
+
tcTopSkolemise, tcSkolemiseScoped
:: UserTypeCtxt -> TcSigmaType
- -> (TcType -> TcM result)
+ -> ([TcInvisTVBinder] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
-- ^ The wrapper has type: spec_ty ~> expected_ty
-- See Note [Skolemisation] for the differences between
@@ -1516,37 +1547,17 @@ tcSkolemiseScoped ctxt expected_ty thing_inside
= do { deep_subsumption <- xoptM LangExt.DeepSubsumption
; let skolemise | deep_subsumption = deeplySkolemise
| otherwise = topSkolemise
- ; -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
- -- in GHC.Tc.Utils.TcType
- rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
-
- ; let skol_tvs = map snd tv_prs
- ; (ev_binds, res)
- <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- tcExtendNameTyVarEnv tv_prs $
- thing_inside rho_ty
-
- ; return (wrap <.> mkWpLet ev_binds, res) }
+ ; tcSkolemiseGeneral skolemise ctxt expected_ty $ \tv_prs rho_ty ->
+ tcExtendNameTyVarEnv (map (fmap binderVar) tv_prs) $
+ thing_inside (map snd tv_prs) rho_ty }
tcTopSkolemise ctxt expected_ty thing_inside
| isRhoTy expected_ty -- Short cut for common case
- = do { res <- thing_inside expected_ty
+ = do { res <- thing_inside [] expected_ty
; return (idHsWrapper, res) }
| otherwise
- = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
- -- in GHC.Tc.Utils.TcType
- rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
-
- ; let skol_tvs = map snd tv_prs
- ; (ev_binds, result)
- <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- thing_inside rho_ty
-
- ; return (wrap <.> mkWpLet ev_binds, result) }
- -- The ev_binds returned by checkConstraints is very
- -- often empty, in which case mkWpLet is a no-op
+ = tcSkolemiseGeneral topSkolemise ctxt expected_ty $ \tv_prs rho_ty ->
+ thing_inside (map snd tv_prs) rho_ty
-- | Variant of 'tcTopSkolemise' that takes an ExpType
tcSkolemiseExpType :: UserTypeCtxt -> ExpSigmaType
@@ -1558,7 +1569,7 @@ tcSkolemiseExpType ctxt (Check ty) thing_inside
= do { deep_subsumption <- xoptM LangExt.DeepSubsumption
; let skolemise | deep_subsumption = tcDeeplySkolemise
| otherwise = tcTopSkolemise
- ; skolemise ctxt ty $ \rho_ty ->
+ ; skolemise ctxt ty $ \_ rho_ty ->
thing_inside (mkCheckExpType rho_ty) }
checkConstraints :: SkolemInfoAnon
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -8,6 +8,7 @@
{-# LANGUAGE FlexibleContexts, MultiWayIf, FlexibleInstances, DeriveDataTypeable,
PatternSynonyms, BangPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+{-# LANGUAGE DeriveFunctor #-}
-- |
-- #name_types#
@@ -714,7 +715,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 )
+ deriving( Data, Functor )
-- | Variable Binder
--
=====================================
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/rep-poly/RepPolyBackpack1.stderr
=====================================
@@ -1,6 +1,6 @@
[1 of 1] Processing number-unknown
- [1 of 2] Compiling NumberUnknown[sig] ( number-unknown\NumberUnknown.hsig, nothing )
- [2 of 2] Compiling NumberStuff ( number-unknown\NumberStuff.hs, nothing )
+ [1 of 2] Compiling NumberUnknown[sig] ( number-unknown/NumberUnknown.hsig, nothing )
+ [2 of 2] Compiling NumberStuff ( number-unknown/NumberStuff.hs, nothing )
RepPolyBackpack1.bkp:17:5: error: [GHC-55287]
The second pattern in the equation for ‘funcA’
=====================================
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/1218bfa7560e41c7be95b866e67a36f385f2aca8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1218bfa7560e41c7be95b866e67a36f385f2aca8
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/20231214/daa287e8/attachment-0001.html>
More information about the ghc-commits
mailing list