Slow compilation times for type-level `Nat`

[joelberkeley]

Steps to Reproduce

data Bar : Nat -> Type where
  B : Unit -> Bar n

Bars : Type
Bars = (
      (Bar 4, Bar 120)
    , (Bar 120, Bar 84)
    , (Bar 84, Bar 2)
  )

bar : (a, b, c, d, e : Unit) -> Unit

foo : Bars -> Unit
foo ((B a, B b), (B c, B d), (B e, B f)) =  id $ bar a b c d e

Expected Behavior

Reasonable compilation times

Observed Behavior

time idris2 --build tinker.ipkg 
1/1: Building Main (src/Main.idr)
Now compiling the executable: tinker

real  2m3.780s
user  2m3.028s
sys   0m0.649s

Notes

I assume the problem is that Idris is manipulating large inductive Nats in a nested type, but I can't help but wonder if there's a principled way to avoid this in the compiler, since it compiles almost instantly if I parametrize over the Nat and only apply 120, 84 at a higher level.

Bars : (m, n : Nat) -> Type
Bars m n = (
      (Bar 4, Bar m)
    , (Bar m, Bar n)
    , (Bar n, Bar 2)
  )

foo : (m, n : Nat) -> Bars m n -> Unit
foo _ _ ((B a, B b), (B c, B d), (B e, B f)) =  id $ bar a b c d e

main : IO ()
main = do
  let _ = foo 120 84 ((B (), B ()), (B (), B ()), (B (), B ()))
  pure ()

[dunhamsteve]

The application of id is required to reproduce this issue. It appears to be exponential in the number of arguments to bar. The slowness is happening in totality checking. It happens when it is calculation the sizeChange of bar a b c d e. The Nat show up in the arguments of MkPair in that pattern.

The path that causes this issue is sizeCompareApp, which peels off one App and retries.

So here we look for bar a b c d e under the S constructor on the LHS: https://github.com/idris-lang/Idris2/blob/95333b3adc33decf1d0cc17e825c90f1afc36a42/src/Core/Termination/CallGraph.idr#L218-L223

When that fails, sizeCompareApp is called with s and t, and it peels off one App of s and retries: https://github.com/idris-lang/Idris2/blob/95333b3adc33decf1d0cc17e825c90f1afc36a42/src/Core/Termination/CallGraph.idr#L241-L242

So it checks bar a b c d e, bar a b c d, ... at the top. When it goes under sizeCompareConArgs for each of those, it checks both that term and each of its shorter versions, and so forth for each level of constructor on the LHS. Changing sizeCompareApp to strip off all of the App resolves the issue above.

--- a/src/Core/Termination/CallGraph.idr
+++ b/src/Core/Termination/CallGraph.idr
@@ -238,7 +238,7 @@ mutual
           Unknown => sizeCompareConArgs fuel s ts
           _ => pure True
 
-  sizeCompareApp fuel (App _ f _) t = sizeCompare fuel f t
+  sizeCompareApp fuel (App _ f _) t = let f = fst $ getFnArgs f in sizeCompare fuel f t
   sizeCompareApp _ _ t = pure Unknown
 
   sizeCompareAsserted : {auto defs : Defs} -> Nat -> Maybe (Term vars) -> Term vars -> Core SizeChange

(I'd also expect this to have a branching factor of 2, but it doesn't seem to be slow, even with bigger test cases.)

[spcfox]

hanging sizeCompareApp to strip off all of the App resolves the issue above.

Now size comparison can also work for partially applied functions:

%default total

data X : Type where
  A : Bool -> Nat -> X
  B : (f : Nat -> X) -> X

P : X -> Type
P (A {}) = ()
P (B f) = f = A True

foo : (x : X) -> P x -> X
foo (A b n)      _    = A b n
foo (B (A True)) Refl = foo (A True 0) () -- A True 0 < A True < B (A True)

With this change, the code above no longer works. However, I think it is rarely used, so it’s probably fine to drop it in exchange for better performance.

fst $ getFnArgs f

There’s also getFn, which might read a bit more nicely here: https://github.com/idris-lang/Idris2/blob/7928774fa79d6ede9ae817877693aab61d2b7749/src/Core/TT/Term.idr#L321-L323

[dunhamsteve]

Yeah, I kind of held off on that patch since it seemed kludgy. I was going to see if there was something more precise I could do to specifically target applications of bound variables or global names. And I was thinking it should be done before calling sizeCompareCon because it is recursing with that application before hitting the fallback case.

In your example it's not a function, but rather a data constructor being applied. I believe functions will never be applied on the LHS (and I had assumed constructors were not partially applied). So maybe strip off the the App only if the head is not a constructor, before calling sizeCompareCon / sizeCompareTyCon. WellFounded is an example of where this is relied on for an application for a bound pattern variable.

Something like:

diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr
index 4bfa8d7b0a..32f3276a14 100644
--- a/src/Core/Termination/CallGraph.idr
+++ b/src/Core/Termination/CallGraph.idr
@@ -191,10 +191,17 @@ mutual
       substMeta rhs _ _ _ = throw (InternalError ("Badly formed metavar solution \{show n}"))
 
   sizeCompare fuel s t
-     = if !(sizeCompareTyCon fuel s t) then pure Same
+     = let s = stripFunApp s in
+       if !(sizeCompareTyCon fuel s t) then pure Same
        else if !(sizeCompareCon fuel s t)
           then pure Smaller
           else knownOr (sizeCompareApp fuel s t) (pure $ if sizeEq s t then Same else Unknown)
+     where
+      stripFunApp : Term vars -> Term vars
+      stripFunApp tm = case getFn tm of
+        fn@(Ref _ Bound cn') => fn
+        fn@(Ref _ Func cn') => fn
+        _ => tm
 
   sizeCompareProdConArgs : {auto defs : Defs} -> Nat -> List (Term vars) -> List (Term vars) -> Core SizeChange
   sizeCompareProdConArgs _ [] [] = pure Same

[spcfox]

In your example it's not a function, but rather a data constructor being applied. I believe functions will never be applied on the LHS (and I had assumed constructors were not partially applied)

We can write essentially the same example using an ordinary function. You’re right that we can’t pattern-match on function applications or partially applied constructors directly, but in this case it’s effectively a dot-pattern (and it can be written explicitly; it behaves the same way).

%default total

data X : Type where
  B : (f : () -> X) -> X

A : Bool -> () -> X

P : X -> Type
P (B f) = f = A True

foo : (x : X) -> Maybe (P x) -> X
foo  x            Nothing    = x
foo (B (A True)) (Just Refl) = foo (A True ()) Nothing -- A True () < A True < B (A True)

I don’t think there’s any real code that relies on this kind of totality proof. Still, it’s worth keeping in mind that this change does make the termination checker slightly weaker.

[dunhamsteve]

@spcfox - this version handles your examples. Unless I'm missing something, the original code was stripping args on the RHS and falling back to sizeEq if the recursion said Unknown - essentially trying sizeEq on each smaller piece of the RHS, but going through sizeCompare to get there. Here, instead of recursing, I run the equivalent of sizeEq inside sizeCompareApp, but allow the bit on the RHS to be longer.

I believe this patch is equivalent to what happens today. But I have a question about the checkArgs (s :: ss) Nil = ... case here. I believe it comes out as Same with the current code, but should it be Smaller? Is foo bar baz always smaller than foo bar? I see you say A True () < A True - is it the case in general that when you apply a function, you get something smaller? (Is this because we're eliminating a lambda?)

diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr
index 4bfa8d7b0a..1ccfb0b6a6 100644
--- a/src/Core/Termination/CallGraph.idr
+++ b/src/Core/Termination/CallGraph.idr
@@ -194,7 +194,7 @@ mutual
      = if !(sizeCompareTyCon fuel s t) then pure Same
        else if !(sizeCompareCon fuel s t)
           then pure Smaller
-          else knownOr (sizeCompareApp fuel s t) (pure $ if sizeEq s t then Same else Unknown)
+          else sizeCompareApp fuel s t
 
   sizeCompareProdConArgs : {auto defs : Defs} -> Nat -> List (Term vars) -> List (Term vars) -> Core SizeChange
   sizeCompareProdConArgs _ [] [] = pure Same
@@ -238,8 +238,16 @@ mutual
           Unknown => sizeCompareConArgs fuel s ts
           _ => pure True
 
-  sizeCompareApp fuel (App _ f _) t = sizeCompare fuel f t
-  sizeCompareApp _ _ t = pure Unknown
+  sizeCompareApp fuel f t =
+    let (f,args) = getFnArgs f
+        (t,args') = getFnArgs t
+    in if sizeEq f t then checkArgs args args' else pure Unknown
+    where
+      checkArgs : List (Term vars) -> List (Term vars) -> Core SizeChange
+      checkArgs Nil Nil = pure Same
+      checkArgs (s :: ss) Nil = pure Same
+      checkArgs (s :: ss) (t :: ts) = if sizeEq s t then checkArgs ss ts else pure Unknown
+      checkArgs _ (t :: ts) = pure Unknown
 
   sizeCompareAsserted : {auto defs : Defs} -> Nat -> Maybe (Term vars) -> Term vars -> Core SizeChange
   sizeCompareAsserted fuel (Just s) t

[spcfox]

I should test a few hypotheses before writing a detailed response.

[dunhamsteve]

Thanks for taking the time. It looks like Abel's Foetus paper says "Be x, y variables, a a vector of terms (arguments of y), ρ a relation in {<, =} and y ρ x. It follows (y a) ρ x", which would suggest to me that Same is indeed appropriate here. What I don't yet understand is why Abel's rule is acceptable for termination checking. I don't have an argument for or against. I'll think through the examples more, because I'd really like to understand why that rule works.

I think the previous cases are covered here. Instead of hitting sizeCompare again, we do sizeEq for each prefix of the app, which would happen at the end of sizeCompare. The cases for checking each prefix under that data constructor should be handled when we go under the data constructor the first time around, with the full application, because sizeCompareApp will get hit at the non-constructor leaves. The other branches of sizeCompare, for dotted and as values, are handled in sizeEq. (Except for the case of as on the RHS of the definition, I don't think that's allowed, but sizeCompare has a case for it.)

[spcfox]

I have examined the problem in more detail and am ready to share my findings. I will split my response into two parts. In the first message, I comment on the changes proposed above. In the second, I describe an issue I have found in the current comparison algorithm that leads to a loss of performance.

---

But I have a question about the checkArgs (s :: ss) Nil = ... case here. I believe it comes out as Same with the current code, but should it be Smaller? Is foo bar baz always smaller than foo bar? I see you say A True () < A True - is it the case in general that when you apply a function, you get something smaller? (Is this because we're eliminating a lambda?)

Yes, I was mistaken in thinking that A True () < A True. As you pointed out, the foetus paper introduces the rule f R g => f x R g (1). It is not difficult to show that this is equivalent to f x <= f (2).

Proof

• (=>) Assume (1). Then f <= f, hence f x <= f.
• (<=) Assume f x <= f and f R g. Then f x R g.

My thoughts on this rule

Before I looked at the formulation in the paper, I assumed that there must be a strict relation here due to lambda elimination. This can break well-foundedness because of the appearance of an infinitely descending chain:

f <
f x <
f x y <
f x y z <
...

but I thought that number of arguments of a function is always limited. This is not true: id id id ... is a valid term. As a result, it would be possible to write a proof of false:

boom : ((a : Type) -> a -> a) -> Void
boom f = foo (f _ f)

This function should not type-check if we have universe levels, but there may be other counterexamples.

---

Returning to your latest patch. It looks similar to the current behaviour of the algorithm, but it does not implement rule (1) in full. To demonstrate this, we need such f and g that

• f is a function (has function type)
• f < g
• f is not a subterm of g

I think these conditions cannot be satisfied in foetus, but they can in Idris 2. This example no longer passes type checking:

%default total

data X : Type where
  A : Nat -> Bool -> X
  B : (f : Bool -> X) -> X

P : X -> Type
P (A {}) = ()
P (B f) = f = A 1

foo : (x : X) -> P x -> X
foo (A b n)   _    = A b n
foo (B (A 1)) Refl = foo (A 0 True) () -- A 0 True <= A 0 < A 1 < B (A 1)

Probably, you did not intend to allow comparisons of partially applied constructors (A 0 < A 1), but this is currently possible. I think this is consistent, due to the requirement that the number of arguments be the same.

[spcfox]

In the second, I describe an issue I have found in the current comparison algorithm that leads to a loss of performance.

To describe the discovered issue, let us consider how argument comparison works using a small example.

bar : Unit -> Unit

foo : Nat -> Unit
foo (S Z) = id $ bar ()
foo _ = ()

The algorithm performs comparisons in the following order:

• S Z with bar ()
  • Z with bar ()
    • Z with bar
  • S Z with bar
    • Z with bar

As can be seen, we reach the comparison of Z and bar via two different paths. As the depth of patterns grows and the number of arguments in the function on the RHS increases, the number of repeated comparisons grows exponentially. I tried cache the results of comparisons, and this version does not have problems with the example from issue. However, it hangs during self-build. https://github.com/spcfox/Idris2/compare/920afcc910cef6905ec4e66a0c1a9fef7d227efc..2b745959e31c321da76717ee08834e24149489aa

Another advantage of caching is that we can avoid repeatedly comparing identical terms if they occur multiple times within a single clause.

Perhaps, instead of caching the results, we could change the algorithm to reduce the number of repetitions.

I also noticed that knownOr evaluates its first argument twice. This does not affect the current example, but it may cause exponential growth. https://github.com/spcfox/Idris2/commit/920afcc910cef6905ec4e66a0c1a9fef7d227efc

[dunhamsteve]

Yeah, I believe that is the issue I'm trying to fix here, although I might not have explained it as well as you. By not recursing for each prefix, we avoid the issue.

[joelberkeley]

Just popping in to say thanks for working on this. Whenever it is fixed - and I don't mean at all to influence when that may be - it will no doubt help with what I'm doing.