PmCheck: Adjust recursion depth for inhabitation testwip/T17977

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.

5 files changed, 98 insertions, 9 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 67d10628dc..a4d849c910 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -1319,10 +1319,11 @@ checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool
 checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
   let definitely_inhabited = definitelyInhabitedType (delta_ty_st amb_cs)
   tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
+  -- See Note [Fuel for the inhabitation test]
   let rec_max_bound | tys_to_check `lengthExceeds` 1
                     = 1
                     | otherwise
-                    = defaultRecTcMaxBound
+                    = 3
       rec_ts' = setRecTcMaxBound rec_max_bound rec_ts
   allM (nonVoid rec_ts' amb_cs) tys_to_check
 
@@ -1342,6 +1343,7 @@ nonVoid rec_ts amb_cs strict_arg_ty = do
   mb_cands <- inhabitationCandidates amb_cs strict_arg_ty
   case mb_cands of
     Right (tc, _, cands)
+      -- See Note [Fuel for the inhabitation test]
       |  Just rec_ts' <- checkRecTc rec_ts tc
       -> anyM (cand_is_inhabitable rec_ts' amb_cs) cands
            -- A strict argument type is inhabitable by a terminating value if
@@ -1390,7 +1392,7 @@ definitelyInhabitedType ty_st ty = do
       null (dataConImplBangs con) -- (2)
 
 {- Note [Strict argument type constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the ConVar case of clause processing, each conlike K traditionally
 generates two different forms of constraints:
 
@@ -1420,6 +1422,7 @@ say, `K2 undefined` or `K2 (let x = x in x)`.)
 Since neither the term nor type constraints mentioned above take strict
 argument types into account, we make use of the `nonVoid` function to
 determine whether a strict type is inhabitable by a terminating value or not.
+We call this the "inhabitation test".
 
 `nonVoid ty` returns True when either:
 1. `ty` has at least one InhabitationCandidate for which both its term and type
@@ -1445,15 +1448,20 @@ determine whether a strict type is inhabitable by a terminating value or not.
   `nonVoid MyVoid` returns False. The InhabitationCandidate for the MkMyVoid
   constructor contains Void as a strict argument type, and since `nonVoid Void`
   returns False, that InhabitationCandidate is discarded, leaving no others.
+* Whether or not a type is inhabited is undecidable in general.
+  See Note [Fuel for the inhabitation test].
+* For some types, inhabitation is evident immediately and we don't need to
+  perform expensive tests. See Note [Types that are definitely inhabitable].
 
-* Performance considerations
+Note [Fuel for the inhabitation test]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Whether or not a type is inhabited is undecidable in general. As a result, we
+can run into infinite loops in `nonVoid`. Therefore, we adopt a fuel-based
+approach to prevent that.
 
-We must be careful when recursively calling `nonVoid` on the strict argument
-types of an InhabitationCandidate, because doing so naïvely can cause GHC to
-fall into an infinite loop. Consider the following example:
+Consider the following example:
 
   data Abyss = MkAbyss !Abyss
-
   stareIntoTheAbyss :: Abyss -> a
   stareIntoTheAbyss x = case x of {}
 
@@ -1474,7 +1482,6 @@ stareIntoTheAbyss above. Then again, the same problem occurs with recursive
 newtypes, like in the following code:
 
   newtype Chasm = MkChasm Chasm
-
   gazeIntoTheChasm :: Chasm -> a
   gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive
 
@@ -1498,9 +1505,26 @@ maximum recursion depth to 1 to mitigate the problem. If the branching factor
 is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay
 to stick with a larger maximum recursion depth.
 
+In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was
+too large and had detrimental effect on performance of the coverage checker.
+Given that we only commit to a best effort anyway, we decided to substantially
+decrement the recursion depth to 3, at the cost of precision in some edge cases
+like
+
+  data Nat = Z | S Nat
+  data Down :: Nat -> Type where
+    Down :: !(Down n) -> Down (S n)
+  f :: Down (S (S (S (S (S Z))))) -> ()
+  f x = case x of {}
+
+Since the coverage won't bother to instantiate Down 4 levels deep to see that it
+is in fact uninhabited, it will emit a inexhaustivity warning for the case.
+
+Note [Types that are definitely inhabitable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Another microoptimization applies to data types like this one:
 
-  data S a = ![a] !T
+  data S a = S ![a] !T
 
 Even though there is a strict field of type [a], it's quite silly to call
 nonVoid on it, since it's "obvious" that it is inhabitable. To make this
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,