[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