[Git][ghc/ghc][master] Update inert_solved_dicts for ImplicitParams

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Fri Aug 4 21:24:34 UTC 2023



Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
41bf2c09 by sheaf at 2023-08-04T17:23:42-04:00
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

- - - - -


8 changed files:

- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- + testsuite/tests/typecheck/should_run/T23761.hs
- + testsuite/tests/typecheck/should_run/T23761.stdout
- + testsuite/tests/typecheck/should_run/T23761b.hs
- + testsuite/tests/typecheck/should_run/T23761b.stdout
- testsuite/tests/typecheck/should_run/all.T


Changes:

=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -106,9 +106,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 ()
 
@@ -210,23 +213,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:
 
@@ -778,8 +793,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
@@ -793,7 +808,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.
@@ -824,12 +841,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
 
 {- *******************************************************************


=====================================
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


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -478,19 +478,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 }
@@ -756,7 +756,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)


=====================================
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


=====================================
testsuite/tests/typecheck/should_run/T23761.stdout
=====================================
@@ -0,0 +1 @@
+7


=====================================
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


=====================================
testsuite/tests/typecheck/should_run/T23761b.stdout
=====================================
@@ -0,0 +1 @@
+7


=====================================
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, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/41bf2c09f17aa00bf4dd13332c6d07adf21af4f8

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/41bf2c09f17aa00bf4dd13332c6d07adf21af4f8
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/20230804/04048d25/attachment-0001.html>


More information about the ghc-commits mailing list