How can I have a monad as a parameter to a typeclass?

Stream: lean4

[Alex Zani]

I would like to make a typeclass instances of which specify a type and a monad. For instance, the example below.

class Sign [Monad m] (α : Type) where
  sign : α → m Bool

def sign_option (i : Int) : Option Bool :=
  if i == 0
  then none
  else
    if i > 0
    then some true
    else some false

instance : Sign Int where
  sign := sign_option

I get the following error:

typeclass instance problem is stuck, it is often due to metavariables
  Monad ?m.240

[Matt Diamond]

if you give Lean a hint then it works:

instance : Sign (m := Option) Int where
  sign := sign_option

there might be a better way but at least that will get you past the error

[Alex Zani]

Thanks. I guess I should get used to hinting.

An alternative I found was to define the class to take the monad as an explicit parameter:

class Sign (m : Type → Type) [Monad m] (α : Type) where
  sign : α → m Bool

Then you don't need to know the name of the metavariable

instance : Sign Option Int where
  sign := sign_option

I'd be curious if more experienced users have developed best practices around implicit + hinting vs explicit.

[Edward van de Meent]

honestly i'm not too sure what other monad you might want to use here?
(also maybe consider something like mathlib's docs#SignType)

[Alex Zani]

This was just an MRE I concocted to demonstrate the issue I was having. I'm mostly just exploring the language to get comfortable with it.

[Kyle Miller]

I think usually classes about monads tend to be explicitly parameterized by the monad

docs#LawfulMonad, docs#MonadLift, docs#MonadControl, etc.

[Kyle Miller]

The core issue in your original example is that Sign Int is fully elaborated before going into the where clause. That means it's not able to pick up on what m is from sign_option, and instead it fails to synthesize [Monad m] for the unknown m.