[ prelude ] Add some lacking %tcinlines

[buzden]

Without this you may get weird wrong totality checker errors when using simple functions like <$>, you can see an example in the added test.

[dunhamsteve]

It's interesting. This one is rejected:

%default total
data X : Type -> Type -> Type where
  B : b -> X a b
  R : X a b -> X b c -> X a c

Functor (X a) where
  map f (B x) = B (f x)
  map f (R x y) = R x (f <$> y)

It's not following the arguments:

 Leaf: Main.map -> [[Nothing, Nothing, Nothing, Nothing, Nothing] @[(Total:6:1--8:32, Main.map), (Total:6:1--8:32, Main.map)]]

But changing it to map f y works.

The diff of the logs (just looking at totality:99) is:

7,8d6
< LOG totality:50: Looking up type of Prelude.Interfaces.(<$>)
< LOG totality.termination.sizechange:10: Looking under Prelude.Interfaces.(<$>)
50c48
< LOG totality:5:   Mutually defined with:[Prelude.Interfaces.(<$>), Main.X, Main.B, Main.R, Main.Functor implementation at Total:6:1--8:32]
---
> LOG totality:5:   Mutually defined with:[Prelude.Interfaces.map, Main.X, Main.B, Main.R, Main.Functor implementation at Total:6:1--8:32]
56c54
< Leaf: Main.map -> [[Nothing, Nothing, Nothing, Nothing, Nothing] @[(Total:6:1--8:32, Main.map), (Total:6:1--8:32, Main.map)]]
---
> Leaf: Main.map -> [[Just (0, Same), Just (1, Same), Just (4, Smaller), Just (3, Same), Just (4, Smaller)] @[(Total:6:1--8:32, Main.map)]]
58,64d55
< Error: map is not total, possibly not terminating due to recursive path Main.map -> Main.map
< 
< Total:6:1--8:32
<  6 | Functor (X a) where
<  7 |   map f (B x) = B (f x)
<  8 |   map f (R x y) = R x (f <$> y)
< 

I added an extra log message, printing out work in checkTerminating and see:

< LOG totality.termination.calc:8: work: [(Main.map, (Main.map, [Nothing, Nothing, Just (4, Smaller), Nothing, Nothing] @[(Total:6:1--8:32, Main.map)]))]
---
> LOG totality.termination.calc:8: work: [(Main.map, (Main.map, [Just (0, Same), Just (1, Same), Just (4, Smaller), Just (3, Same), Just (4, Smaller)] @[(Total:6:1--8:32, Main.map)]))]

In one case it doesn't look like it's matching up the variables. I'm curious what's up, but might not have time to get to it today.

This is interesting though. I logged the sizeChange (it's hard to get at these nameless things from the REPL), and it looks like args are partitioned between the <$> call and the map call (in the case where we're going through <$>:

LOG totality.termination.calc:8: Adding function: Main.map [Prelude.Interfaces.(<$>): [Just (0, Same), Just (1, Same), Nothing, Nothing, Just (3, Same), Just (4, Smaller)], Main.map: [Nothing, Nothing, Just (4, Smaller), Nothing, Nothing]]

[dunhamsteve]

In case anyone is wondering why it is happening without the %tcinline - findSC sees:

Prelude.Interfaces.MkFunctor [Main.X, \{0 b : Type} => \{0 a : Type} => \(func : ?Main.{_:849}_[b[1], a[0]]) => \({arg:8747} : (Main.X a[1])) => (Main.map b[3] a[2] func[1] {arg:8747}[0])]

It finds is a call to Main.map with unknown arguments and flags the loop. With the <$> inlined, I think this is reduced out to a function call with known arguments.

[buzden]

It finds is a call to Main.map with unknown arguments and flags the loop

Look like the current behaviour is strange. I thought it just doesn't look inside unless it's %tcinlined, but it looks inside, but with strange consequences.

[dunhamsteve]

You probably know most of this already, but my understanding of the situation:

When it's checking totality, it goes through each of the functions on the graph and calculates the size changes. For example, if it is looking at map, then for each function map calls, it will emit a pair of the function name and a list of size changes of the arguments passed into the function. So it would say which argument of map each the argument to <$> came from (or Nothing) and whether it is smaller than value that it came from.

When it looks at map, the metas are already solved, and it does an additional normalization with a flag to inline anything marked %tcinline (in CallGraph.idr:findCalls).

Below I'm using a simplified test case (to remove some extra variables):

%default total
data X : Type -> Type where
  R : X b -> X c -> X c

Functor X where
  map f (R x y) = R x (f <$> y)

When processing Main.map, it doesn't look inside <$> (it would later process <$> separately and then analyze the graph for loops). The input to findCalls looks like (lhs and rhs_inin findCalls):

Main.map b' a f (R a {b} x y) =
  R b' {b} x ((<$>) b' a X "Main.Functor implementation at..." f y)

After normaization with tcinline turned on (lhs and rhs):

Main.map b' a f (R a {b} x y) =
  R b' {b} x ((<$>) b' a X (MkFunctor X \{0 b'' : Type} -> \{0 a' : Type} => \(func : _) => \(arg : X a') => Main.map b'' a' func arg) f y)

So the definition of the Functor X instance is marked %tcinline.

Now it goes into the mechanism at findSC, which drills down under the lambdas and sees a call to Main.map where none of the arguments line up with the left hand side, and flags it as not total.

If you tcline the <$>, the normalization substitutes it in and β-reduces the lambdas out, leaving a call to Main.map with the arguments from the LHS.

I considered tweaking findSC to not look under lambdas (or pi's) - and it passes all of the tests - but I constructed a case where it fails to mark a non-total function as total:

%default total
data Foo = MkFoo Nat (Nat -> Nat)

bar : Foo -> Nat
bar (MkFoo k f) = f (k + 2)

foo, baz : Nat -> Nat

baz k = bar (MkFoo k (\x => foo x))

foo (S k) = baz k
foo Z = Z

[dunhamsteve]

One further note: I think the implementation is marked TcInline only long enough to process the declaration. This is done near the bottom of elabImplementation in Idris/Elab/Implementation.idr. (It sets the flag, processes the decl and then clears it.)