Search code examples
interfaceidris

Idris - derive extended interface instance

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} ...
Solution

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

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