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)
read image description
ALT
1
1
3
Conversation
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
Looks similar to the ‘forced patterns’ feature was working on for Aya?
For this specific issue, you might need to help Idris along by matching on the implicit `n` parameter. This might let you remove the redundant case. twitter.com/OwoTizusa/stat
This Tweet is unavailable.
2
2
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
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 :(
read image description
ALT
1
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).
read image description
ALT
1
1
the definition (a : Nat) -> Vect (S n) a -> a works but is much uglier than the workaround I had before imo
1
1
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
bind it yourself
1
2
Ahh yeah, what I said here: twitter.com/brendanzab/sta
Think the trick is knowing that Idris _generalises_ this:
last : Vect (S n) a -> a
to this:
last : {0 n : Nat} -> Vect (S n) a -> a
where as we really want:
last : {n : Nat} -> Vect (S n) a -> a
Quote Tweet
Replying to @brendanzab @zornsllama and @OwoTizusa
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).