Limit function argument in interface

Question

What is the syntax for restricting a function argument in an interface that accepts a function? I tried:

interface Num a => Color (f : a -> Type) where
     defs...

But he says that Name a is not bound in interface...

Answer 1

There interfaceare two parameters in yours : aand f. But fshould be enough to choose implementation:

interface Num a => Color (a : Type) (f : a -> Type) | f where

fhere is called the defining parameter .

Here is a meaningless full example:

import Data.Fin

interface Num a => Color (a : Type) (f : a -> Type) | f where
  foo : (x : a) -> f (1 + x)

Color Nat Fin where
  foo _ = FZ

x : Fin 6
x = foo {f = Fin} 5