Throw exception in rec-fix
Closed this issue · 1 comments
liyishuai commented
Installed versions
coq
8.8.2coq-ext-lib
0.10.1coq-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 commented
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.