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!)