Remove duplicate quantified constraints

This is an easy fix for Trac #15244: just avoid adding
the same quantified Given constraint to the inert set twice.

See TcSMonad Note [Do not add duplicate quantified instances].

4 files changed, 131 insertions, 31 deletions

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 3e41c61264..f20a17bf8f 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -2341,8 +2341,9 @@ matchClassInst :: DynFlags -> InertSet
                -> CtLoc -> TcS LookupInstResult
 matchClassInst dflags inerts clas tys loc
 -- First check whether there is an in-scope Given that could
--- match this constraint.  In that case, do not use top-level
--- instances.  See Note [Instance and Given overlap]
+-- match this constraint.  In that case, do not use any instance
+-- whether top level, or local quantified constraints.
+-- ee Note [Instance and Given overlap]
   | not (xopt LangExt.IncoherentInstances dflags)
   , not (naturallyCoherentClass clas)
   , let matchable_givens = matchableGivens loc pred inerts
@@ -2356,7 +2357,7 @@ matchClassInst dflags inerts clas tys loc
   = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
        ; local_res <- matchLocalInst pred loc
        ; case local_res of
-           OneInst {} ->
+           OneInst {} ->  -- See Note [Local instances and incoherence]
                 do { traceTcS "} matchClassInst local match" $ ppr local_res
                    ; return local_res }
 
@@ -2399,6 +2400,7 @@ naturallyCoherentClass cls
     || cls `hasKey` eqTyConKey
     || cls `hasKey` coercibleTyConKey
 
+
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Example, from the OutsideIn(X) paper:
@@ -2525,9 +2527,37 @@ Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
 
 PS: the term "naturally coherent" doesn't really seem helpful.
 Perhaps "invertible" or something?  I left it for now though.
+
+Note [Local instances and incoherence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
+                 => c b -> Bool
+   f x = x==x
+
+We get [W] Eq (c b), and we must use the local instance to solve it.
+
+BUT that wanted also unifies with the top-level Eq [a] instance,
+and Eq (Maybe a) etc.  We want the local instance to "win", otherwise
+we can't solve the wanted at all.  So we mark it as Incohherent.
+According to Note [Rules for instance lookup] in InstEnv, that'll
+make it win even if there are other instances that unify.
+
+Moreover this is not a hack!  The evidence for this local instance
+will be constructed by GHC at a call site... from the very instances
+that unify with it here.  It is not like an incoherent user-written
+instance which might have utterly different behaviour.
+
+Consdider  f :: Eq a => blah.  If we have [W] Eq a, we certainly
+get it from the Eq a context, without worrying that there are
+lots of top-level instances that unify with [W] Eq a!  We'll use
+those instances to build evidence to pass to f. That's just the
+nullary case of what's happening here.
 -}
 
 matchLocalInst :: TcPredType -> CtLoc -> TcS LookupInstResult
+-- Try any Given quantified constraints, which are
+-- effectively just local instance declarations.
 matchLocalInst pred loc
   = do { ics <- getInertCans
        ; case match_local_inst (inert_insts ics) of
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 9814358c74..b1865e829c 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -1483,35 +1483,35 @@ equalities arising from injectivity.
 
 addInertForAll :: QCInst -> TcS ()
 -- Add a local Given instance, typically arising from a type signature
-addInertForAll qci
+addInertForAll new_qci
   = updInertCans $ \ics ->
-    ics { inert_insts = qci : inert_insts ics }
-
-{- Note [Local instances and incoherence]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
-                 => c b -> Bool
-   f x = x==x
-
-We get [W] Eq (c b), and we must use the local instance to solve it.
-
-BUT that wanted also unifies with the top-level Eq [a] instance,
-and Eq (Maybe a) etc.  We want the local instance to "win", otherwise
-we can't solve the wanted at all.  So we mark it as Incohherent.
-According to Note [Rules for instance lookup] in InstEnv, that'll
-make it win even if there are other instances that unify.
-
-Moreover this is not a hack!  The evidence for this local instance
-will be constructed by GHC at a call site... from the very instances
-that unify with it here.  It is not like an incoherent user-written
-instance which might have utterly different behaviour.
-
-Consdider  f :: Eq a => blah.  If we have [W] Eq a, we certainly
-get it from the Eq a context, without worrying that there are
-lots of top-level instances that unify with [W] Eq a!  We'll use
-those instances to build evidence to pass to f. That's just the
-nullary case of what's happening here.
+    ics { inert_insts = add_qci (inert_insts ics) }
+  where
+    add_qci :: [QCInst] -> [QCInst]
+    -- See Note [Do not add duplicate quantified instances]
+    add_qci qcis | any same_qci qcis = qcis
+                 | otherwise         = new_qci : qcis
+
+    same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci))
+                                (ctEvPred (qci_ev new_qci))
+
+{- Note [Do not add duplicate quantified instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this (Trac #15244):
+
+  f :: (C g, D g) => ....
+  class S g => C g where ...
+  class S g => D g where ...
+  class (forall a. Eq a => Eq (g a)) => S g where ...
+
+Then in f's RHS there are two identical quantified constraints
+available, one via the superclasses of C and one via the superclasses
+of D.  The two are identical, and it seems wrong to reject the program
+because of that. But without doing duplicate-elimination we will have
+two matching QCInsts when we try to solve constraints arising from f's
+RHS.
+
+The simplest thing is simply to eliminate duplicattes, which we do here.
 -}
 
 {- *********************************************************************
diff --git a/testsuite/tests/quantified-constraints/T15244.hs b/testsuite/tests/quantified-constraints/T15244.hs
new file mode 100644
index 0000000000..16d2b65d53
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T15244.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE QuantifiedConstraints, TypeFamilies #-}
+
+module T15244 where
+class (forall t . Eq (c t)) => Blah c
+
+-- Unquantified works
+foo :: (Eq (a t), Eq (b t), a ~ b) => a t -> b t -> Bool
+foo a b = a == b
+-- Works
+
+-- Two quantified instances fail with double ambiguity check errors
+bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool
+bar a b = a == b
+-- Minimal.hs:11:8: error:
+--     • Could not deduce (Eq (b t1))
+--       from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),
+--                          a ~ b)
+--         bound by the type signature for:
+--                    bar :: forall (a :: * -> *) (b :: * -> *) t.
+--                           (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>
+--                           a t -> b t -> Bool
+--         at Minimal.hs:11:8-78
+--     • In the ambiguity check for ‘bar’
+--       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+--       In the type signature:
+--         bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>
+--                a t -> b t -> Bool
+--    |
+-- 11 | bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool
+--    |
+-- [And then another copy of the same error]
+
+-- Two copies from superclass instances fail
+baz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool
+baz a b = a == b
+-- Minimal.hs:34:11: error:
+--     • Could not deduce (Eq (b t)) arising from a use of ‘==’
+--       from the context: (Blah a, Blah b, a ~ b)
+--         bound by the type signature for:
+--                    baz :: forall (a :: * -> *) (b :: * -> *) t.
+--                           (Blah a, Blah b, a ~ b) =>
+--                           a t -> b t -> Bool
+--         at Minimal.hs:33:1-52
+--     • In the expression: a == b
+--       In an equation for ‘baz’: baz a b = a == b
+--    |
+-- 34 | baz a b = a == b
+--    |
+
+-- Two copies from superclass from same declaration also fail
+mugga :: (Blah a, Blah a) => a t -> a t -> Bool
+mugga a b = a == b
+--     • Could not deduce (Eq (a t)) arising from a use of ‘==’
+--       from the context: (Blah a, Blah a)
+--         bound by the type signature for:
+--                    mugga :: forall (a :: * -> *) t.
+--                             (Blah a, Blah a) =>
+--                             a t -> a t -> Bool
+--         at Minimal.hs:50:1-47
+--     • In the expression: a == b
+--       In an equation for ‘mugga’: mugga a b = a == b
+--    |
+-- 51 | mugga a b = a == b
+--    |
+
+-- One copy works
+quux :: (Blah a, a ~ b) => a t -> b t -> Bool
+quux a b = a == b
+-- Works
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 71f5b9159a..e546a7c495 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -8,3 +8,4 @@ test('T9123', normal, compile, [''])
 test('T14863', normal, compile, [''])
 test('T14961', normal, compile, [''])
 test('T9123a', normal, compile, [''])
+test('T15244', normal, compile, [''])