Constrain type

Stream: new members

[Miguel Negrão]

In the type signature of a function, how can I restrict a type to any type which is an instance of a particular type class, such as a Monad ?

[Kevin Buzzard]

Ask for [Monad X]?

[Miguel Negrão]

This example is a bit silly, but how would I constrain m such that it must be a Monad ?

def A (m : Type → Type) (y : Type) : Type := m y

I don't quite get how to use the [ ] syntax you mention. Thanks !

[Miguel Negrão]

Ok, I think I got it !

def A (m : Type → Type) [Monad m] (y : Type) : Type := m y