Typeclass inference and definition

Dear Coq community,

Edit: Turned out it is a bug, and one I had found in the past, but totally forgot about (oups). I created an issue on the GH bugtracker.

I am currently struggling with what I believe is a very strange behavior. I have implemented a monad typeclass hierarchy in coq-prelude.

This package provides the classical Monad typeclass, along with several canonical definitions such as an instance for option and a StateT monad.

Today, I wanted to try to play with coq-prelude by implementing a dead simple parser combinator library.

My first step was to define an alias for a Parser monad made of StateT and option.

Definition Parser (s a:  Type): Type :=
  StateT (string * s) option a.

I know this stack is a monad, as I can write something like that:

Definition t: StateT (string * unit) option unit :=
  pure tt >>= fun _ => pure tt.

Unfortunately, when it comes to using my Parser definition, Coq fails to find a monad instance.

Fail Definition t: Parser unit unit :=
  pure tt >>= fun _ => pure tt.
The command has indeed failed with message:
Unable to satisfy the following constraints:

?Monad : "Monad (Parser unit)"

Which means Coq does not try to unfold Parser.

I tried several options: Typeclasses Transparent Parser, Typeclasses eauto := 100, Hint Unfold Parser etc.

Does this means I am supposed to explicitely provides instances of my typeclasses for Parser (and any other type alias I will define)?

Thanks by advance for your help, I hope my post was clear.
(and thanks for the Coq devteam for setting up this forum!)

You might want to compare your approach with coq-haskell, which seems to have similar goals.