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
This package provides the classical
Monad typeclass, along with several canonical definitions such as an instance for
option and a
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
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
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!)