Wibbleswip/T23070-dicts

12 files changed, 110 insertions, 108 deletions

diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index 86acfbee23..1946d4cee9 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -25,7 +25,7 @@ module GHC.Core.Predicate (
   classMethodTy, classMethodInstTy,
 
   -- Implicit parameters
-  isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,
+  isIPLikePred, mentionsIP, isIPTyCon, isIPClass,
   isCallStackTy, isCallStackPred, isCallStackPredTy,
   isIPPred_maybe,
 
@@ -260,39 +260,16 @@ isIPTyCon tc = tc `hasKey` ipClassKey
 isIPClass :: Class -> Bool
 isIPClass cls = cls `hasKey` ipClassKey
 
-isIPLikePred :: Type -> Bool
--- See Note [Local implicit parameters]
-isIPLikePred = is_ip_like_pred initIPRecTc
-
-
-is_ip_like_pred :: RecTcChecker -> Type -> Bool
-is_ip_like_pred rec_clss ty
-  | Just (tc, tys) <- splitTyConApp_maybe ty
-  , Just rec_clss' <- if isTupleTyCon tc  -- Tuples never cause recursion
-                      then Just rec_clss
-                      else checkRecTc rec_clss tc
-  , Just cls       <- tyConClass_maybe tc
-  = isIPClass cls || has_ip_super_classes rec_clss' cls tys
-
+-- | Decomposes a predicate if it is an implicit parameter. Does not look in
+-- superclasses. See also [Local implicit parameters].
+isIPPred_maybe :: Class -> [Type] -> Maybe (FastString, Type)
+isIPPred_maybe cls tys
+  | isIPClass cls
+  , [t1,t2] <- tys
+  , Just x <- isStrLitTy t1
+  = Just (x,t2)
   | otherwise
-  = False -- Includes things like (D []) where D is
-          -- a Constraint-ranged family; #7785
-
-hasIPSuperClasses :: Class -> [Type] -> Bool
--- See Note [Local implicit parameters]
-hasIPSuperClasses = has_ip_super_classes initIPRecTc
-
-has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool
-has_ip_super_classes rec_clss cls tys
-  = any ip_ish (classSCSelIds cls)
-  where
-    -- Check that the type of a superclass determines its value
-    -- sc_sel_id :: forall a b. C a b -> <superclass type>
-    ip_ish sc_sel_id = is_ip_like_pred rec_clss $
-                       classMethodInstTy sc_sel_id tys
-
-initIPRecTc :: RecTcChecker
-initIPRecTc = setRecTcMaxBound 1 initRecTc
+  = Nothing
 
 -- --------------------- CallStack predicates ---------------------------------
 
@@ -326,20 +303,48 @@ isCallStackTy ty
   | otherwise
   = False
 
+-- --------------------- isIPLike and mentionsIP  --------------------------
+--                 See Note [Local implicit parameters]
 
--- | Decomposes a predicate if it is an implicit parameter. Does not look in
--- superclasses. See also [Local implicit parameters].
-isIPPred_maybe :: Class -> [Type] -> Maybe (FastString, Type)
-isIPPred_maybe cls tys
-  | cls `hasKey` ipClassKey
-  , [t1,t2] <- tys
-  , Just x <- isStrLitTy t1
-  = Just (x,t2)
+isIPLikePred :: Type -> Bool
+-- Is `pred`, or any of its superclasses, an implicit parameter?
+-- See Note [Local implicit parameters]
+isIPLikePred pred = mentions_ip_pred initIPRecTc Nothing pred
+
+mentionsIP :: FastString -> Class -> [Type] -> Bool
+-- Is (cls tys) an implicit parameter with string `fs`, or
+-- is any of its superclasses such at thing.
+-- See Note [Local implicit parameters]
+mentionsIP fs cls tys = mentions_ip initIPRecTc (Just fs) cls tys
+
+mentions_ip :: RecTcChecker -> Maybe FastString -> Class -> [Type] -> Bool
+mentions_ip rec_clss mb_fs cls tys
+  | Just (fs', _) <- isIPPred_maybe cls tys
+  = case mb_fs of
+       Nothing -> True
+       Just fs -> fs == fs'
   | otherwise
-  = Nothing
+  = or [ mentions_ip_pred rec_clss mb_fs (classMethodInstTy sc_sel_id tys)
+       | sc_sel_id <- classSCSelIds cls ]
+
+mentions_ip_pred :: RecTcChecker -> Maybe FastString -> Type -> Bool
+mentions_ip_pred  rec_clss mb_fs ty
+  | Just (cls, tys) <- getClassPredTys_maybe ty
+  , let tc = classTyCon cls
+  , Just rec_clss' <- if isTupleTyCon tc then Just rec_clss
+                      else checkRecTc rec_clss tc
+  = mentions_ip rec_clss' mb_fs cls tys
+  | otherwise
+  = False -- Includes things like (D []) where D is
+          -- a Constraint-ranged family; #7785
+
+initIPRecTc :: RecTcChecker
+initIPRecTc = setRecTcMaxBound 1 initRecTc
 
 {- Note [Local implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Shadowing of Implicit Parameters] in GHC.Tc.Solver.Dict.
+
 The function isIPLikePred tells if this predicate, or any of its
 superclasses, is an implicit parameter.
 
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index f0303a9aa0..ac5f3aae25 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -106,8 +106,10 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
        ; stopWithStage (dictCtEvidence dict_ct) "Kept inert DictCt" }
 
 updInertDicts :: DictCt -> TcS ()
-updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
-  = do { -- See Note [Shadowing of Implicit Parameters]
+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]
        ; when (isGiven ev && isIPClass cls) $
          updInertCans (updDicts (delIPDict dict_ct))
 
@@ -195,7 +197,24 @@ in two places:
    (?x :: ty) in the inert set and an identical (?x :: ty) as the work item.
 
 * In `updInertDicts` in this module, when adding [G] (?x :: ty), remove  any
-  existing [G] (?x :: ty'), regardless of ty'
+  existing [G] (?x :: ty'), regardless of ty'.
+
+* Wrinkle (SIP1): we must be careful of superclasses.  Consider
+     f,g :: (?x::Int, C a) => a -> a
+     f v = let ?x = 4 in g v
+
+  The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
+  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] C tys, where (C 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 )
+
+* 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
 
 Example 1:
 
@@ -248,13 +267,14 @@ behaviour.
 
 All this works for the normal cases but it has an odd side effect in
 some pathological programs like this:
--- This is accepted, the second parameter shadows
-f1 :: (?x :: Int, ?x :: Char) => Char
-f1 = ?x
 
--- This is rejected, the second parameter shadows
-f2 :: (?x :: Int, ?x :: Char) => Int
-f2 = ?x
+    -- This is accepted, the second parameter shadows
+    f1 :: (?x :: Int, ?x :: Char) => Char
+    f1 = ?x
+
+    -- This is rejected, the second parameter shadows
+    f2 :: (?x :: Int, ?x :: Char) => Int
+    f2 = ?x
 
 Both of these are actually wrong:  when we try to use either one,
 we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
@@ -618,7 +638,8 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys
                            ; continueWith () } } }
 
   | otherwise
-  = continueWith ()
+  = do { traceTcS "tryInertDicts:no" (ppr dict_w $$ ppr cls <+> ppr tys)
+       ; continueWith () }
 
 -- See Note [Shortcut solving]
 shortCutSolver :: DynFlags
@@ -810,9 +831,10 @@ matchClassInst dflags inerts clas tys loc
 -- whether top level, or local quantified constraints.
 -- See Note [Instance and Given overlap]
   | not (xopt LangExt.IncoherentInstances dflags)
+  , not (isCTupleClass clas)  -- It is always safe to unpack constraint tuples
   , not (noMatchableGivenDicts inerts loc clas tys)
   = do { traceTcS "Delaying instance application" $
-           vcat [ text "Work item=" <+> pprClassPred clas tys ]
+           vcat [ text "Work item:" <+> pprClassPred clas tys ]
        ; return NotSure }
 
   | otherwise
@@ -989,7 +1011,7 @@ The same reasoning applies to
 And less obviously to:
 
 * Tuple classes.  For reasons described in GHC.Tc.Solver.Types
-  Note [Tuples hiding implicit parameters], we may have a constraint
+  Note [Shadowing of implicit parameters], we may have a constraint
      [W] (?x::Int, C a)
   with an exactly-matching Given constraint.  We must decompose this
   tuple and solve the components separately, otherwise we won't solve
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index 1b85fdab0c..f621de211b 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -79,6 +79,7 @@ import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 import GHC.Data.Maybe
 import GHC.Data.Bag
+import GHC.Data.FastString
 
 import Data.List.NonEmpty ( NonEmpty(..), (<|) )
 import qualified Data.List.NonEmpty as NE
@@ -321,6 +322,7 @@ data InertSet
 
        , inert_solved_dicts :: DictMap CtEvidence
               -- All Wanteds, of form (C t1 .. tn)
+              -- Always a dictionary solved by an instance decl; never an implict parameter
               -- See Note [Solved dictionaries]
               -- and Note [Do not add superclasses of solved dictionaries]
        }
@@ -1323,20 +1325,15 @@ delDict (DictCt { di_cls = cls, di_tys = tys }) m
   = delTcApp m (classTyCon cls) tys
 
 delIPDict :: DictCt -> DictMap DictCt -> DictMap DictCt
-delIPDict (DictCt { di_cls = cls, di_tys = tys }) m
-  | [ip_str, _] <- tys
-  = assert (isIPClass cls) $
-    filterDicts (doesn't_match ip_str) m
+delIPDict dict@(DictCt { di_cls = cls, di_tys = tys }) dict_map
+  | Just (fs, _) <- isIPPred_maybe cls tys
+  = filterDicts (doesn't_match fs) dict_map
   | otherwise
-  = m
+  = pprPanic "delIPDict" (ppr dict)
  where
-    doesn't_match :: TcType -> DictCt -> Bool
-    doesn't_match ip_str (DictCt { di_cls = cls, di_tys = tys })
-      | isIPClass cls
-      , [ip_str', _] <- tys
-      = not (ip_str `eqType` ip_str')
-      | otherwise
-      = True
+    doesn't_match :: FastString -> DictCt -> Bool
+    doesn't_match fs (DictCt { di_cls = cls, di_tys = tys })
+      = not (mentionsIP fs cls tys)
 
 addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
 addDict item@(DictCt { di_cls = cls, di_tys = tys }) dm
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index d385d27b29..c89a9f282b 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -707,9 +707,7 @@ lookupInInerts loc pty
 -- | Look up a dictionary inert.
 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
-  = case findDict dicts loc cls tys of
-      Just ct -> Just ct
-      _       -> Nothing
+  = findDict dicts loc cls tys
 
 -- | Look up a solved inert.
 lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs
index 0d34022df7..d47eef71b7 100644
--- a/compiler/GHC/Tc/Solver/Types.hs
+++ b/compiler/GHC/Tc/Solver/Types.hs
@@ -133,9 +133,6 @@ emptyDictMap = emptyTcAppMap
 
 findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
 findDict m loc cls tys
-  | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters]
-  = Nothing
-
   | Just {} <- isCallStackPred cls tys
   , isPushCallStackOrigin (ctLocOrigin loc)
   = Nothing             -- See Note [Solving CallStack constraints]
@@ -157,25 +154,8 @@ dictsToBag = tcAppMapToBag
 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
 foldDicts = foldTcAppMap
 
-{- Note [Tuples hiding implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   f,g :: (?x::Int, C a) => a -> a
-   f v = let ?x = 4 in g v
-
-The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
-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 we always fail when looking up a
-tuple constraint that hides an implicit parameter. Note that this applies
-  * both to the inert_dicts (lookupInertDict)
-  * and to the solved_dicts (looukpSolvedDict)
-An alternative would be not to extend these sets with such tuple
-constraints, but it seemed more direct to deal with the lookup.
-
-Note [Solving CallStack constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Solving CallStack constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence.
 
 Suppose f :: HasCallStack => blah.  Then
diff --git a/testsuite/tests/gadt/T3651.stderr b/testsuite/tests/gadt/T3651.stderr
index b4c7a2e65d..aaf69f6dec 100644
--- a/testsuite/tests/gadt/T3651.stderr
+++ b/testsuite/tests/gadt/T3651.stderr
@@ -6,7 +6,7 @@ T3651.hs:11:15: error: [GHC-83865]
     • In the expression: ()
       In an equation for ‘unsafe1’: unsafe1 B U = ()
 
-T3651.hs:14:15: error: [GHC-83865]
+T3651.hs:27:15: error: [GHC-83865]
     • Couldn't match type ‘()’ with ‘Bool’
       Expected: a
         Actual: ()
diff --git a/testsuite/tests/pmcheck/should_compile/T15450.stderr b/testsuite/tests/pmcheck/should_compile/T15450.stderr
index 18f4a931f8..ca5f6ae71c 100644
--- a/testsuite/tests/pmcheck/should_compile/T15450.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T15450.stderr
@@ -1,11 +1,11 @@
 
-T15450.hs:6:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
+T15450.hs:8:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative:
         Patterns of type ‘Bool’ not matched:
             False
             True
 
-T15450.hs:9:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
+T15450.hs:11:7: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns of type ‘Bool’ not matched: False
diff --git a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
index ae71b40a91..b615c3b86f 100644
--- a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
+++ b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
@@ -1,20 +1,20 @@
 
-GivenForallLoop.hs:8:11: error: [GHC-25897]
+GivenForallLoop.hs:9:11: error: [GHC-25897]
     • Could not deduce ‘a ~ b’
       from the context: a ~ (forall b1. F a b1)
         bound by the type signature for:
                    loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
-        at GivenForallLoop.hs:7:1-42
+        at GivenForallLoop.hs:8:1-42
       ‘a’ is a rigid type variable bound by
         the type signature for:
           loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
-        at GivenForallLoop.hs:7:1-42
+        at GivenForallLoop.hs:8:1-42
       ‘b’ is a rigid type variable bound by
         the type signature for:
           loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
-        at GivenForallLoop.hs:7:1-42
+        at GivenForallLoop.hs:8:1-42
     • In the expression: x
       In an equation for ‘loopy’: loopy x = x
     • Relevant bindings include
-        x :: a (bound at GivenForallLoop.hs:8:7)
-        loopy :: a -> b (bound at GivenForallLoop.hs:8:1)
+        x :: a (bound at GivenForallLoop.hs:9:7)
+        loopy :: a -> b (bound at GivenForallLoop.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/T20189.stderr b/testsuite/tests/typecheck/should_fail/T20189.stderr
index 077f57d6d5..e1dd352506 100644
--- a/testsuite/tests/typecheck/should_fail/T20189.stderr
+++ b/testsuite/tests/typecheck/should_fail/T20189.stderr
@@ -1,12 +1,12 @@
 
-T20189.hs:6:5: error: [GHC-88464]
+T20189.hs:7:5: error: [GHC-88464]
     • Found hole: _ :: t
       Where: ‘t’ is a rigid type variable bound by
                the type signature for:
                  y :: forall t. (t ~ (forall x. Show x => x -> IO ())) => t
-               at T20189.hs:5:1-49
+               at T20189.hs:6:1-49
     • In an equation for ‘y’: y = _
-    • Relevant bindings include y :: t (bound at T20189.hs:6:1)
+    • Relevant bindings include y :: t (bound at T20189.hs:7:1)
       Constraints include
-        t ~ (forall x. Show x => x -> IO ()) (from T20189.hs:5:1-49)
-      Valid hole fits include y :: t (bound at T20189.hs:6:1)
+        t ~ (forall x. Show x => x -> IO ()) (from T20189.hs:6:1-49)
+      Valid hole fits include y :: t (bound at T20189.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/T22924b.stderr b/testsuite/tests/typecheck/should_fail/T22924b.stderr
index ba4bd79198..46f456fc1f 100644
--- a/testsuite/tests/typecheck/should_fail/T22924b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T22924b.stderr
@@ -1,7 +1,7 @@
 
 T22924b.hs:10:5: error:
     • Reduction stack overflow; size = 201
-      When simplifying the following type: R
+      When simplifying the following type: S
       Use -freduction-depth=0 to disable this check
       (any upper bound you could choose might fail unpredictably with
        minor updates to GHC, so disabling the check is recommended if
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
index bbb18280c7..be1b5928b3 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
@@ -50,7 +50,7 @@ TcCoercibleFail.hs:30:9: error: [GHC-18872]
 
 TcCoercibleFail.hs:35:8: error:
     • Reduction stack overflow; size = 201
-      When simplifying the following type: Age
+      When simplifying the following type: Fix (Either Age)
       Use -freduction-depth=0 to disable this check
       (any upper bound you could choose might fail unpredictably with
        minor updates to GHC, so disabling the check is recommended if
diff --git a/testsuite/tests/typecheck/should_run/Defer01.hs b/testsuite/tests/typecheck/should_run/Defer01.hs
index 551c626f7c..8fcf999b32 100644
--- a/testsuite/tests/typecheck/should_run/Defer01.hs
+++ b/testsuite/tests/typecheck/should_run/Defer01.hs
@@ -1,8 +1,8 @@
 -- Test -fdefer-type-errors
 -- Should compile and run
-
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- Allows the strange type for `k`
 {-# OPTIONS_GHC -fdefer-type-errors #-}
 
 module Main where