Fixes #19627.wip/T19627

Previously the solver failed with an unhelpful "solver reached too may iterations" error.
With the fix for #21909 in place we no longer have the possibility of generating such an error if we have `-fconstraint-solver-iteration` > `-fgivens-fuel > `-fwanteds-fuel`. This is true by default, and the said fix also gives programmers a knob to control how hard the solver should try before giving up.

This commit adds:
* Reference to ticket #19627 in the Note [Expanding Recursive Superclasses and ExpansionFuel]
* Test `typecheck/should_fail/T19627.hs` for regression purposes

4 files changed, 156 insertions, 2 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 81fa86aea4..fad6cbae4f 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -2371,7 +2371,7 @@ any new unifications, and iterate the implications only if so.
 -}
 
 {- Note [Expanding Recursive Superclasses and ExpansionFuel]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the class declaration (T21909)
 
     class C [a] => C a where
@@ -2431,7 +2431,7 @@ There are two preconditions for the default fuel values:
 Precondition (1) ensures that we expand givens at least as many times as we expand wanted constraints
 preferably givenFuel > wantedsFuel to avoid issues like T21909 while
 the precondition (2) ensures that we do not reach the solver iteration limit and fail with a
-more meaningful error message
+more meaningful error message (see T19627)
 
 This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field.
 -}
diff --git a/testsuite/tests/typecheck/should_fail/T19627.hs b/testsuite/tests/typecheck/should_fail/T19627.hs
new file mode 100644
index 0000000000..8e79e14c47
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19627.hs
@@ -0,0 +1,108 @@
+{-# language BlockArguments #-}
+{-# language DefaultSignatures #-}
+{-# language DerivingStrategies #-}
+{-# language EmptyCase #-}
+{-# language ExplicitNamespaces #-}
+{-# language ImportQualifiedPost #-}
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language FunctionalDependencies #-}
+{-# language GADTs #-}
+{-# language LambdaCase #-}
+{-# language LinearTypes #-}
+{-# language NoStarIsType #-}
+{-# language PolyKinds #-}
+{-# language QuantifiedConstraints #-}
+{-# language RankNTypes #-}
+{-# language RoleAnnotations #-}
+{-# language ScopedTypeVariables #-}
+{-# language StandaloneDeriving #-}
+{-# language StandaloneKindSignatures #-}
+{-# language StrictData #-}
+{-# language TupleSections #-}
+{-# language TypeApplications #-}
+{-# language TypeFamilies #-}
+{-# language TypeFamilyDependencies #-}
+{-# language TypeOperators #-}
+{-# language UndecidableInstances #-}
+{-# language UndecidableSuperClasses #-}
+
+module T19627 where
+
+import Data.Kind
+import Prelude hiding ( Functor(..) )
+
+--------------------
+
+class (Prop (Not p), Not (Not p) ~ p) => Prop (p :: Type) where
+  type Not p :: Type
+  (!=) :: p -> Not p -> r
+
+data Y (a :: Type) (b :: Type) (c :: Type) where
+  L :: Y a b a
+  R :: Y a b b
+
+newtype a & b = With (forall c. Y a b c -> c)
+
+with :: (forall c. Y a b c -> c) -> a & b
+with = With
+
+runWith :: a & b -> Y a b c -> c
+runWith (With f) = f
+
+withL' :: a & b -> a
+withL' (With f) = f L
+
+withR' :: a & b -> b
+withR' (With f) = f R
+
+instance (Prop a, Prop b) => Prop (a & b) where
+  type Not (a & b) = Not a `Either` Not b
+  w != Left a  = withL' w != a
+  w != Right b = withR' w != b
+
+instance (Prop a, Prop b) => Prop (Either a b) where
+  type Not (Either a b) = Not a & Not b
+  Left a  != w = a != withL' w
+  Right a != w = a != withR' w
+
+newtype Yoneda f a = Yoneda
+  (forall r. Prop r => (a -> r) -> f r)
+
+data Noneda f a where
+  Noneda :: Prop r => !(f r <#- (a ⊸ r)) -> Noneda f a
+
+liftYoneda :: forall f a i. (Functor f, Prop a, Iso i) => i (f a) (Yoneda f a)
+liftYoneda = iso \case
+  L -> lowerYoneda'
+  R -> lol \case
+    L -> \(Noneda ((a2r :: a ⊸ r) :-#> nfr)) -> runLol (fmap @f @a @r a2r) L nfr
+    R -> \fa -> Yoneda do
+      lol \case
+        R -> \f -> fmap' f fa
+        L -> \nfr -> whyNot \a2r -> fmap a2r fa != nfr
+
+
+type family NotApart (p :: Type -> Type -> Type) :: Type -> Type -> Type
+
+class
+  ( forall a b. (Prop a, Prop b) => Prop (p a b)
+  , NotApart (NotIso p) ~ p
+  ) => Iso p where
+  type NotIso p = (q :: Type -> Type -> Type) | q -> p
+  iso :: (forall c. Y (b ⊸ a) (a ⊸ b) c -> c) -> p a b
+
+data b <#- a where (:-#>) :: a -> Not b -> b <#- a
+newtype a ⊸ b = Lol (forall c. Y (Not b %1 -> Not a) (a %1 -> b) c -> c)
+
+class
+  ( forall a. Prop a => Prop (f a)
+  ) => Functor f where
+  fmap' :: (Prop a, Prop b, Lol l, Lol l') => l ((a ⊸ b)) (l' (f a) (f b))
+
+fmap :: forall f a b l. (Functor f, Prop a, Prop b, Lol l) => (a ⊸ b) -> l (f a) (f b)
+fmap f = fmap' f
+
+class Iso p => Lol (p :: Type -> Type -> Type) where
+  lol :: (forall c. Y (Not b -> Not a) (a -> b) c -> c) -> p a b
+  apartR :: Not (p a b) -> b <#- a
diff --git a/testsuite/tests/typecheck/should_fail/T19627.stderr b/testsuite/tests/typecheck/should_fail/T19627.stderr
new file mode 100644
index 0000000000..af80fdc74d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19627.stderr
@@ -0,0 +1,45 @@
+
+T19627.hs:108:3: error: [GHC-05617]
+    • Could not deduce ‘Not (p0 a b) ~ Not (p a b)’
+      from the context: Lol p
+        bound by the type signature for:
+                   apartR :: forall (p :: * -> * -> *) a b.
+                             Lol p =>
+                             Not (p a b) -> b <#- a
+        at T19627.hs:108:3-34
+      Expected: Not (p a b) -> b <#- a
+        Actual: Not (p0 a b) -> b <#- a
+        NB: ‘Not’ is a non-injective type family
+        The type variable ‘p0’ is ambiguous
+    • In the ambiguity check for ‘apartR’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the class method:
+        apartR :: forall (p :: * -> * -> *) a b.
+                  Lol p =>
+                  Not (p a b) -> b <#- a
+      In the class declaration for ‘Lol’
+
+T19627.hs:108:3: error: [GHC-05617]
+    • Could not deduce ‘Not (Not (p0 a1 b1)) ~ p0 a1 b1’
+        arising from a superclass required to satisfy ‘Prop (p0 a1 b1)’,
+        arising from the head of a quantified constraint
+        arising from a superclass required to satisfy ‘Iso p0’,
+        arising from a superclass required to satisfy ‘Lol p0’,
+        arising from a type ambiguity check for
+        the type signature for ‘apartR’
+      from the context: Lol p
+        bound by the type signature for:
+                   apartR :: forall (p :: * -> * -> *) a b.
+                             Lol p =>
+                             Not (p a b) -> b <#- a
+        at T19627.hs:108:3-34
+      or from: (Prop a1, Prop b1)
+        bound by a quantified context at T19627.hs:108:3-34
+        The type variable ‘p0’ is ambiguous
+    • In the ambiguity check for ‘apartR’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the class method:
+        apartR :: forall (p :: * -> * -> *) a b.
+                  Lol p =>
+                  Not (p a b) -> b <#- a
+      In the class declaration for ‘Lol’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index bf03352115..94f0cdfa77 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -671,3 +671,4 @@ test('T20666a', normal, compile, [''])  # To become compile_fail after migration
 test('T22924a', normal, compile_fail, [''])
 test('T22924b', normal, compile_fail, [''])
 test('T22940', normal, compile_fail, [''])
+test('T19627', normal, compile_fail, [''])