No such variable {n1}?

[Dominic Mulligan]

Hi,

I'm trying to typecheck the following function on Vects (an analogue
of the existing function on lists in the Prelude):

last : Vect a (S n) -> a
last (x::xs) =
case xs of
[] => x
y::ys => last (y::ys)

This seems OK to me, but Idris is producing the error:

MoreVect.idr:26:No such variable {n1}

on typechecking it. Is this a bug, or something else?

Cheers,
Dom

[Alexander Njemz]

Hi,

On Thu, Feb 16, 2012 at 7:50 PM, Dominic Mulligan
<dominic.p...@googlemail.com> wrote:
> Hi,
>
> I'm trying to typecheck the following function on Vects (an analogue
> of the existing function on lists in the Prelude):
>
> last : Vect a (S n) -> a
> last (x::xs) =
>  case xs of
>    []    => x
>    y::ys => last (y::ys)
>

this:

last : Vect a (S n) -> a

last {n=S k} (x::xs) =
case k of
O => x
_ => last xs

works. But I don't think it really answers your question.

Cheers,

Alexander

[Edwin Brady]

Hi Dom,
The problem with using case here is that case will only work on simple types - or more precisely, each branch has to have the same type and each pattern has to have the same type. The variable it can't find is (I think) because it hasn't generated the right type for the auxiliary function to do the case analysis (there's an implicit argument missing). Obviously this error message should be improved...

One way to fix this might be to use top level matching instead.

last : Vect a (S n) -> a

last (x :: []) = x
last (x :: y :: ys) = last (y :: ys)

It's probably possible to make the case construct a bit more flexible in this sort of situation. At the minute it's just not clever enough to generate the right type for the auxiliary function.

Edwin.

[Dominic Mulligan]

Ah OK, that makes sense. Top level matching does work here.

Thanks,
Dom.