Totality checker too strict ?

[nicolabotta]

The following code

> import Data.Vect
> import Data.Vect.Quantifiers
> import Data.Fin

> %default total

> instance Uninhabited (Elem {a} x Nil) where
>   uninhabited Here impossible                                                                                          
>   uninhabited (There p) impossible      

> lookup : {A : Type} -> 
>          (a : A) -> (as : Vect n A) -> Elem a as -> Fin n
> lookup a  Nil        prf        = absurd prf
> lookup a (a :: as)   Here       = FZ
> lookup a (a' :: as) (There prf) = FS (lookup a as prf)

> indexLookupLemma : {A : Type} -> 
>                    (x : A) -> (xs : Vect n A) -> (prf : Elem x xs) -> 
>                    index (lookup x xs prf) xs = x
> indexLookupLemma x  Nil        prf        = absurd prf
> indexLookupLemma x (x :: xs)   Here       = Refl
> indexLookupLemma x (x' :: xs) (There prf) = 
>   let ih = indexLookupLemma x xs prf in rewrite ih in Refl

> lookupIndexLemma : {A : Type} -> 
>                    (k : Fin n) -> (xs : Vect n A) -> (prf : Elem (index k xs) xs) ->
>                    lookup (index k xs) xs prf = k
> lookupIndexLemma  k      Nil       prf        = absurd prf
> lookupIndexLemma  FZ    (x :: xs)  Here       = Refl
> lookupIndexLemma (FS k) (x :: xs) (There prf) = 
>   let ih = lookupIndexLemma k xs prf in rewrite ih in Refl

type checks but lookupIndexLemma appears not to be total:

*VectProperties> :total lookupIndexLemma
VectProperties.lookupIndexLemma is not total as there are missing cases

I understand that "is not total as there are missing cases" judgements have to be read as "might not be total". Thus, this is not an issue in the same sense as #1917 is. But I tought of reporting it because, in the specific case, I would have expected that, if indexLookupLemma is checked to be total, so would lookupIndexLemma. Am I missing something obvious here ? Thanks, Nicola

[falsifian]

What about the case lookupIndexLemma FZ (x :: xs) (There prf) ?

[nicolabotta]

Good point but even adding a

> lookupIndexLemma  FZ    (x :: xs) (There prf) = ?lookupIndexLemma_meta1

case does not make lookupIndexLemma pass the totality check.

[edwinb]

According to :missing, you need to add the following:

> lookupIndexLemma  FZ    (x :: xs) (There prf) = ?foo
> lookupIndexLemma (FS _) (_ :: _)  Here        = ?bar

So I think this is behaving correctly.