Coq : mutually recursive definitions with [mrec] in InteractionTrees Library

Question

I'm studying this great library for Representing Recursive and Impure Programs in Coq

I am having problems with mutual recursion (very first example in documentation gives me an error) https://deepspec.github.io/InteractionTrees/5.0.0/ITree.Interp.Recursion.html#mrec

Inductive D : Type -> Type :=
| Even : nat -> D bool
| Odd : nat -> D bool.

Definition def : D ~> itree (D +' void1) := fun _ d =>
  match d with
  | Even n => match n with
              | O => ret true
              | S m => ITree.trigger (Odd m)
              end
  | Odd n => match n with
             | O => ret false
             | S m => ITree.trigger (Even m)
             end
end. 

This is the Error I am getting

Error:
In environment
T : Type
d : D T
n : nat
m : nat
The term "ITree.trigger (Odd m)" has type "itree (D +' void1) ?T0"
while it is expected to have type
 "itree (D +' void1) ?T@{T0:=T; T1:=bool}" (cannot satisfy constraint
"D bool" == "(D +' void1) ?T0").

what should I do to solve this problem?

By the way, I managed to use generic [rec] interface of the library's [Interp] module to define a single recursive function (no errors, no problems, and working example is given in tutorial (Introduction.v file)). But I couldn't find working example for more general [mrec] which allows multiple, mutually recursive definitions.

Thank you.

Answer 1

Replace ITree.trigger (not overloaded) with trigger (overloaded).

Compilable example:

From ExtLib Require Import Monad.
From ITree Require Import ITree.

Inductive D : Type -> Type :=
| Even : nat -> D bool
| Odd : nat -> D bool.

Definition def : D ~> itree (D +' void1) := fun _ d =>
  match d with
  | Even n => match n with
              | O => ret true
              | S m => trigger (Odd m)
              end
  | Odd n => match n with
             | O => ret false
             | S m => trigger (Even m)
             end
end.