Use transSuperClasses in TcErrorswip/T16414

Code in TcErrors was recursively using immSuperClasses,
which loops in the presence of UndecidableSuperClasses.

Better to use transSuperClasses instead, which has a loop-breaker
mechanism built in.

Fixes issue #16414.

5 files changed, 62 insertions, 12 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index d56e344454..3f0f82cb1d 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -2577,15 +2577,15 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over
                             2 (sep [ text "bound by" <+> ppr skol_info
                                    , text "at" <+>
                                      ppr (tcl_loc (implicLclEnv implic)) ])
-        where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
-              ev_var_matches ty = case getClassPredTys_maybe ty of
-                 Just (clas', tys')
-                   | clas' == clas
-                   , Just _ <- tcMatchTys tys tys'
-                   -> True
-                   | otherwise
-                   -> any ev_var_matches (immSuperClasses clas' tys')
-                 Nothing -> False
+        where ev_vars_matching = [ pred
+                                 | ev_var <- evvars
+                                 , let pred = evVarPred ev_var
+                                 , any can_match (pred : transSuperClasses pred) ]
+              can_match pred
+                 = case getClassPredTys_maybe pred of
+                     Just (clas', tys') -> clas' == clas
+                                          && isJust (tcMatchTys tys tys')
+                     Nothing -> False
 
     -- Overlap error because of Safe Haskell (first
     -- match should be the most specific match)
@@ -2716,7 +2716,7 @@ the alleged "provided" constraints, Show a.
 
 So we suppress that Implication in discardProvCtxtGivens.  It's
 painfully ad-hoc but the truth is that adding it to the "required"
-constraints would work.  Suprressing it solves two problems.  First,
+constraints would work.  Suppressing it solves two problems.  First,
 we never tell the user that we could not deduce a "provided"
 constraint from the "required" context. Second, we never give a
 possible fix that suggests to add a "provided" constraint to the
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 155037b775..d4bac5c12b 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -2011,8 +2011,25 @@ isInsolubleOccursCheck eq_rel tv ty
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we expand superclasses, we use the following algorithm:
 
-expand( so_far, pred ) returns the transitive superclasses of pred,
-                               not including pred itself
+transSuperClasses( C tys ) returns the transitive superclasses
+                           of (C tys), not including C itself
+
+For example
+  class C a b => D a b
+  class D b a => C a b
+
+Then
+  transSuperClasses( Ord ty )  = [Eq ty]
+  transSuperClasses( C ta tb ) = [D tb ta, C tb ta]
+
+Notice that in the recursive-superclass case we include C again at
+the end of the chain.  One could exclude C in this case, but
+the code is more awkward and there seems no good reason to do so.
+(However C.f. TcCanonical.mk_strict_superclasses, which /does/
+appear to do so.)
+
+The algorithm is expand( so_far, pred ):
+
  1. If pred is not a class constraint, return empty set
        Otherwise pred = C ts
  2. If C is in so_far, return empty set (breaks loops)
@@ -2024,6 +2041,8 @@ Notice that
  * With normal Haskell-98 classes, the loop-detector will never bite,
    so we'll get all the superclasses.
 
+ * We need the loop-breaker in case we have UndecidableSuperClasses on
+
  * Since there is only a finite number of distinct classes, expansion
    must terminate.
 
diff --git a/testsuite/tests/typecheck/should_fail/T16414.hs b/testsuite/tests/typecheck/should_fail/T16414.hs
new file mode 100644
index 0000000000..27807e82bf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16414.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+module T16414 where
+
+data I = I
+
+class All2 x => All x
+class All x => All2 x
+
+class AllZip2 f
+instance AllZip2 f
+
+f1 :: (All x, AllZip2 I) => x -> ()
+f1 = f2
+
+f2 :: AllZip2 f => x -> ()
+f2 _ = ()
diff --git a/testsuite/tests/typecheck/should_fail/T16414.stderr b/testsuite/tests/typecheck/should_fail/T16414.stderr
new file mode 100644
index 0000000000..5cfbf7549a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16414.stderr
@@ -0,0 +1,13 @@
+
+T16414.hs:14:6: error:
+    • Overlapping instances for AllZip2 f0 arising from a use of ‘f2’
+      Matching givens (or their superclasses):
+        AllZip2 I
+          bound by the type signature for:
+                     f1 :: forall x. (All x, AllZip2 I) => x -> ()
+          at T16414.hs:13:1-35
+      Matching instances:
+        instance AllZip2 f -- Defined at T16414.hs:11:10
+      (The choice depends on the instantiation of ‘f0’)
+    • In the expression: f2
+      In an equation for ‘f1’: f1 = f2
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 1a775d3a7c..54cd211e50 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -510,3 +510,4 @@ test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
     ['T16059e', '-v0'])
 test('T16255', normal, compile_fail, [''])
 test('T16204c', normal, compile_fail, [''])
+test('T16414', normal, compile_fail, [''])