The simplest example of the problem (but not the only example I can exhibit) is: suppose I'm given a higher order function f : (a -> b) -> c. I'd like to prove that f = (\g => f (\x => g x)).
In my own reasoning, it should be pretty straightforward: just apply eta-equivalence twice (once inside, and then outside).
If I wanted to prove f = (\x => f x), a simple Refl would have sufficed: this led me to think that "Idris knows about eta-equivalence". But then again, the same solution didn't work for f = (\g => f (\x => g x)).
At that point, I tried using rewrite, but couldn't find a way to reference the g in (\g => f (\x => g x)):
lemma : {g : a -> b} -> g = (\x => g x)
lemma = Refl
theorem : {f : (a -> b) -> c} ->
f = (\g => f (\x => g x))
theorem = rewrite (lemma {g = _}) in Refl
But, of course, Idris can't figure out what _ should be, and neither do I.
This can be further reduced to the problem of proving (\g => f g) = (\g => f (\x => g x)), of course, because Idris knows equality is transitive and knows about eta-equivalence (at least when it's not "hidden" in lambda abstractions).
I'm starting to believe that what I'm experiencing is somehow happening because Idris doesn't know about extensionality: is there any other way of proving this (without tweaking the notion of equality I'm using, such as using setoids)?
I'm using Idris 1.3.2 from git.
You can postulate extensionality:
postulate
funext : {f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g
theorem : {f : (a -> b) -> c} -> f = (\g => f (\x => g x))
theorem = funext $ \g => Refl