From ed58d4fdcbc7b4fa8fbdf3d638a8d53c444ef4f2 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 30 Mar 2020 21:41:27 +0200 Subject: 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. --- compiler/GHC/HsToCore/PmCheck/Oracle.hs | 42 +++++++++++++++++----- testsuite/tests/pmcheck/should_compile/T17977.hs | 33 +++++++++++++++++ testsuite/tests/pmcheck/should_compile/T17977b.hs | 24 +++++++++++++ .../tests/pmcheck/should_compile/T17977b.stderr | 4 +++ testsuite/tests/pmcheck/should_compile/all.T | 4 +++ 5 files changed, 98 insertions(+), 9 deletions(-) create mode 100644 testsuite/tests/pmcheck/should_compile/T17977.hs create mode 100644 testsuite/tests/pmcheck/should_compile/T17977b.hs create mode 100644 testsuite/tests/pmcheck/should_compile/T17977b.stderr 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, -- cgit v1.2.1