Strange unification error ... maybe bug ?

[nicolabotta]

The program

> import Data.Vect
> import Data.Fin

> %default total

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

> lookup : (x : t) -> (xs : Vect n t) -> Elem x xs -> Fin n
> lookup {n = Z}   x  Nil prf               = absurd prf
> lookup {n = S m} x (x :: xs)   Here       = FZ
> lookup {n = S m} x (x' :: xs) (There prf) = FS (lookup x xs prf)

> indexLookupLemma : (x : alpha) -> 
>                    (xs : Vect n alpha) ->
>                    (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 : (k : Fin n) ->
>                    (xs : Vect n t) ->
>                    (prf : Elem (index k xs) xs) ->
>                    lookup (index k xs) xs prf = k
> lookupIndexLemma  k      Nil       prf        = absurd k
> lookupIndexLemma  FZ    (x :: xs)  Here       = ?kika
> lookupIndexLemma (FS k) (x :: xs) (There prf) = 
>   let ih = lookupIndexLemma k xs prf in rewrite ih in Refl

fails to type check with the error message

- + Errors (1)
 `-- unification.lidr line 29 col 18:
     When elaborating left hand side of lookupIndexLemma:
     When elaborating argument prf to Main.lookupIndexLemma:
             Unifying xs and index FZ xs :: xs would lead to infinite value

Am I missing something obvious here ?

[edwinb]

This works in master (except that lookupIndexLemma has some missing cases, which may need manual proofs to show they're absurd)