Na sequência,example1 é uma sintaxe padrão (conforme documentada), comEq a como uma restrição. Noexample2, Eu especificoEq a diretamente como o tipo de um parâmetro e o compilador o aceita. No entanto, não está claro o que posso especificar como um valor desse tipo. Para um tipo específicoa, por exemploNat, Presumo que faria sentido especificar de alguma forma uma implementação deEq Nat, a implementação padrão ou outra implementação nomeada.

%default total

example1: Eq a => (x : a) -> (y : a) -> Type
example1 {a} x y = ?example1_rhs

example1b: Eq a => (x : a) -> (y : a) -> Type
example1b {a} x y = x == y = True

example2: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type
example2 a eqa x y = ?example2_rhs

example2b: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type
example2b a eqa x y = x == y = True

eq_nat : Eq Nat
eq_nat = ?eq_nat_rhs

example_of_example2 : Type
example_of_example2 = example2 Nat eq_nat 3 3

Orifícios resultantes:

- + Main.example1_rhs [P]
 `--                  a : Type
                      x : a
                      y : a
             constraint : Eq a
     --------------------------
      Main.example1_rhs : Type

- + Main.example2_rhs [P]
 `--                  a : Type
                    eqa : Eq a
                      x : a
                      y : a
     -----------,---------------
      Main.example2_rhs : Type

- + Main.eq_nat_rhs [P]
 `-- Eq Nat

Tanto quanto eu posso dizer, eu realmente não posso usarexample2b como uma função, a menos que eu tenha alguma maneira de especificar um valor para o segundo parâmetro do tipoEq a.

Há situações em que seria realmente útil poder aplicar uma restrição de interface ao valor de um parâmetro (em oposição ao tipo de parâmetro), por isso espero que esse seja um recurso válido do Idris.