[Git][ghc/ghc][wip/sand-witch/lazy-skol] Move implicationNeeded check to tcSkolemiseGeneral

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC


Commits:
0bb3bbfe by Simon Peyton Jones at 2024-01-09T14:06:11+00:00
Move implicationNeeded check to tcSkolemiseGeneral

- - - - -


1 changed file:

- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -369,10 +369,20 @@ tcSkolemiseGeneral
   :: DeepSubsumptionFlag
   -> UserTypeCtxt
   -> TcType
-  -> ([(Name, TcInvisTVBinder)] -> TcType -> IOEnv (Env TcGblEnv TcLclEnv) result)
+  -> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
   -> TcM (HsWrapper, result)
 tcSkolemiseGeneral ds_flag ctxt expected_ty thing_inside
-  = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+  = do { implication_needed <- implicationNeeded ds_flag ctxt expected_ty
+       ; if not implication_needed
+              -- Fast path.  We check every function argument with tcCheckPolyExpr,
+              -- which uses tcTopSkolemise and hence checkConstraints.
+              -- So this fast path is well-exercised
+         then do { res <- thing_inside [] expected_ty
+                 ; return (idHsWrapper, res) }
+         else
+
+    -- So we need an implication constraint
+    do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
          --           in GHC.Tc.Utils.TcType
        ; rec { (wrap, tv_prs, given, rho_ty) <- case ds_flag of
                     Deep    -> deeplySkolemise skol_info expected_ty
@@ -383,7 +393,7 @@ tcSkolemiseGeneral ds_flag ctxt expected_ty thing_inside
        ; (ev_binds, result) <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
                                thing_inside tv_prs rho_ty
 
-       ; return (wrap <.> mkWpLet ev_binds, result) }
+       ; return (wrap <.> mkWpLet ev_binds, result) } }
          -- The ev_binds returned by checkConstraints is very
          -- often empty, in which case mkWpLet is a no-op
 
@@ -407,37 +417,21 @@ tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType
             -> (TcRhoType -> TcM result)
             -> TcM (HsWrapper, result)
 tcSkolemise ds_flag ctxt expected_ty thing_inside
-  | case ds_flag of
-       Shallow -> isRhoTy expected_ty
-       Deep    -> isDeepRhoTy expected_ty
-  = -- Short cut for common case:  no skolemisation to do
-    do { res <- thing_inside expected_ty
-       ; return (idHsWrapper, res) }
-  | otherwise
   = tcSkolemiseGeneral ds_flag ctxt expected_ty $ \_ rho_ty ->
-    thing_inside rho_ty
+    thing_inside rho_ty)
 
 checkConstraints :: SkolemInfoAnon
                  -> [TcTyVar]           -- Skolems
                  -> [EvVar]             -- Given
                  -> TcM result
                  -> TcM (TcEvBinds, result)
-
+-- Always builds an implication
 checkConstraints skol_info skol_tvs given thing_inside
-  = do { implication_needed <- implicationNeeded skol_info skol_tvs given
-
-       ; if implication_needed
-         then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
-                 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
-                 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
-                 ; emitImplications implics
-                 ; return (ev_binds, result) }
-
-         else -- Fast path.  We check every function argument with tcCheckPolyExpr,
-              -- which uses tcTopSkolemise and hence checkConstraints.
-              -- So this fast path is well-exercised
-              do { res <- thing_inside
-                 ; return (emptyTcEvBinds, res) } }
+  = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
+       ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
+       ; emitImplications implics
+       ; return (ev_binds, result) }
 
 checkTvConstraints :: SkolemInfo
                    -> [TcTyVar]          -- Skolem tyvars
@@ -485,18 +479,19 @@ buildTvImplication skol_info skol_tvs tclvl wanted
        ; checkImplicationInvariants implic'
        ; return implic' }
 
-implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
+implicationNeeded :: DeepSubsumptionFlag -> UserTypeCtxt -> TcType -> TcM Bool
 -- See Note [When to build an implication]
-implicationNeeded skol_info skol_tvs given
-  | null skol_tvs
-  , null given
-  , not (alwaysBuildImplication skol_info)
+implicationNeeded ds_flag ctxt expected_ty
+  | case ds_flag of          -- Check for no invisible quantifiers
+       Shallow -> isRhoTy expected_ty
+       Deep    -> isDeepRhoTy expected_ty
+  , not (alwaysBuildImplication ctxt)
   = -- Empty skolems and givens
     do { tc_lvl <- getTcLevel
        ; if not (isTopTcLevel tc_lvl)  -- No implication needed if we are
          then return False             -- already inside an implication
          else
-    do { dflags <- getDynFlags       -- If any deferral can happen,
+    do { dflags <- getDynFlags       -- At top level, if any deferral can happen,
                                      -- we must build an implication
        ; return (gopt Opt_DeferTypeErrors dflags ||
                  gopt Opt_DeferTypedHoles dflags ||
@@ -505,7 +500,7 @@ implicationNeeded skol_info skol_tvs given
   | otherwise     -- Non-empty skolems or givens
   = return True   -- Definitely need an implication
 
-alwaysBuildImplication :: SkolemInfoAnon -> Bool
+alwaysBuildImplication :: UserTypeCtxt -> Bool
 -- See Note [When to build an implication]
 alwaysBuildImplication _ = False
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0bb3bbfee137b2218cab2aa101c77081054df43e

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0bb3bbfee137b2218cab2aa101c77081054df43e
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/20240109/bab1ed3c/attachment-0001.html>