Идрис - получить расширенный экземпляр интерфейса

Question

Предположим, у меня есть функция f : Ord a => ..., для которой требуется a и экземпляр Ord.Я могу получить доступ к экземпляру Ord a, используя

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

Поскольку Eq a => Ord a, a также должен иметь экземпляр Eq a.Есть ли способ получить его непосредственно из Ord a, вместо того, чтобы делать что-то вроде следующего?

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

Answer 1

Я бы использовал решение @marcosh, но вот еще один пример того, что нам не нужно %implementation:

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

eqFromOrd : Ord a => Eq a
eqFromOrd = eqExplicit

Answer 2

Можно использовать %implementation, выполнив что-то следующим образом:

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