From 59e2c96977fc63f867aad60a2bf4ac9a89456721 Mon Sep 17 00:00:00 2001
From: sheaf <sam.derbyshire@gmail.com>
Date: Wed, 2 Aug 2023 12:05:31 +0200
Subject: [PATCH] Update inert_solved_dicts for ImplicitParams
When adding an implicit parameter dictionary to the inert set, we must
make sure that it replaces any previous implicit parameter dictionaries
that overlap, in order to get the appropriate shadowing behaviour, as in
let ?x = 1 in let ?x = 2 in ?x
We were already doing this for inert_cans, but we weren't doing the same
thing for inert_solved_dicts, which lead to the bug reported in #23761.
The fix is thus to make sure that, when handling an implicit parameter
dictionary in updInertDicts, we update **both** inert_cans and
inert_solved_dicts to ensure a new implicit parameter dictionary
correctly shadows old ones.
Fixes #23761
(cherry picked from commit 41bf2c09f17aa00bf4dd13332c6d07adf21af4f8)
---
compiler/GHC/Tc/Solver/Dict.hs | 49 +++++++++++++------
compiler/GHC/Tc/Solver/InertSet.hs | 9 ++--
compiler/GHC/Tc/Solver/Monad.hs | 10 ++--
.../tests/typecheck/should_run/T23761.hs | 20 ++++++++
.../tests/typecheck/should_run/T23761.stdout | 1 +
.../tests/typecheck/should_run/T23761b.hs | 24 +++++++++
.../tests/typecheck/should_run/T23761b.stdout | 1 +
testsuite/tests/typecheck/should_run/all.T | 2 +
8 files changed, 90 insertions(+), 26 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_run/T23761.hs
create mode 100644 testsuite/tests/typecheck/should_run/T23761.stdout
create mode 100644 testsuite/tests/typecheck/should_run/T23761b.hs
create mode 100644 testsuite/tests/typecheck/should_run/T23761b.stdout
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index 8c85d9e06df..c7298ddf0d1 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -103,9 +103,12 @@ updInertDicts :: DictCt -> TcS ()
updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
= do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls <+> ppr tys)
- -- See Note [Shadowing of implicit parameters]
; if | isGiven ev, Just (str_ty, _) <- isIPPred_maybe cls tys
- -> updInertCans (updDicts (filterDicts (not_ip_for str_ty)))
+ -> -- See (SIP1) and (SIP2) in Note [Shadowing of implicit parameters]
+ -- Update /both/ inert_cans /and/ inert_solved_dicts.
+ updInertSet $ \ inerts@(IS { inert_cans = ics, inert_solved_dicts = solved }) ->
+ inerts { inert_cans = updDicts (filterDicts (not_ip_for str_ty)) ics
+ , inert_solved_dicts = filterDicts (not_ip_for str_ty) solved }
| otherwise
-> return ()
@@ -207,23 +210,35 @@ in two places:
We must /not/ solve this from the Given (?x::Int, C a), because of
the intervening binding for (?x::Int). #14218.
- We deal with this by arranging that when we add [G] (?x::ty) we delete any
- existing [G] (?x::ty) /and/ any [G] D tys, where (D tys) has a superclass
- with (?x::ty). See Note [Local implicit parameters] in GHC.Core.Predicate.
+ We deal with this by arranging that when we add [G] (?x::ty) we delete
+ * from the inert_cans, and
+ * from the inert_solved_dicts
+ any existing [G] (?x::ty) /and/ any [G] D tys, where (D tys) has a superclass
+ with (?x::ty). See Note [Local implicit parameters] in GHC.Core.Predicate.
An important special case is constraint tuples like [G] (% ?x::ty, Eq a %).
But it could happen for `class xx => D xx where ...` and the constraint D
(?x :: int). This corner (constraint-kinded variables instantiated with
implicit parameter constraints) is not well explorered.
- Example in #14218.
+ Example in #14218, and #23761
- The code that accounts for (SIP1) is in updInertDicts, and the call to
+ The code that accounts for (SIP1) is in updInertDicts; in particular the call to
GHC.Core.Predicate.mentionsIP.
-* Wrinkle (SIP2): we delete dictionaries in inert_dicts, but we don't need to
- look in inert_solved_dicts. They are never implicit parameters. See
- Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
+* Wrinkle (SIP2): we must apply this update semantics for `inert_solved_dicts`
+ as well as `inert_cans`.
+ You might think that wouldn't be necessary, because an element of
+ `inert_solved_dicts` is never an implicit parameter (see
+ Note [Solved dictionaries] in GHC.Tc.Solver.InertSet).
+ While that is true, dictionaries in `inert_solved_dicts` may still have
+ implicit parameters as a /superclass/! For example:
+
+ class c => C c where ...
+ f :: C (?x::Int) => blah
+
+ Now (C (?x::Int)) has a superclass (?x::Int). This may look exotic, but it
+ happens particularly for constraint tuples, like `(% ?x::Int, Eq a %)`.
Example 1:
@@ -775,8 +790,8 @@ shortCutSolver dflags ev_w ev_i
loc_w = ctEvLoc ev_w
try_solve_from_instance -- See Note [Shortcut try_solve_from_instance]
- :: (EvBindMap, DictMap CtEvidence) -> CtEvidence
- -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
+ :: (EvBindMap, DictMap DictCt) -> CtEvidence
+ -> MaybeT TcS (EvBindMap, DictMap DictCt)
try_solve_from_instance (ev_binds, solved_dicts) ev
| let pred = ctEvPred ev
, ClassPred cls tys <- classifyPredType pred
@@ -788,7 +803,9 @@ shortCutSolver dflags ev_w ev_i
, cir_what = what }
| safeOverlap what
, all isTyFamFree preds -- Note [Shortcut solving: type families]
- -> do { let solved_dicts' = addSolvedDict cls tys ev solved_dicts
+ -> do { let dict_ct = DictCt { di_ev = ev, di_cls = cls
+ , di_tys = tys, di_pend_sc = doNotExpand }
+ solved_dicts' = addSolvedDict dict_ct solved_dicts
-- solved_dicts': it is important that we add our goal
-- to the cache before we solve! Otherwise we may end
-- up in a loop while solving recursive dictionaries.
@@ -819,12 +836,12 @@ shortCutSolver dflags ev_w ev_i
-- We bail out of the entire computation if we need to emit an EvVar for
-- a subgoal that isn't a ClassPred.
new_wanted_cached :: CtEvidence -> CtLoc
- -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
+ -> DictMap DictCt -> TcPredType -> MaybeT TcS MaybeNew
new_wanted_cached ev_w loc cache pty
| ClassPred cls tys <- classifyPredType pty
= lift $ case findDict cache loc_w cls tys of
- Just ctev -> return $ Cached (ctEvExpr ctev)
- Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty
+ Just dict_ct -> return $ Cached (ctEvExpr (dictCtEvidence dict_ct))
+ Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty
| otherwise = mzero
{- *******************************************************************
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index 28b1e287176..a41525d5e82 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -319,7 +319,7 @@ data InertSet
-- (We have no way of "kicking out" from the cache, so putting
-- wanteds here means we can end up solving a Wanted with itself. Bad)
- , inert_solved_dicts :: DictMap CtEvidence
+ , inert_solved_dicts :: DictMap DictCt
-- All Wanteds, of form (C t1 .. tn)
-- Always a dictionary solved by an instance decl; never an implict parameter
-- See Note [Solved dictionaries]
@@ -1327,10 +1327,9 @@ addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addDict item@(DictCt { di_cls = cls, di_tys = tys }) dm
= insertTcApp dm (classTyCon cls) tys item
-addSolvedDict :: Class -> [Type] -> CtEvidence
- -> DictMap CtEvidence -> DictMap CtEvidence
-addSolvedDict cls tys ev dm
- = insertTcApp dm (classTyCon cls) tys ev
+addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt
+addSolvedDict item@(DictCt { di_cls = cls, di_tys = tys }) dm
+ = insertTcApp dm (classTyCon cls) tys item
filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
filterDicts f m = filterTcAppMap f m
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index da38736dbfc..77ac9b9dd37 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -479,19 +479,19 @@ getSafeOverlapFailures
updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
-- Conditionally add a new item in the solved set of the monad
-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
-updSolvedDicts what dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
+updSolvedDicts what dict_ct@(DictCt { di_ev = ev })
| isWanted ev
, instanceReturnsDictCon what
= do { traceTcS "updSolvedDicts:" $ ppr dict_ct
; updInertSet $ \ ics ->
- ics { inert_solved_dicts = addSolvedDict cls tys ev (inert_solved_dicts ics) } }
+ ics { inert_solved_dicts = addSolvedDict dict_ct (inert_solved_dicts ics) } }
| otherwise
= return ()
-getSolvedDicts :: TcS (DictMap CtEvidence)
+getSolvedDicts :: TcS (DictMap DictCt)
getSolvedDicts = do { ics <- getInertSet; return (inert_solved_dicts ics) }
-setSolvedDicts :: DictMap CtEvidence -> TcS ()
+setSolvedDicts :: DictMap DictCt -> TcS ()
setSolvedDicts solved_dicts
= updInertSet $ \ ics ->
ics { inert_solved_dicts = solved_dicts }
@@ -757,7 +757,7 @@ lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
- = findDict solved loc cls tys
+ = fmap dictCtEvidence (findDict solved loc cls tys)
---------------------------
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
diff --git a/testsuite/tests/typecheck/should_run/T23761.hs b/testsuite/tests/typecheck/should_run/T23761.hs
new file mode 100644
index 00000000000..4658b408232
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T23761.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ImplicitParams #-}
+
+module Main where
+
+import Data.Kind ( Constraint )
+
+type IPInt =
+ ( (?ipInt :: Int)
+ , ( () :: Constraint) -- Comment this out and main prints 7 instead of 3 on GHC 9.8
+ )
+
+hasIPInt :: IPInt => Int
+hasIPInt = ?ipInt
+
+let_ipInt_7_in :: IPInt => (IPInt => r) -> r
+let_ipInt_7_in x = let ?ipInt = 7 in x
+
+main :: IO ()
+main = print (let ?ipInt = 3 in let_ipInt_7_in hasIPInt)
+ -- the 7 in 'let_ipInt_eq_7_in' should shadow the outer 3
diff --git a/testsuite/tests/typecheck/should_run/T23761.stdout b/testsuite/tests/typecheck/should_run/T23761.stdout
new file mode 100644
index 00000000000..7f8f011eb73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T23761.stdout
@@ -0,0 +1 @@
+7
diff --git a/testsuite/tests/typecheck/should_run/T23761b.hs b/testsuite/tests/typecheck/should_run/T23761b.hs
new file mode 100644
index 00000000000..74093a28926
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T23761b.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Main where
+
+class c => IdCt c
+instance c => IdCt c
+
+type IPInt = IdCt (?ipInt :: Int)
+
+hasIPInt :: IPInt => Int
+hasIPInt = ?ipInt
+
+let_ipInt_eq_7_in :: IPInt => (IPInt => r) -> r
+let_ipInt_eq_7_in x = let ?ipInt = 7 in x
+
+test :: Int
+test = let ?ipInt = 3 in let_ipInt_eq_7_in hasIPInt
+
+main :: IO ()
+main = print test
+ -- the 7 in 'let_ipInt_eq_7_in' should shadow the outer 3
diff --git a/testsuite/tests/typecheck/should_run/T23761b.stdout b/testsuite/tests/typecheck/should_run/T23761b.stdout
new file mode 100644
index 00000000000..7f8f011eb73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T23761b.stdout
@@ -0,0 +1 @@
+7
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index b3272d19953..f09be8203c2 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -169,3 +169,5 @@ test('T20768', normal, compile_and_run, [''])
test('T22510', normal, compile_and_run, [''])
test('T21973a', [exit_code(1)], compile_and_run, [''])
test('T21973b', normal, compile_and_run, [''])
+test('T23761', normal, compile_and_run, [''])
+test('T23761b', normal, compile_and_run, [''])
--
GitLab