[Git][ghc/ghc][master] 2 commits: Add test for #25185
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Nov 20 23:10:51 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
791a47b2 by Arnaud Spiwack at 2024-11-20T14:00:05+00:00
Add test for #25185
- - - - -
374e18e5 by Arnaud Spiwack at 2024-11-20T14:09:30+00:00
Quick look: emit the multiplicity of app heads in tcValArgs
Otherwise it's not scaled properly by the context, allowing unsound
expressions.
Fixes #25185.
- - - - -
7 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Utils/Monad.hs
- testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr
- + testsuite/tests/linear/should_fail/T25185.hs
- + testsuite/tests/linear/should_fail/T25185.stderr
- testsuite/tests/linear/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -569,6 +569,7 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted
, eaql_arg_ty = sc_arg_ty
, eaql_larg = larg@(L arg_loc rn_expr)
, eaql_tc_fun = tc_head
+ , eaql_fun_ue = head_ue
, eaql_args = inst_args
, eaql_encl = arg_influences_enclosing_call
, eaql_res_rho = app_res_rho })
@@ -578,7 +579,8 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted
; traceTc "tcEValArgQL {" (vcat [ text "app_res_rho:" <+> ppr app_res_rho
, text "exp_arg_ty:" <+> ppr exp_arg_ty
- , text "args:" <+> ppr inst_args ])
+ , text "args:" <+> ppr inst_args
+ , text "mult:" <+> ppr mult])
; ds_flag <- getDeepSubsumptionFlag
; (wrap, arg')
@@ -587,6 +589,9 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted
do { -- Emit saved-up constraints, /under/ the tcSkolemise
-- See (QLA4) in Note [Quick Look at value arguments]
emitConstraints wanted
+ -- Emit saved-up usages /under/ the tcScalingUsage.
+ -- See (QLA5) in Note [Quick Look at value arguments]
+ ; tcEmitBindingUsage head_ue
-- Unify with context if we have not already done so
-- See (QLA4) in Note [Quick Look at value arguments]
@@ -1630,6 +1635,41 @@ This turned out to be more subtle than I expected. Wrinkles:
(kappa = [forall a. a->a]). Now we resume typechecking argument [], and
we must take advantage of what we have now discovered about `kappa`,
to typecheck [] :: [forall a. a->a]
+
+(QLA5) In the quicklook pass, we don't scale multiplicities. Since arguments
+ aren't typechecked yet, we don't know their free variable usages
+ anyway. But, in a nested call, the head of an application chain is fully
+ typechecked.
+
+ In order for the multiplicities in the head to be properly scaled, we store
+ the head's usage environment in the eaql_fun_ue field. Then, when we do the
+ full-typechecking pass, we can emit the head's usage environment where we
+ would have typechecked the head in a naive algorithm.
+
+(QLA6) `quickLookArg` is supposed to capture the result of partially typechecking
+ the argument, so it can be resumed later. "Capturing" should include all
+ generated type-class/equality constraints and Linear-Haskell usage info. There
+ are two calls in `quickLookArg1` that might generate such constraints:
+
+ - `tcInferAppHead_maybe`. This can generat Linear-Haskell usage info, via
+ the call to `tcEmitBindingUsage` in `check_local_id`, which is called
+ indirectly by `tcInferAppHead_maybe`.
+
+ In contrast, `tcInferAppHead_maybe` does not generate any type-class or
+ equality constraints, because it doesn't instantiate any functions. [But
+ see #25493 and #25494 for why this isn't quite true today.]
+
+ - `tcInstFun` generates lots of type-class and equality constraints, as it
+ instantiates the function. But it generates no usage info, because that
+ comes only from the call to `check_local_id`, whose usage info is captured
+ in the call to `tcInferAppHead_maybe` in `quickLookArg1`.
+
+ Conclusion: in quickLookArg1:
+ - capture usage information (but not constraints)
+ for the call to `tcInferAppHead_maybe`
+ - capture constraints (but not usage information)
+ for the call to `tcInstFun`
+
-}
quickLookArg :: QLFlag -> AppCtxt
@@ -1697,7 +1737,12 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
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
+ ; (fun_ue, mb_fun_ty) <- tcCollectingUsage $ tcInferAppHead_maybe rn_fun
+ -- tcCollectingUsage: the use of an Id at the head generates usage-info
+ -- See the call to `tcEmitBindingUsage` in `check_local_id`. So we must
+ -- capture and save it in the `EValArgQL`. See (QLA6) in
+ -- Note [Quick Look at value arguments]
+
; traceTc "quickLookArg {" $
vcat [ text "arg:" <+> ppr arg
, text "orig_arg_rho:" <+> ppr orig_arg_rho
@@ -1714,6 +1759,9 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
; ((inst_args, app_res_rho), wanted)
<- captureConstraints $
tcInstFun do_ql True tc_head fun_sigma rn_args
+ -- We must capture type-class and equality constraints here, but
+ -- not equality constraints. See (QLA6) in Note [Quick Look at
+ -- value arguments]
; traceTc "quickLookArg 2" $
vcat [ text "arg:" <+> ppr arg
@@ -1746,6 +1794,7 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
, eaql_arg_ty = sc_arg_ty
, eaql_larg = larg
, eaql_tc_fun = tc_head
+ , eaql_fun_ue = fun_ue
, eaql_args = inst_args
, eaql_wanted = wanted
, eaql_encl = arg_influences_enclosing_call
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -57,7 +57,7 @@ import GHC.Tc.Zonk.TcType
import GHC.Core.FamInstEnv ( FamInstEnvs )
-import GHC.Core.UsageEnv ( singleUsageUE )
+import GHC.Core.UsageEnv ( singleUsageUE, UsageEnv )
import GHC.Core.PatSyn( PatSyn, patSynName )
import GHC.Core.ConLike( ConLike(..) )
import GHC.Core.DataCon
@@ -178,6 +178,7 @@ data HsExprArg (p :: TcPass) where -- See Note [HsExprArg]
, eaql_larg :: LHsExpr GhcRn -- Original application, for
-- location and error msgs
, eaql_tc_fun :: (HsExpr GhcTc, AppCtxt) -- Typechecked head
+ , eaql_fun_ue :: UsageEnv -- Usage environment of the typechecked head (QLA5)
, eaql_args :: [HsExprArg 'TcpInst] -- Args: instantiated, not typechecked
, eaql_wanted :: WantedConstraints
, eaql_encl :: Bool -- True <=> we have already qlUnified
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -1412,7 +1412,7 @@ tcCollectingUsage thing_inside
tcScalingUsage :: Mult -> TcM a -> TcM a
tcScalingUsage mult thing_inside
= do { (usage, result) <- tcCollectingUsage thing_inside
- ; traceTc "tcScalingUsage" (ppr mult)
+ ; traceTc "tcScalingUsage" $ vcat [ppr mult, ppr usage]
; tcEmitBindingUsage $ scaleUE mult usage
; return result }
=====================================
testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr
=====================================
@@ -1,3 +1,7 @@
+LinearConfusedDollar.hs:12:3: error: [GHC-18872]
+ • Couldn't match type ‘Many’ with ‘One’
+ arising from multiplicity of ‘x’
+ • In an equation for ‘g’: g x = f $ x
LinearConfusedDollar.hs:12:7: error: [GHC-83865]
• Couldn't match type ‘One’ with ‘Many’
@@ -6,3 +10,4 @@ LinearConfusedDollar.hs:12:7: error: [GHC-83865]
• In the first argument of ‘($)’, namely ‘f’
In the expression: f $ x
In an equation for ‘g’: g x = f $ x
+
=====================================
testsuite/tests/linear/should_fail/T25185.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module T25185 where
+
+f :: Int -> Int
+f x = x
+
+g :: Int %1 -> Int
+g y = f y
=====================================
testsuite/tests/linear/should_fail/T25185.stderr
=====================================
@@ -0,0 +1,5 @@
+T25185.hs:10:3: error: [GHC-18872]
+ • Couldn't match type ‘Many’ with ‘One’
+ arising from multiplicity of ‘y’
+ • In an equation for ‘g’: g y = f y
+
=====================================
testsuite/tests/linear/should_fail/all.T
=====================================
@@ -53,3 +53,4 @@ test('LinearLet9', normal, compile_fail, [''])
test('LinearLet10', normal, compile_fail, [''])
test('T25081', normal, compile_fail, [''])
test('T24961', normal, compile_fail, [''])
+test('T25185', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/11bad98d67ae5557eae1dd965f0457b78b496ecc...374e18e5e79125375a49432da939abbb36268c8a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/11bad98d67ae5557eae1dd965f0457b78b496ecc...374e18e5e79125375a49432da939abbb36268c8a
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/20241120/609178b8/attachment-0001.html>
More information about the ghc-commits
mailing list