fixed bugs that caused compiler to hang forever when there is %tcinline pragma

CHANGELOG_NEXT.md

@@ -52,6 +52,13 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun`
   and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`.
 
+* Add new pragma `%tcinline_fuel` to avoid totality checker from infinitely
+  inlining recursive function with `%tcinline` and hang forever. The default
+  value of `%tcinline_fuel` is `1000`.
+
+* Fix a bug in `CallGraph.idr` that caused compiler to hang forever even when
+  `%tcinline_fuel` is set.
+
 * LHS of `with`-applications are parsed as `PWithApp` instead of `PApp`. As a
   consequence, `IWithApp` appears in `TTImp` values in elaborator scripts instead
   of `IApp`, as it should have been.

CONTRIBUTORS

@@ -14,6 +14,7 @@ Andre Kuhlenschmidt
 André Videla
 Andy Lok
 Anthony Lodi
+Anton Ping
 Arnaud Bailly
 Brian Wignall
 Bryn Keller

docs/source/reference/pragmas.rst

@@ -151,6 +151,12 @@ the ``minimal`` directive priority over the ``compact`` directive if both are pr
 
 See the section for each codegen under :ref:`sect-execs` for available directives.
 
+``%tcinline_fuel``
+--------------------
+
+Set fuel to avoid totality checker from infinitely inlining recursive function with `%tcinline` and hang
+forever. The default value is 1000. (See ``%tcinline`` pragma)
+
 Pragmas on declarations
 =======================
 

src/Core/Context.idr

@@ -2262,6 +2262,17 @@ setNFThreshold : {auto c : Ref Ctxt Defs} ->
                  Nat -> Core ()
 setNFThreshold max = update Ctxt { options->elabDirectives->nfThreshold := max }
 
+export
+setTcInlineFuel : {auto c : Ref Ctxt Defs} ->
+                Nat -> Core ()
+setTcInlineFuel fuel = update Ctxt { options->elabDirectives->tcInlineFuel := fuel }
+
+export
+getTcInlineFuel : {auto c : Ref Ctxt Defs} -> Core Nat
+getTcInlineFuel = do
+    defs <- get Ctxt
+    pure (tcInlineFuel (elabDirectives (options defs)))
+
 export
 setSearchTimeout : {auto c : Ref Ctxt Defs} ->
                    Integer -> Core ()

src/Core/Options.idr

@@ -132,6 +132,7 @@ record ElabDirectives where
   -- in addition to postfix (dot) projections
   -- default: yes
   prefixRecordProjections : Bool
+  tcInlineFuel : Nat
 
 public export
 record Session where
@@ -230,7 +231,7 @@ defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True 1000
 
 -- FIXME: This turns out not to be reliably portable, since different systems
 -- may have tools with the same name but different required arugments. We

src/Core/Termination/CallGraph.idr

@@ -70,23 +70,24 @@ mutual
   findSC : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            Defs -> Env Term vars -> Guardedness ->
+           List Name -> -- to avoid caseblock looping
            List (Term vars) -> -- LHS args
            Term vars -> -- RHS
            Core (List SCCall)
-  findSC {vars} defs env g pats (Bind fc n b sc)
+  findSC {vars} defs env g cbs pats (Bind fc n b sc)
        = pure $
             !(findSCbinder b) ++
-            !(findSC defs (b :: env) g (map weaken pats) sc)
+            !(findSC defs (b :: env) g cbs (map weaken pats) sc)
     where
       findSCbinder : Binder (Term vars) -> Core (List SCCall)
-      findSCbinder (Let _ c val ty) = findSC defs env g pats val
+      findSCbinder (Let _ c val ty) = findSC defs env g cbs pats val
       findSCbinder b = pure [] -- only types, no need to look
   -- If we're Guarded and find a Delay, continue with the argument as InDelay
-  findSC defs env Guarded pats (TDelay _ _ _ tm)
-      = findSC defs env InDelay pats tm
-  findSC defs env g pats (TDelay _ _ _ tm)
-      = findSC defs env g pats tm
-  findSC defs env g pats tm
+  findSC defs env Guarded cbs pats (TDelay _ _ _ tm)
+      = findSC defs env InDelay cbs pats tm
+  findSC defs env g cbs pats (TDelay _ _ _ tm)
+      = findSC defs env g cbs pats tm
+  findSC defs env g cbs pats tm
       = do let (fn, args) = getFnArgs tm
            -- if it's a 'case' or 'if' just go straight into the arguments
            Nothing <- handleCase fn args
@@ -97,42 +98,42 @@ mutual
     -- If we're InDelay and find a constructor (or a function call which is
     -- guaranteed to return a constructor; AllGuarded set), continue as InDelay
              (InDelay, Ref fc (DataCon _ _) cn, args) =>
-                 do scs <- traverse (findSC defs env InDelay pats) args
+                 do scs <- traverse (findSC defs env InDelay cbs pats) args
                     pure (concat scs)
              -- If we're InDelay otherwise, just check the arguments, the
              -- function call is okay
              (InDelay, _, args) =>
-                 do scs <- traverse (findSC defs env Unguarded pats) args
+                 do scs <- traverse (findSC defs env Unguarded cbs pats) args
                     pure (concat scs)
              (Guarded, Ref fc (DataCon _ _) cn, args) =>
                  do Just ty <- lookupTyExact cn (gamma defs)
                          | Nothing => do
                               log "totality" 50 $ "Lookup failed"
-                              findSCcall defs env Guarded pats fc cn args
-                    findSCcall defs env Guarded pats fc cn args
+                              findSCcall defs env Guarded cbs pats fc cn args
+                    findSCcall defs env Guarded cbs pats fc cn args
              (Toplevel, Ref fc (DataCon _ _) cn, args) =>
                  do Just ty <- lookupTyExact cn (gamma defs)
                          | Nothing => do
                               log "totality" 50 $ "Lookup failed"
-                              findSCcall defs env Guarded pats fc cn args
-                    findSCcall defs env Guarded pats fc cn args
+                              findSCcall defs env Guarded cbs pats fc cn args
+                    findSCcall defs env Guarded cbs pats fc cn args
              (_, Ref fc Func fn, args) =>
                  do logC "totality" 50 $
                        pure $ "Looking up type of " ++ show !(toFullNames fn)
                     Just ty <- lookupTyExact fn (gamma defs)
                          | Nothing => do
                               log "totality" 50 $ "Lookup failed"
-                              findSCcall defs env Unguarded pats fc fn args
-                    findSCcall defs env Unguarded pats fc fn args
+                              findSCcall defs env Unguarded cbs pats fc fn args
+                    findSCcall defs env Unguarded cbs pats fc fn args
              (_, f, args) =>
-                 do scs <- traverse (findSC defs env Unguarded pats) args
+                 do scs <- traverse (findSC defs env Unguarded cbs pats) args
                     pure (concat scs)
       where
         handleCase : Term vars -> List (Term vars) -> Core (Maybe (List SCCall))
         handleCase (Ref fc nt n) args
             = do n' <- toFullNames n
                  if caseFn n'
-                    then Just <$> findSCcall defs env g pats fc n args
+                    then Just <$> findSCcall defs env g cbs pats fc n args
                     else pure Nothing
         handleCase _ _ = pure Nothing
 
@@ -303,23 +304,24 @@ mutual
   findSCcall : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                Defs -> Env Term vars -> Guardedness ->
+               List Name -> -- to avoid caseblock looping
                List (Term vars) ->
                FC -> Name -> List (Term vars) ->
                Core (List SCCall)
-  findSCcall defs env g pats fc fn_in args
+  findSCcall defs env g cbs pats fc fn_in args
         -- Under 'assert_total' we assume that all calls are fine, so leave
         -- the size change list empty
       = do fn <- getFullName fn_in
            logC "totality.termination.sizechange" 10 $ do pure $ "Looking under " ++ show !(toFullNames fn)
            aSmaller <- resolved (gamma defs) (NS builtinNS (UN $ Basic "assert_smaller"))
            cond [(fn == NS builtinNS (UN $ Basic "assert_total"), pure [])
-                ,(caseFn fn,
-                    do scs1 <- traverse (findSC defs env g pats) args
+                ,(caseFn fn && not (elem fn cbs),
+                    do scs1 <- traverse (findSC defs env g (fn::cbs) pats) args
                        mps  <- getCasePats defs fn pats args
-                       scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps
+                       scs2 <- traverse (findInCase defs g (fn::cbs)) $ fromMaybe [] mps
                        pure (concat (scs1 ++ scs2)))
               ]
-              (do scs <- traverse (findSC defs env g pats) args
+              (do scs <- traverse (findSC defs env g cbs pats) args
                   pure ([MkSCCall fn
                            (fromListList
                                 (map (mkChange defs aSmaller pats) args))
@@ -328,23 +330,25 @@ mutual
 
   findInCase : {auto c : Ref Ctxt Defs} ->
                Defs -> Guardedness ->
+               List Name -> -- to avoid caseblock looping
                (vs ** (Env Term vs, List (Term vs), Term vs)) ->
                Core (List SCCall)
-  findInCase defs g (_ ** (env, pats, tm))
+  findInCase defs g cbs (_ ** (env, pats, tm))
      = do logC "totality" 10 $
                    do ps <- traverse toFullNames pats
                       pure ("Looking in case args " ++ show ps)
           logTermNF "totality" 10 "        =" env tm
           rhs <- normaliseOpts tcOnly defs env tm
-          findSC defs env g pats (delazy defs rhs)
+          findSC defs env g cbs pats (delazy defs rhs)
 
 findCalls : {auto c : Ref Ctxt Defs} ->
             Defs -> (vars ** (Env Term vars, Term vars, Term vars)) ->
             Core (List SCCall)
 findCalls defs (_ ** (env, lhs, rhs_in))
    = do let pargs = getArgs (delazy defs lhs)
-        rhs <- normaliseOpts tcOnly defs env rhs_in
-        findSC defs env Toplevel pargs (delazy defs rhs)
+        fuel <- getTcInlineFuel
+        rhs <- normaliseOpts ({fuel := Just fuel} tcOnly) defs env rhs_in
+        findSC defs env Toplevel [] pargs (delazy defs rhs)
 
 getSC : {auto c : Ref Ctxt Defs} ->
         Defs -> Def -> Core (List SCCall)

src/Idris/Desugar.idr

@@ -1332,6 +1332,7 @@ mutual
              Overloadable n => pure [IPragma fc [] (\nest, env => setNameFlag fc n Overloadable)]
              Extension e => pure [IPragma fc [] (\nest, env => setExtension e)]
              DefaultTotality tot => pure [IPragma fc [] (\_, _ => setDefaultTotalityOption tot)]
+             TcInlineFuel n => pure [IPragma fc [] (\nest, env => setTcInlineFuel n)]
   desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name]
 
   export

src/Idris/Parser.idr

@@ -1534,6 +1534,10 @@ directive fname indents
          tot <- totalityOpt fname
          atEnd indents
          pure (DefaultTotality tot)
+  <|> do decoratedPragma fname "tcinline_fuel"
+         fuel <- decorate fname Keyword $ intLit
+         atEnd indents
+         pure (TcInlineFuel (fromInteger fuel))
 
 fix : Rule Fixity
 fix

src/Idris/Syntax.idr

@@ -381,6 +381,7 @@ mutual
        AutoImplicitDepth : Nat -> Directive
        NFMetavarThreshold : Nat -> Directive
        SearchTimeout : Integer -> Directive
+       TcInlineFuel : Nat -> Directive
 
   public export
   PField : Type

tests/idris2/total/total025/Issue-2995.idr

@@ -0,0 +1,15 @@
+-- see https://github.com/idris-lang/Idris2/issues/2995
+
+%default total
+
+%tcinline
+zs : Stream Nat
+zs = Z :: zs
+
+%tcinline
+zs' : Stream Nat -> Stream Nat
+zs' xs = Z :: zs' xs
+
+%tcinline
+zs'' : Stream Nat -> Stream Nat
+zs'' = \xs => Z :: zs'' xs

tests/idris2/total/total025/expected

@@ -0,0 +1 @@
+1/1: Building Issue-2995 (Issue-2995.idr)

tests/idris2/total/total025/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue-2995.idr

tests/idris2/total/total026/Issue-2995.idr

@@ -0,0 +1,16 @@
+-- see https://github.com/idris-lang/Idris2/issues/2995
+
+%default total
+
+%tcinline
+incAll : Stream Nat -> Stream Nat
+incAll (x::xs) = S x :: incAll xs
+
+%tcinline
+incAll' : Stream Nat -> Stream Nat
+incAll' = \(x::xs) => S x :: incAll' xs
+
+%tcinline
+incAll'' : Stream Nat -> Stream Nat
+incAll'' = \ys => case ys of
+    (x :: xs) => S x :: incAll'' xs

tests/idris2/total/total026/expected

@@ -0,0 +1 @@
+1/1: Building Issue-2995 (Issue-2995.idr)

tests/idris2/total/total026/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue-2995.idr

tests/idris2/total/total027/TcInlineFuel.idr

@@ -0,0 +1,18 @@
+%default total
+
+%tcinline_fuel 42
+
+%tcinline
+f : Nat -> a -> a
+f Z x = x
+f (S k) x = f k x
+
+-- this will typecheck
+g1 : Nat -> Nat
+g1 Z = Z
+g1 (S k) = g1 (f 41 k)
+
+-- but this will not
+g2 : Nat -> Nat
+g2 Z = Z
+g2 (S k) = g2 (f 42 k)

tests/idris2/total/total027/expected

@@ -0,0 +1,11 @@
+1/1: Building TcInlineFuel (TcInlineFuel.idr)
+Error: g2 is not total, possibly not terminating due to recursive path Main.g2
+
+TcInlineFuel:16:1--16:16
+ 12 | g1 Z = Z
+ 13 | g1 (S k) = g1 (f 41 k)
+ 14 | 
+ 15 | -- but this will not
+ 16 | g2 : Nat -> Nat
+      ^^^^^^^^^^^^^^^
+

tests/idris2/total/total027/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check TcInlineFuel.idr