Throw exception in rec-fix

[liyishuai]

Installed versions

• coq 8.8.2
• coq-ext-lib 0.10.1
• coq-itree 1.0.0

Description

I'm trying to translate one exception to another:

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

Parameter err : Set.
Variant error := Error_Err : err -> error.

Definition wrap {E} `{exceptE error -< E} :
  itree (exceptE err) unit -> itree E unit :=
  rec-fix wrap_rec m :=
    match m.(observe) with
    | RetF tt => Ret tt
    | TauF m' => wrap_rec m'
    | VisF (Throw e) _ =>
      (* throw (Error_Err e) *)
      (* Ret tt *)
      ret tt
    end.

If I substitute ret tt with any commented line above:

Error:
In environment
E : Type -> Type
H : exceptE error -< E
The term "rec-fix ..." has type "itree (fun _ : Type => exceptE err void) unit -> itree ?E unit" while it is expected to have type
 "itree (exceptE err) unit -> itree E unit" (cannot unify "itree (exceptE err) unit" and
"itree (fun _ : Type => exceptE err void) unit").

Notice that Ret tt is not what I want, but yet another case that failed compilation.

[Lysxia]

One workaround is to add some type annotations:

   match m.(observe) return itree (_ +' E) _ with

or

   throw (Error_Err e) : itree (_ +' E) _

I don't see an obvious fix to avoid that at the moment.