Totality checker too permissive ?

[nicolabotta]

The program

> import Data.Vect

> total
> Dec1 : {A : Type} -> (P : A -> Type) -> Type
> Dec1 {A} P = (a : A) -> Dec (P a) 

> total
> filter : {A : Type} ->
>          {P : A -> Type} ->
>          Dec1 P ->
>          Vect n A -> 
>          (m : Nat ** Vect m A)
> filter d1P Nil = (Z ** Nil)
> filter d1P (a :: as) with (filter d1P as)
>   | (_ ** tail) with (d1P a)
>     | (Yes p)     = (_ ** a :: tail)
>     | (No contra) = (_ ** tail)

> total
> filterLemma : {A : Type} ->
>               {P : A -> Type} ->
>               (d1P : Dec1 P) ->
>               (a : A) ->
>               (as : Vect n A) ->
>               Elem a as ->
>               (p : P a) ->
>               Elem a (getProof (filter d1P as))
> filterLemma d1P a Nil  Here       p impossible

type checks fine although |filterLemma| is obviously not total. Is this the expected behavior ? Is the totality checker too permissive ?

[edwinb]

The problem is that it has guessed which "Nil" is meant and picked the wrong one. This is similar to an issue I was discussing with @david-christiansen recently - when there's only impossible cases given, it doesn't disambiguate names properly.

(This is more a note to myself about how to go about fixing it at some point...)

[nicolabotta]

Thanks Edwin. I cannot claim I understand what is going on but avoiding |impossible| appears to help:

> filterLemma d1P a Nil  prf p = absurd prf -- impossible

gives

*totalityChecker> :total filterLemma
Main.filterLemma is not total as there are missing cases

as one would expect. For the time being, I am going to adopt this scheme and restrict the usage of |impossible| to instance declarations. Best, Nicola

[TimRichter]

Another, slightly shorter, example:

> descent : {P : Nat -> Type} -> 
>           ((x : Nat) -> P x -> (x' : Nat ** (x' `LT` x,P x'))) ->
>           ( y : Nat ** P y) -> Void
> descent {P} desc (Z ** pZ) with (desc Z pZ)
>     | (Z ** (LTESucc _, _)) impossible

Idris 0.11 accepts descent as total. Avoiding "impossible" doesn't
help here: this implementation

> descent {P} desc (Z ** pZ) with (desc Z pZ)
>     | (Z ** (p, _)) = absurd p

is also reported total.

Best,
Tim