[Git][ghc/ghc][wip/T24676] First attempt at #24676
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Apr 18 23:17:53 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
297971de by Simon Peyton Jones at 2024-04-19T00:17:26+01:00
First attempt at #24676
- - - - -
2 changed files:
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Tc/Gen/App.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -29,6 +29,7 @@ module GHC.Core.TyCo.FVs
-- Any and No Free vars
anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
+ anyFreeVarsOfTypeM,
-- * Free type constructors
tyConsOfType, tyConsOfTypes,
@@ -58,7 +59,7 @@ import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )
import GHC.Builtin.Types.Prim( funTyFlagTyCon )
-import Data.Monoid as DM ( Endo(..), Any(..) )
+import Data.Monoid as DM ( Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom( coAxiomTyCon )
@@ -74,6 +75,8 @@ import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Pair
+import Data.Semigroup
+
{-
%************************************************************************
%* *
@@ -974,6 +977,36 @@ noFreeVarsOfCo co = not $ DM.getAny (f co)
where (_, _, f, _) = foldTyCo (afvFolder (const True)) emptyVarSet
+{- *********************************************************************
+* *
+ Folding over free vars
+* *
+********************************************************************* -}
+
+newtype AnyM m = AM { unAnyM :: m Bool }
+
+instance Monad m => Semigroup (AnyM m) where
+ AM ml <> AM mr = AM (do { l <- ml; if l then return True else mr })
+
+instance Monad m => Monoid (AnyM m) where
+ mempty = AM (return False)
+
+{-# INLINE afvFolderM #-} -- so that specialization to (const True) works
+afvFolderM :: Monad m => (TyCoVar -> m Bool) -> TyCoFolder TyCoVarSet (AnyM m)
+afvFolderM check_fv = TyCoFolder { tcf_view = noView
+ , tcf_tyvar = do_tv, tcf_covar = mempty
+ , tcf_hole = mempty, tcf_tycobinder = do_bndr }
+ where
+ do_bndr is tcv _ = extendVarSet is tcv
+ do_tv is tv | tv `elemVarSet` is = AM (return False)
+ | otherwise = AM (check_fv tv)
+
+anyFreeVarsOfTypeM :: Monad m => (TyCoVar -> m Bool) -> Type -> m Bool
+-- Returns True if check_fv returns True of any free var of the type
+anyFreeVarsOfTypeM check_fv ty = unAnyM (f ty)
+ where (f, _, _, _) = foldTyCo (afvFolderM check_fv) emptyVarSet
+
+
{- *********************************************************************
* *
scopedSort
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -1472,7 +1472,7 @@ quickLookArg delta larg (Scaled _ arg_ty)
where
guarded = isGuardedTy arg_ty
-- NB: guardedness is computed based on the original,
- -- unzonked arg_ty (before calling `go`, so that we deliberately do
+ -- unzonked arg_ty (before calling `go`), so that we deliberately do
-- not exploit guardedness that emerges a result of QL on earlier args
go arg_ty | not (isRhoTy arg_ty)
@@ -1499,11 +1499,15 @@ isGuardedTy ty
quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaTypeFRR
-> TcM (Delta, EValArg 'TcpInst)
+-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
quickLookArg1 guarded delta larg@(L _ arg) arg_ty
= do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
+
+ -- Step 1: get the type of the head of the argument
; mb_fun_ty <- tcInferAppHead_maybe rn_fun
; traceTc "quickLookArg 1" $
vcat [ text "arg:" <+> ppr arg
+ , text "arg_ty:" <+> ppr arg_ty
, text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
, text "args:" <+> ppr rn_args ]
@@ -1511,8 +1515,10 @@ quickLookArg1 guarded delta larg@(L _ arg) arg_ty
Nothing -> skipQuickLook delta larg ; -- fun is too complicated
Just (tc_fun, fun_sigma) ->
+ -- Step 2: use |-inst to instantiate the head applied to the arguments
do { do_ql <- wantQuickLook rn_fun
; (delta_app, inst_args, app_res_rho) <- tcInstFun do_ql True (tc_fun, fun_ctxt) fun_sigma rn_args
+
; traceTc "quickLookArg 2" $
vcat [ text "arg:" <+> ppr arg
, text "delta:" <+> ppr delta
@@ -1520,36 +1526,44 @@ quickLookArg1 guarded delta larg@(L _ arg) arg_ty
, text "arg_ty:" <+> ppr arg_ty
, text "app_res_rho:" <+> ppr app_res_rho ]
- -- Now check whether arg_ty is guar
- ; let do_one :: TcTyVar -> TcM Bool -> TcM Bool
- do_one tv do_rest = do { unfilled <- isUnfilledMetaTyVar tv
- ; if unfilled then return False
- else do_rest }
- check_no_free_kappas :: Delta -> TcM Bool
- check_no_free_kappas delta
- = nonDetStrictFoldVarSet do_one (return True) delta
-
- ; can_do_ql <- if guarded
+ -- Step 3: check the two other premises of APP-lightning-bolt (Fig 5 in the paper)
+ -- Namely: (A) is rho guarded, and (B) fiv(rho_r) = emptyset
+ ; can_do_ql <- if guarded -- (A)
then return True
- else check_no_free_kappas delta_app
+ else not <$> anyFreeKappa delta_app app_res_rho -- (B)
+ -- For (B) see Note [The fiv test in quickLookArg]
- ; if not can_do_ql then skipQuickLook delta larg
- else
+ -- Step 4: do quick-look unification if either (A) or (B) hold
+ -- NB: arg_ty may not be zonked, but that's ok
+ ; let delta' = delta `unionVarSet` delta_app
+ ; when can_do_ql $
+ qlUnify delta' arg_ty app_res_rho
- do { traceTc "quickLookArg 3" $
+ ; traceTc "quickLookArg 3" $
vcat [ text "tc_fun:" <+> ppr tc_fun
, text "fun_sigma:" <+> ppr fun_sigma ]
- -- Do quick-look unification
- -- NB: arg_ty may not be zonked, but that's ok
- ; let delta' = delta `unionVarSet` delta_app
- ; qlUnify delta' arg_ty app_res_rho
-
- ; let ql_arg = ValArgQL { va_expr = larg
- , va_fun = (tc_fun, fun_ctxt)
- , va_args = inst_args
- , va_ty = app_res_rho }
- ; return (delta', ql_arg) } } } }
+ ; let ql_arg = ValArgQL { va_expr = larg
+ , va_fun = (tc_fun, fun_ctxt)
+ , va_args = inst_args
+ , va_ty = app_res_rho }
+ ; return (delta', ql_arg) } } }
+
+anyFreeKappa :: Delta -> TcType -> TcM Bool
+-- True if there is a free instantiation variable (member of Delta)
+-- in the argument type, after zonking
+-- See Note [The fiv test in quickLookArg]
+anyFreeKappa delta ty
+ = anyFreeVarsOfTypeM is_free_kappa ty
+ where
+ is_free_kappa :: TcTyVar -> TcM Bool
+ is_free_kappa tv | tv `elemVarSet` delta
+ = do { info <- readMetaTyVar tv
+ ; case info of
+ Indirect ty -> anyFreeKappa delta ty
+ Flexi -> return True }
+ | otherwise
+ = return False
skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook delta larg = return (delta, ValArg larg)
@@ -1578,6 +1592,20 @@ quickLookResultType _ app_res_rho (Infer {})
-- generator. The safe thing to do is to zonk any instantiation
-- variables away. See Note [Instantiation variables are short lived]
+{- Note [The fiv test in quickLookArg]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In rule APP-lightning-bolt in Fig 5 of the paper, we have to test rho_r
+for having no free instantiation variables. We do this in Step 3 of quickLookArg1,
+using anyFreeKappa. Example:
+ Suppose ids :: [forall a. a->a]
+ and consider Just (ids++ids)
+We will instantiate Just with kappa, say, and then call
+ quickLookArg1 False {kappa} (ids ++ ids) kappa
+The call to tcInstFun will return with app_res_rho = [forall a. a->a]
+which has no free instantiation variables, so we can QL-unify
+ kappa ~ [Forall a. a->a]
+-}
+
---------------------
qlUnify :: Delta -> TcType -> TcType -> TcM ()
-- Unify ty1 with ty2, unifying only variables in delta
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/297971defa05c370e528ad452f2f8d2a21ccf78d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/297971defa05c370e528ad452f2f8d2a21ccf78d
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/20240418/4af0cca5/attachment-0001.html>
More information about the ghc-commits
mailing list