Actually implement a terminating termination analysis

3 files changed, 38 insertions, 10 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index a6991d8508..be28831ca8 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -1002,9 +1002,21 @@ addVarNonVoidCt delta@MkDelta{ delta_tm_st = TmSt env } x =
     then pure delta
     else do
       vi  <- lift (initLookupVarInfo delta x)
-      vi' <- MaybeT (ensureInhabited delta vi)
+      vi' <- case splitTyConApp_maybe (vi_ty vi) of
+        Just (tc,_)
+          | lookupRecTc (delta_rec_tc delta) tc >= 1
+          , isAlgTyCon tc
+          -- not inhabited by inductive reasoning! If it was, some other
+          -- constructor would be inhabited.
+          -> mzero
+          | Just rec_tc' <- checkRecTc (delta_rec_tc delta) tc
+          -> MaybeT (ensureInhabited delta{ delta_rec_tc = rec_tc' } vi)
+        -- We ran out of fuel or it's not a TyCon app. Just assume it's
+        -- inhabited
+        _ -> pure vi
       pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') }
 
+
 {- Note [Strict argument type constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the ConVar case of clause processing, each conlike K traditionally
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index b2be6197d8..814b3913c4 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -456,7 +456,7 @@ data VarInfo
   -- ^ The type of the variable. Important for rejecting possible GADT
   -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).
 
-  , vi_pos :: [(PmAltCon, [Id])]
+  , vi_pos :: ![(PmAltCon, [Id])]
   -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
   -- at the same time (i.e. conjunctive).  We need a list because of nested
   -- pattern matches involving pattern synonym
@@ -514,12 +514,20 @@ initTyState = TySt emptyBag
 -- | Term and type constraints to accompany each value vector abstraction.
 -- For efficiency, we store the term oracle state instead of the term
 -- constraints.
-data Delta = MkDelta { delta_ty_st :: TyState    -- Type oracle; things like a~Int
-                     , delta_tm_st :: TmState }  -- Term oracle; things like x~Nothing
+data Delta
+  = MkDelta
+  { delta_ty_st  :: !TyState
+  -- ^ Type oracle; things like a~Int
+  , delta_tm_st  :: !TmState
+  -- ^ Term oracle; things like x~Nothing
+  , delta_rec_tc :: !RecTcChecker
+  -- ^ Only important for checking non-void constraints on recursive data types,
+  -- where we want to give up after a number of recursions.
+  }
 
 -- | An initial delta that is always satisfiable
 initDelta :: Delta
-initDelta = MkDelta initTyState initTmState
+initDelta = MkDelta initTyState initTmState (setRecTcMaxBound 1 initRecTc)
 
 instance Outputable Delta where
   ppr delta = vcat [
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 7af2bc0ad7..04fd026eda 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -127,7 +127,7 @@ module TyCon(
 
         -- * Recursion breaking
         RecTcChecker, initRecTc, defaultRecTcMaxBound,
-        setRecTcMaxBound, checkRecTc
+        setRecTcMaxBound, checkRecTc, lookupRecTc
 
 ) where
 
@@ -2713,6 +2713,7 @@ The function that manages all this is checkRecTc.
 data RecTcChecker = RC !Int (NameEnv Int)
   -- The upper bound, and the number of times
   -- we have encountered each TyCon
+  -- Invariant: if there's an entry for T in the NameEnv, then it is at least 1.
 
 -- | Initialise a 'RecTcChecker' with 'defaultRecTcMaxBound'.
 initRecTc :: RecTcChecker
@@ -2732,11 +2733,18 @@ setRecTcMaxBound new_bound (RC _old_bound rec_nts) = RC new_bound rec_nts
 checkRecTc :: RecTcChecker -> TyCon -> Maybe RecTcChecker
 -- Nothing      => Recursion detected
 -- Just rec_tcs => Keep going
-checkRecTc (RC bound rec_nts) tc
+checkRecTc rc@(RC bound rec_nts) tc
+  = case lookupRecTc rc tc of
+      n | n >= bound -> Nothing
+      n              -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
+  where
+    tc_name = tyConName tc
+
+lookupRecTc :: RecTcChecker -> TyCon -> Int
+lookupRecTc (RC _bound rec_nts) tc
   = case lookupNameEnv rec_nts tc_name of
-      Just n | n >= bound -> Nothing
-             | otherwise  -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
-      Nothing             -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
+      Just n  -> n
+      Nothing -> 0
   where
     tc_name = tyConName tc