Idris - derive extended interface instance

Question

Suppose I have a function f : Ord a => ... which requires a to have and Ord instance. I can access the Ord a instance using

f : Ord a => ...
f @{ord} ...

Since Eq a => Ord a, a needs to have also an Eq a instance. Is there a way to retrieve it directly from Ord a, instead of doing something like the following?

f : (Eq a, Ord a) => ...
f @{eq} @{ord} ...

Answer 1

It is possible using %implementation, doing something as follows:

eqFromOrd : Ord a => Eq a
eqFromOrd @{ord} = %implementation

Answer 2

I would use the solution by @marcosh, but here is another take on this showing we don't strictly need %implementation:

eqExplicit : Eq a => Eq a
eqExplicit @{eq} = eq

eqFromOrd : Ord a => Eq a
eqFromOrd = eqExplicit