How do I convince the totality checker in Idris that I'm not using a variable?

Question

I've been having trouble convincing the Idris totality checker that my function is total. Here's a simple example version of the problem I'm running into. Say we have a very simple expression type of the following form:

data SimpleType = Prop | Fn SimpleType SimpleType

data Expr : SimpleType -> Type where
  Var : String -> Expr type
  Lam : String -> Expr rng -> Expr (Fn dom rng)
  App : Expr (Fn dom rng) -> Expr dom -> Expr rng

I'd like to write the function

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b

which will require a DecEq instance for SimpleType but nothing too fancy. The problem is how to convince the type checker that the function is total. For instance, consider implementing sub as follows:

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub name repl (App l r) = App (substitute name repl l) (substitute name repl r)
sub _ _ expr = expr

(which is incorrect, but a fine place to start.) This yields the error:

Main.sub is possibly not total due to: repl

At first glance, it seems that perhaps Idris is having trouble verifying that l and r are structurally smaller than (App l r). Perhaps the following will work?

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub name repl expr@(App l r) = App
  (sub name repl (assert_smaller expr l))
  (sub name repl (assert_smaller expr r))
sub _ _ expr = expr

Nope!

Main.sub is possibly not total due to: repl

In fact, on further investigation, it is revealed that, while this program compiles:

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub _ _ expr = expr

This one does not!

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub _ repl expr = expr

And now I am at a loss as to how to convince Idris that, in this final example, repl really isn't going to interfere with totality. Anyone know how to make this work?

Answer 1

This turns out to be an error in the totality checker, where it thinks the 'repl' you're referring to on the left hand side is the one defined in the library for making simple interactive loops. It obviously isn't - it's just a mistake in the name lookup - and it's trivial to fix this.

This is fixed in the git master and will therefore be fixed in the next release. In the meantime, using a different name than 'repl' will work (I realise this is a bit annoying, but there you go...)