PmCheck: Adjust recursion depth for inhabitation test

In #17977, we ran into the reduction depth limit of the typechecker.
That was only a symptom of a much broader issue: The recursion depth
of the coverage checker for trying to instantiate strict fields in the
`nonVoid` test was far too high (100, the `defaultMaxTcBound`).

As a result, we were performing quite poorly on `T17977`.
Short of a proper termination analysis to prove emptyness of a type,
we just arbitrarily default to a much lower recursion limit of 3.

Fixes #17977.

4 files changed, 65 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T17977.hs b/testsuite/tests/pmcheck/should_compile/T17977.hs
new file mode 100644
index 0000000000..4905989ead
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17977.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+import Data.Kind
+import Data.Type.Equality
+
+data Nat = Z | S Nat
+
+data SNat :: Nat -> Type where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+
+type family S' (n :: Nat) :: Nat where
+  S' n = S n
+
+data R :: Nat -> Nat -> Nat -> Type where
+  MkR :: !(R m n o) -> R (S m) n (S o)
+
+type family NatPlus (m :: Nat) (n :: Nat) :: Nat where
+  NatPlus Z     n = n
+  NatPlus (S m) n = S' (NatPlus m n)
+
+f :: forall (m :: Nat) (n :: Nat) (o :: Nat).
+     SNat m -> SNat n -> SNat o
+  -> R m n o -> NatPlus m n :~: o
+f (SS sm) sn (SS so) (MkR r)
+  | Refl <- f sm sn so r
+  = Refl
diff --git a/testsuite/tests/pmcheck/should_compile/T17977b.hs b/testsuite/tests/pmcheck/should_compile/T17977b.hs
new file mode 100644
index 0000000000..c6b81f5439
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17977b.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE EmptyCase #-}
+module Bug where
+
+import Data.Kind
+
+data Nat = Z | S Nat
+
+data Down :: Nat -> Type where
+  Down :: !(Down n) -> Down (S n)
+
+data Up :: Nat -> Type where
+  Up :: !(Up (S n)) -> Up n
+
+f :: Down n -> ()
+f (Down r) = ()
+
+f' :: Down (S (S (S (S Z)))) -> ()
+f' (Down r) = ()
+
+g :: Up n -> ()
+g (Up r) = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17977b.stderr b/testsuite/tests/pmcheck/should_compile/T17977b.stderr
new file mode 100644
index 0000000000..d46492db22
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17977b.stderr
@@ -0,0 +1,4 @@
+
+T17977b.hs:21:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f'’: f' (Down r) = ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 6295fa77ab..0c3bfcf510 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -114,6 +114,10 @@ test('T17703', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17783', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17977', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,