[Git][ghc/ghc][wip/sand-witch/lazy-skol] Tidying up

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Sun Jan 7 00:09:31 UTC 2024



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


Commits:
7b785ac8 by Simon Peyton Jones at 2024-01-07T00:09:00+00:00
Tidying up

- - - - -


7 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-boot
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/typecheck/should_fail/tcfail175.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -638,7 +638,7 @@ tcPolyCheck prag_fn
        ; (wrap_gen, (wrap_res, matches'))
              <- tcSkolemiseCompleteSig sig $ \invis_pat_tys rho_ty ->
                 setSrcSpanA bind_loc  $
-                tcFunBindMatches ctxt mono_name mult matches invis_pat_tys rho_ty
+                tcFunBindMatches ctxt mono_name mult matches invis_pat_tys (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,
-         tcPolyLExpr, tcPolyLExprNC, tcPolyExpr, tcExpr,
+         tcPolyLExpr, tcPolyExpr, tcExpr, tcPolyLExprSig,
          tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
          tcCheckId,
          ) where
@@ -100,7 +100,6 @@ import qualified Data.List.NonEmpty as NE
 ************************************************************************
 -}
 
-
 tcCheckPolyExpr, tcCheckPolyExprNC
   :: LHsExpr GhcRn         -- Expression to type check
   -> TcSigmaType           -- Expected type (could be a polytype)
@@ -129,6 +128,104 @@ tcPolyLExprNC (L loc expr) res_ty
     do { expr' <- tcPolyExpr expr res_ty
        ; return (L loc expr') }
 
+
+tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
+tcPolyExpr e (Infer inf) = tcExpr e (Infer inf)
+tcPolyExpr e (Check ty)  = tcPolyExprCheck e (Left ty)
+
+tcPolyLExprSig :: LHsExpr GhcRn -> TcCompleteSig -> TcM (LHsExpr GhcTc)
+tcPolyLExprSig (L loc expr) sig
+  = setSrcSpanA loc $ addExprCtxt expr $
+    do { expr' <- tcPolyExprCheck expr (Right sig)
+       ; return (L loc expr') }
+
+-----------------
+tcPolyExprCheck :: HsExpr GhcRn
+                -> Either TcSigmaType TcCompleteSig
+                -> TcM (HsExpr GhcTc)
+-- tcPolyExpCheck deals with the special case for HsLam, in case the pushed-down
+-- type is a forall-type.  E.g.    (\@a -> blah) :: forall b. b -> Int
+--
+-- 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.
+
+tcPolyExprCheck expr res_ty
+  = outer_skolemise res_ty $ \pat_tys rho_ty ->
+    let
+      -- tc_body is a little loop that looks past parentheses
+      tc_body (HsPar x (L loc e))
+        = setSrcSpanA loc $
+          do { e' <- tc_body e
+             ; return (HsPar x (L loc e')) }
+
+      -- The special case for lambda: go to tcLambdaPatches, 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,
+               --     if DeepSubsumption is on;  hence no need to do that here
+             ; return (mkHsWrap wrap $ HsLam x lam_variant matches') }
+
+      -- The general case: just do deep skolemisation if necessary,
+      -- before handing off to tcExpr
+      tc_body e
+        = do { ds_flag <- getDeepSubsumptionFlag
+             ; inner_skolemise ds_flag rho_ty $ \rho_ty' ->
+               tcExpr e (mkCheckExpType rho_ty') }
+    in tc_body expr
+  where
+    -- outer_skolemise is used always
+    -- It only does shallow skolemisation
+    outer_skolemise :: Either TcSigmaType TcCompleteSig
+                    -> ([ExpPatType] -> TcRhoType -> TcM (HsExpr GhcTc))
+                    -> TcM (HsExpr GhcTc)
+    outer_skolemise (Left ty) thing_inside
+      = do { (wrap, expr') <- tcSkolemise Shallow GenSigCtxt ty $ \rho_ty ->
+                              thing_inside [] rho_ty
+           ; return (mkHsWrap wrap expr') }
+    outer_skolemise (Right sig) thing_inside
+      = do { (wrap, expr') <- tcSkolemiseCompleteSig sig thing_inside
+           ; return (mkHsWrap wrap expr') }
+
+    -- inner_skolemise is used when we do not have a lambda
+    -- With deep skolemisation we must remember to deeply skolemise
+    -- after the (always-shallow) tcSkolemiseCompleteSig
+    inner_skolemise :: DeepSubsumptionFlag -> TcRhoType
+                    -> (TcRhoType -> TcM (HsExpr GhcTc)) -> TcM (HsExpr GhcTc)
+    inner_skolemise Shallow rho_ty thing_inside
+      = -- We have already done shallow skolemisation, so nothing further to do
+        thing_inside rho_ty
+    inner_skolemise Deep rho_ty thing_inside
+      = -- Try deep skolemisation
+        do { (wrap, expr') <- tcSkolemise Deep ctxt rho_ty thing_inside
+           ; return (mkHsWrap wrap expr') }
+
+    ctxt = case res_ty of
+             Left {}   -> GenSigCtxt
+             Right sig -> sig_ctxt sig
+
+
+{- *********************************************************************
+*                                                                      *
+        tcExpr: the main expression typechecker
+*                                                                      *
+********************************************************************* -}
+
+tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
+-- Infer a *rho*-type. The return type is always instantiated.
+tcInferRho (L loc expr)
+  = setSrcSpanA loc   $  -- Set location /first/; see GHC.Tc.Utils.Monad
+    addExprCtxt expr $  -- Note [Error contexts in generated code]
+    do { (expr', rho) <- tcInfer (tcExpr expr)
+       ; return (L loc expr', rho) }
+
+tcInferRhoNC (L loc expr)
+  = setSrcSpanA loc $
+    do { (expr', rho) <- tcInfer (tcExpr expr)
+       ; return (L loc expr', rho) }
+
 ---------------
 tcCheckMonoExpr, tcCheckMonoExprNC
     :: LHsExpr GhcRn     -- Expression to type check
@@ -138,6 +235,7 @@ tcCheckMonoExpr, tcCheckMonoExprNC
 tcCheckMonoExpr   expr res_ty = tcMonoExpr   expr (mkCheckExpType res_ty)
 tcCheckMonoExprNC expr res_ty = tcMonoExprNC expr (mkCheckExpType res_ty)
 
+---------------
 tcMonoExpr, tcMonoExprNC
     :: LHsExpr GhcRn     -- Expression to type check
     -> ExpRhoType        -- Expected type
@@ -156,51 +254,6 @@ tcMonoExprNC (L loc expr) res_ty
         ; return (L loc expr') }
 
 ---------------
-tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
--- Infer a *rho*-type. The return type is always instantiated.
-tcInferRho (L loc expr)
-  = setSrcSpanA loc   $  -- Set location /first/; see GHC.Tc.Utils.Monad
-    addExprCtxt expr $  -- Note [Error contexts in generated code]
-    do { (expr', rho) <- tcInfer (tcExpr expr)
-       ; return (L loc expr', rho) }
-
-tcInferRhoNC (L loc expr)
-  = setSrcSpanA loc $
-    do { (expr', rho) <- tcInfer (tcExpr expr)
-       ; return (L loc expr', rho) }
-
-
-{- *********************************************************************
-*                                                                      *
-        tcExpr: the main expression typechecker
-*                                                                      *
-********************************************************************* -}
-
-tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
-
--- We begin with a special case for HsLam, in case the pushed-down type
--- is a forall-type.  E.g.    (\@a -> blah) :: forall b. b -> Int
-tcPolyExpr e@(HsLam x lam_variant matches) res_ty
-  = do { (wrap, matches') <- tcLambdaMatches e lam_variant matches [] res_ty
-       ; return (mkHsWrap wrap $ HsLam x lam_variant matches') }
-
--- This HsPar case means that the lambda can be wrapped in parens
-tcPolyExpr (HsPar x expr) res_ty
-  = do { expr' <- tcPolyLExprNC expr res_ty
-       ; return (HsPar x expr') }
-
--- Otherwise we skolemise the expected type, perhaps deeply
--- if DeepSkolemisation is on, and then do tcExpr
-tcPolyExpr expr exp_ty@(Infer {})
-  = do { traceTc "tcPolyExpr:infer" (ppr exp_ty)
-       ; tcExpr expr exp_ty }
-tcPolyExpr expr (Check ty)
-  = do { traceTc "tcPolyExpr:check" (ppr ty)
-       ; ds_flag <- getDeepSubsumptionFlag
-       ; (wrap,expr') <- tcSkolemise ds_flag GenSigCtxt ty $ \rho_ty ->
-                         tcExpr expr (mkCheckExpType rho_ty)
-       ; return $ mkHsWrap wrap expr' }
-
 tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
 
 -- Use tcApp to typecheck applications, which are treated specially


=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -5,6 +5,7 @@ import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR
                            , SyntaxOpType
                            , ExpType, ExpRhoType, ExpSigmaType )
 import GHC.Tc.Types        ( TcM )
+import GHC.Tc.Types.BasicTypes( TcCompleteSig )
 import GHC.Tc.Types.Origin ( CtOrigin )
 import GHC.Core.Type ( Mult )
 import GHC.Hs.Extension ( GhcRn, GhcTc )
@@ -23,7 +24,8 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
        -> TcRhoType
        -> TcM (LHsExpr GhcTc)
 
-tcPolyLExpr, tcPolyLExprNC :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
+tcPolyLExpr    :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
+tcPolyLExprSig :: LHsExpr GhcRn -> TcCompleteSig -> TcM (LHsExpr GhcTc)
 
 tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
 tcExpr     :: HsExpr GhcRn -> ExpRhoType   -> TcM (HsExpr GhcTc)


=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -29,8 +29,7 @@ module GHC.Tc.Gen.Head
 
        , addHeadCtxt, addExprCtxt, addFunResCtxt ) where
 
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckPolyExprNC, tcPolyLExprNC )
-import {-# SOURCE #-} GHC.Tc.Gen.Match( tcLambdaMatches )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckPolyExprNC, tcPolyLExprSig )
 
 import GHC.Prelude
 import GHC.Hs
@@ -980,26 +979,10 @@ tcExprWithSig expr hs_ty
     loc = getLocA (dropWildCards hs_ty)
 
 tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcSigmaType)
-tcExprSig _ (TcPatSynSig sig) = pprPanic "tcExprSig" (ppr sig)
-
+tcExprSig _ (TcPatSynSig sig)      = pprPanic "tcExprSig" (ppr sig)
 tcExprSig expr (TcCompleteSig sig)
-  = do { (wrap, expr') <- tcSkolemiseCompleteSig sig $ \invis_pat_tys rho_ty ->
-                          tc_body invis_pat_tys rho_ty
-       ; return (mkLHsWrap wrap expr', idType (sig_bndr sig)) }
-  where
-    tc_body :: [ExpPatType] -> ExpRhoType -> TcM (LHsExpr GhcTc)
-    tc_body pat_tys rho_ty = go expr
-      where
-        -- Look for (\@a -> blah), in case we have
-        --   (\@a -> blah) :: forall b. woo
-        go (L loc e@(HsLam x lam_variant matches))
-          = setSrcSpanA loc $
-            do { (wrap, matches') <- tcLambdaMatches e lam_variant matches pat_tys rho_ty
-               ; return (L loc $ mkHsWrap wrap $ HsLam x lam_variant matches') }
-        go (L _ (HsPar _ expr)) = go expr
-        go expr  -- Even though we have skolemised, call tcCheckPolyExpr so that
-                 -- if we need to /deeply/ skolemise, we will do so (in tcPolyExpr).
-          = tcPolyLExprNC expr rho_ty
+   = do { expr' <- tcPolyLExprSig expr sig
+        ; return (expr', idType (sig_bndr sig)) }
 
 tcExprSig expr sig@(TcPartialSig (PSig { psig_name = name, psig_loc = loc }))
   = setSrcSpan loc $   -- Sets the location for the implication constraint


=====================================
compiler/GHC/Tc/Gen/Match.hs-boot
=====================================
@@ -1,5 +1,5 @@
 module GHC.Tc.Gen.Match where
-import GHC.Hs           ( GRHSs, MatchGroup, LHsExpr, HsExpr, HsLamVariant, Mult )
+import GHC.Hs           ( GRHSs, MatchGroup, LHsExpr, Mult )
 import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType, ExpPatType )
 import GHC.Tc.Types     ( TcM )
 import GHC.Tc.Types.Origin  ( UserTypeCtxt )
@@ -18,9 +18,3 @@ tcFunBindMatches :: UserTypeCtxt -> Name
                  -> [ExpPatType]
                  -> ExpSigmaType
                  -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
-
-tcLambdaMatches :: HsExpr GhcRn -> HsLamVariant
-                -> MatchGroup GhcRn (LHsExpr GhcRn)
-                -> [ExpPatType]
-                -> ExpSigmaType
-                -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -384,6 +384,9 @@ matchExpectedFunTys :: forall a.
 -- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
 --   where [t1, ..., tn], ty_r are passed to the thing_inside
 --
+-- Unconditionally concludes by skolemising any trailing invisible
+-- binders and, if DeepSubsumption is on, it does so deeply.
+--
 -- Postcondition:
 --   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{}
@@ -1525,7 +1528,7 @@ tcSkolemiseGeneral ds_flag ctxt expected_ty thing_inside
          -- often empty, in which case mkWpLet is a no-op
 
 tcSkolemiseCompleteSig :: TcCompleteSig
-                       -> ([ExpPatType] -> ExpRhoType -> TcM result)
+                       -> ([ExpPatType] -> TcRhoType -> TcM result)
                        -> TcM (HsWrapper, result)
 -- ^ The wrapper has type: spec_ty ~> expected_ty
 -- See Note [Skolemisation] for the differences between
@@ -1536,11 +1539,10 @@ tcSkolemiseCompleteSig (CSig { sig_bndr = poly_id, sig_ctxt = ctxt, sig_loc = lo
   = setSrcSpan loc $   -- Sets the location for the implication constraint
     do { tcSkolemiseGeneral Shallow ctxt (idType poly_id) $ \tv_prs rho_ty ->
          tcExtendNameTyVarEnv (map (fmap binderVar) tv_prs) $
-         thing_inside (map (mkInvisExpPatType . snd) tv_prs)
-                      (mkCheckExpType rho_ty) }
+         thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty }
 
 tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType
-            -> (TcType -> TcM result)
+            -> (TcRhoType -> TcM result)
             -> TcM (HsWrapper, result)
 tcSkolemise ds_flag ctxt expected_ty thing_inside
   | isRhoTy expected_ty  -- Short cut for common case


=====================================
testsuite/tests/typecheck/should_fail/tcfail175.hs
=====================================
@@ -1,7 +1,7 @@
 
 -- Crashed GHC 6.6!
 -- #1153
- 
+
 module ShouldFail where
 
 eval :: Int -> String -> String ->  String



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7b785ac8bd821337b2100d130d28f639a63238e6

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7b785ac8bd821337b2100d130d28f639a63238e6
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/20240106/c9b65f95/attachment-0001.html>


More information about the ghc-commits mailing list