Add a recursivity check in nonVoid

Summary:
Previously `nonVoid` outright refused to call itself
recursively to avoid the risk of hitting infinite loops when
checking recurisve types. But this is too conservative—we //can//
call `nonVoid` recursively as long as we incorporate a way to detect
the presence of recursive types, and bail out if we do detect one.
Happily, such a mechanism already exists in the form of `checkRecTc`,
so let's use it.

Test Plan: make test TEST=T15584

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15584

Differential Revision: https://phabricator.haskell.org/D5116

1 files changed, 142 insertions, 49 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index d57e34a79c..24ce3a9ebb 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -438,7 +438,7 @@ checkEmptyCase' var = do
 
     -- A list of inhabitant candidates is available: Check for each
     -- one for the satisfiability of the constraints it gives rise to.
-    Right candidates -> do
+    Right (_, candidates) -> do
       missing_m <- flip mapMaybeM candidates $
           \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
                                 , ic_ty_cs = ty_cs
@@ -610,18 +610,15 @@ pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do
     Just delta -> do
       -- We know that the term and type constraints are inhabitable, so now
       -- check if each strict argument type is inhabitable.
-      non_voids <- traverse (nonVoid delta) strict_arg_tys
-      pure $ if and non_voids -- Check if each strict argument type
-                              -- is inhabitable
+      all_non_void <- checkAllNonVoid initRecTc delta strict_arg_tys
+      pure $ if all_non_void -- Check if each strict argument type
+                             -- is inhabitable
                 then Just delta
                 else Nothing
 
 -- | Like 'pmIsSatisfiable', but only checks if term and type constraints are
 -- satisfiable, and doesn't bother checking anything related to strict argument
--- types. It's handy to have this factored out into is own function since term
--- and type constraints are the only forms of constraints that are checked for
--- each 'InhabitationCandidate' in 'nonVoid'
--- (as discussed in @Note [Extensions to GADTs Meet Their Match]@).
+-- types.
 tmTyCsAreSatisfiable
   :: Delta     -- ^ The ambient term and type constraints
                --   (known to be satisfiable).
@@ -642,38 +639,85 @@ tmTyCsAreSatisfiable
                                                  , delta_tm_cs = term_cs }
            _unsat               -> Nothing
 
+-- | Implements two performance optimizations, as described in the
+-- \"Strict argument type constraints\" section of
+-- @Note [Extensions to GADTs Meet Their Match]@.
+checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
+checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
+  fam_insts <- liftD dsGetFamInstEnvs
+  let tys_to_check = filterOut (definitelyInhabitedType fam_insts)
+                               strict_arg_tys
+      rec_max_bound | tys_to_check `lengthExceeds` 1
+                    = 1
+                    | otherwise
+                    = defaultRecTcMaxBound
+      rec_ts' = setRecTcMaxBound rec_max_bound rec_ts
+  allM (nonVoid rec_ts' amb_cs) tys_to_check
+
 -- | Checks if a strict argument type of a conlike is inhabitable by a
 -- terminating value (i.e, an 'InhabitationCandidate').
 -- See @Note [Extensions to GADTs Meet Their Match]@.
 nonVoid
-  :: Delta    -- ^ The ambient term/type constraints (known to be satisfiable).
-  -> Type     -- ^ The strict argument type.
-  -> PmM Bool -- ^ 'True' if the strict argument type might be inhabited by a
-              --   terminating value (i.e., an 'InhabitationCandidate').
-              --   'False' if it is definitely uninhabitable by anything
-              --   (except bottom).
-nonVoid amb_cs strict_arg_ty = do
+  :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit.
+  -> Delta        -- ^ The ambient term/type constraints (known to be
+                  --   satisfiable).
+  -> Type         -- ^ The strict argument type.
+  -> PmM Bool     -- ^ 'True' if the strict argument type might be inhabited by
+                  --   a terminating value (i.e., an 'InhabitationCandidate').
+                  --   'False' if it is definitely uninhabitable by anything
+                  --   (except bottom).
+nonVoid rec_ts amb_cs strict_arg_ty = do
   fam_insts <- liftD dsGetFamInstEnvs
   mb_cands <- inhabitationCandidates fam_insts strict_arg_ty
   case mb_cands of
-    Left _ -> pure True -- The type is trivially inhabited
-    Right cands -> do
-      cand_inhabs <- traverse cand_tm_ty_cs_are_satisfiable cands
-      pure $ or cand_inhabs
-        -- A strict argument type is inhabitable by a terminating value if at
-        -- least one InhabitationCandidate is satisfiable
+    Right (tc, cands)
+      |  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
+           -- at least one InhabitationCandidate is inhabitable.
+    _ -> pure True
+           -- Either the type is trivially inhabited or we have exceeded the
+           -- recursion depth for some TyCon (so bail out and conservatively
+           -- claim the type is inhabited).
   where
-    -- Checks if an InhabitationCandidate for a strict argument type has
-    -- satisfiable term and type constraints. We deliberately don't call
-    -- nonVoid on the InhabitationCandidate's own strict argument types, since
-    -- that can result in infinite loops.
+    -- Checks if an InhabitationCandidate for a strict argument type:
+    --
+    -- (1) Has satisfiable term and type constraints.
+    -- (2) Has 'nonVoid' strict argument types (we bail out of this
+    --     check if recursion is detected).
+    --
     -- See Note [Extensions to GADTs Meet Their Match]
-    cand_tm_ty_cs_are_satisfiable :: InhabitationCandidate -> PmM Bool
-    cand_tm_ty_cs_are_satisfiable
-      (InhabitationCandidate{ ic_tm_ct = new_term_c
-                            , ic_ty_cs = new_ty_cs }) = do
+    cand_is_inhabitable :: RecTcChecker -> Delta
+                        -> InhabitationCandidate -> PmM Bool
+    cand_is_inhabitable rec_ts amb_cs
+      (InhabitationCandidate{ ic_tm_ct          = new_term_c
+                            , ic_ty_cs          = new_ty_cs
+                            , ic_strict_arg_tys = new_strict_arg_tys }) = do
         mb_sat <- tmTyCsAreSatisfiable amb_cs new_term_c new_ty_cs
-        pure $ isJust mb_sat
+        case mb_sat of
+          Nothing -> pure False
+          Just new_delta -> do
+            checkAllNonVoid rec_ts new_delta new_strict_arg_tys
+
+-- | @'definitelyInhabitedType' ty@ returns 'True' if @ty@ has at least one
+-- constructor @C@ such that:
+--
+-- 1. @C@ has no equality constraints.
+-- 2. @C@ has no strict argument types.
+--
+-- See the \"Strict argument type constraints\" section of
+-- @Note [Extensions to GADTs Meet Their Match]@.
+definitelyInhabitedType :: FamInstEnvs -> Type -> Bool
+definitelyInhabitedType env ty
+  | Just (_, cons, _) <- pmTopNormaliseType_maybe env ty
+  = any meets_criteria cons
+  | otherwise
+  = False
+  where
+    meets_criteria :: DataCon -> Bool
+    meets_criteria con =
+      null (dataConEqSpec con) && -- (1)
+      null (dataConImplBangs con) -- (2)
 
 {- Note [Type normalisation for EmptyCase]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -733,7 +777,7 @@ Which means that in source Haskell:
 -- one accompanied by the term- and type- constraints it gives rise to.
 -- See also Note [Checking EmptyCase Expressions]
 inhabitationCandidates :: FamInstEnvs -> Type
-                       -> PmM (Either Type [InhabitationCandidate])
+                       -> PmM (Either Type (TyCon, [InhabitationCandidate]))
 inhabitationCandidates fam_insts ty
   = case pmTopNormaliseType_maybe fam_insts ty of
       Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
@@ -751,7 +795,7 @@ inhabitationCandidates fam_insts ty
 
     -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
     alts_to_check :: Type -> Type -> [DataCon]
-                  -> PmM (Either Type [InhabitationCandidate])
+                  -> PmM (Either Type (TyCon, [InhabitationCandidate]))
     alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
       Just (tc, _)
         |  tc `elem` trivially_inhabited
@@ -759,9 +803,9 @@ inhabitationCandidates fam_insts ty
              []    -> return (Left src_ty)
              (_:_) -> do var <- liftD $ mkPmId core_ty
                          let va = build_tm (PmVar var) dcs
-                         return $ Right [InhabitationCandidate
+                         return $ Right (tc, [InhabitationCandidate
                            { ic_val_abs = va, ic_tm_ct = mkIdEq var
-                           , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }]
+                           , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }])
 
         |  pmIsClosedType core_ty && not (isAbstractTyCon tc)
            -- Don't consider abstract tycons since we don't know what their
@@ -770,8 +814,9 @@ inhabitationCandidates fam_insts ty
         -> liftD $ do
              var  <- mkPmId core_ty -- it would be wrong to unify x
              alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
-             return $ Right [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs}
-                            | alt <- alts ]
+             return $ Right
+               (tc, [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs}
+                    | alt <- alts ])
       -- For other types conservatively assume that they are inhabited.
       _other -> return (Left src_ty)
 
@@ -1419,7 +1464,8 @@ determine whether a strict type is inhabitable by a terminating value or not.
 
 `nonVoid ty` returns True when either:
 1. `ty` has at least one InhabitationCandidate for which both its term and type
-   constraints are satifiable.
+   constraints are satifiable, and `nonVoid` returns `True` for all of the
+   strict argument types in that InhabitationCandidate.
 2. We're unsure if it's inhabited by a terminating value.
 
 `nonVoid ty` returns False when `ty` is definitely uninhabited by anything
@@ -1433,12 +1479,19 @@ determine whether a strict type is inhabitable by a terminating value or not.
 * `nonVoid (Int :~: Bool)` returns False. Although it has an
   InhabitationCandidate (by way of Refl), its type constraint (Int ~ Bool) is
   not satisfiable.
+* Given the following definition of `MyVoid`:
+
+    data MyVoid = MkMyVoid !Void
 
-Observe that the definition of `nonVoid ty` does not say whether `ty`'s
-InhabitationCandidate must itself have `nonVoid` return True for all its own
-strict argument types. This is a deliberate choice, because trying to take
-these into account in a naïve way can lead to infinite loops. Consider the
-following example:
+  `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.
+
+* Performance considerations
+
+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:
 
   data Abyss = MkAbyss !Abyss
 
@@ -1453,13 +1506,53 @@ There is only one InhabitationCandidate for Abyss—MkAbyss—and both its term
 and type constraints are satisfiable, so we'd need to check if `nonVoid Abyss`
 returns False... and now we've entered an infinite loop!
 
-To avoid this sort of conundrum, `nonVoid ty` doesn't call `nonVoid` on any of
-the strict argument types of `ty`'s InhabitationCandidates. This means
-that `nonVoid` is incomplete. For instance, GHC will warn that
-stareIntoTheAbyss is non-exhaustive, even though it actually is. Properly
-detecting that stareIntoTheAbyss is non-exhaustive would require a much more
-sophisticated implementation for `nonVoid`, however, so for now we simply
-implement the current, more straightforward approach.
+To avoid this sort of conundrum, `nonVoid` uses a simple test to detect the
+presence of recursive types (through `checkRecTc`), and if recursion is
+detected, we bail out and conservatively assume that the type is inhabited by
+some terminating value. This avoids infinite loops at the expense of making
+the coverage checker incomplete with respect to functions like
+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
+
+So this limitation is somewhat understandable.
+
+Note that even with this recursion detection, there is still a possibility that
+`nonVoid` can run in exponential time. Consider the following data type:
+
+  data T = MkT !T !T !T
+
+If we call `nonVoid` on each of its fields, that will require us to once again
+check if `MkT` is inhabitable in each of those three fields, which in turn will
+require us to check if `MkT` is inhabitable again... As you can see, the
+branching factor adds up quickly, and if the recursion depth limit is, say,
+100, then `nonVoid T` will effectively take forever.
+
+To mitigate this, we check the branching factor every time we are about to call
+`nonVoid` on a list of strict argument types. If the branching factor exceeds 1
+(i.e., if there is potential for exponential runtime), then we limit the
+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.
+
+Another microoptimization applies to data types like this one:
+
+  data S a = ![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
+intuition formal, we say that a type is definitely inhabitable (DI) if:
+
+  * It has at least one constructor C such that:
+    1. C has no equality constraints (since they might be unsatisfiable)
+    2. C has no strict argument types (since they might be uninhabitable)
+
+It's relatively cheap to cheap if a type is DI, so before we call `nonVoid`
+on a list of strict argument types, we filter out all of the DI ones.
 -}
 
 instance Outputable InhabitationCandidate where