Conversation

eleanor 🌻
@zornsllama
Does anyone know why Idris 2 can’t figure this out? I have to explicitly tell it that xs matches _::_, even though it knows xs can’t match Nil (because it’s in the wrong case) (This also happens with case..of)
last : Vect (S n) a -> a last (x :: Nil) = x last (_ :: xs) = last xs
1
3
eleanor 🌻
@zornsllama
The simplest answer is just “it isn’t that smart” but I’m wondering if there’s a more detailed answer explaining whys
2
2
eleanor 🌻
@zornsllama
For the record if I make it `last (_::xs@(_::_))` then Idris works it out just fine. I’ll try matching on the implicit parameter tomorrow!
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
eleanor 🌻
@zornsllama
so the top definition works, but if I try to match on the implicit parameter (last') Idris yells at me because `n` is only accessible at compile time :(
last : (n : Nat) -> Vect (S n) a -> a last Z (x::Nil) = x last (S n) (_::xs) = last n xs last' : Vect (S n) a -> a last' {n} xs = last n xs
1
eleanor 🌻
@zornsllama
Idris also doesn't like doing it directly, it says: Error: While processing left hand side of last. Can't match on S ?_ (Erased argument).
last : Vect (S n) a -> a last {n=Z} (x::Nil) = x last {n=S _} (_::xs) = last xs
1
1
Brendan Zabarauskas
@brendanzab
Ohhhh so idris erases implicit variables by default I think. Ie. you can't match on them if they are erased at runtime! I believe there is a way to make these usable at runtime though, lemme check.
2
1
Brendan Zabarauskas
@brendanzab
On I think it is just `{n : Nat} -> Vect (S n) a -> a` - it's the lowercase, auto-generalised variables it automatically sets to be 'erased' (ie. to a 0 multiplicity).
1
2
Brendan Zabarauskas
@brendanzab
Yeah agreed! Might be good feedback to give in the Idris discord (they have a channel about error messages), or on the issue tracker? Not sure how receptive they are though. I only know this stuff because I'm familiar with the approach… never actually used Idris 2 myself 😳
2