# Type errors when intercepting effects
**URL:** https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491
**Category:** Ecosystem
**Tags:** effects
**Created:** [September 14, 2021, 2:28pm UTC](https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491 "2021-09-14T14:28:16Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@Cjen1](https://discuss.ocaml.org/u/Cjen1)
#### Post date: [September 14, 2021, 2:28pm UTC](https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491/1 "2021-09-14T14:28:16Z")
I’m experimenting with intercepting effects as in order to attach information to them, for example in order to prioritise certain fibres.
This as an idea seemingly does work, although there is many slightly weird type errors.
Throughout this I’m using the `State` example.
After much trial and error here is a working example.
```auto
effect Get : string
effect Priority : 'a eff * string -> 'a
let run f ~init =
let comp =
match f () with
| x -> (fun s -> x)
| effect (Priority (Get, p)) k -> (fun (s : string) -> print_endline p; continue k s s)
in comp init
let priority f ~p =
match f () with
| x -> x
| effect Get k -> let r = perform (Priority (Get, p)) in continue k r;;
let () =
run ~init:"1" @@
@@ fun () -> priority ~p:"p"
@@ print_endline (perform Get)
```
#### Q1. You need to constrain the type of `s` in run?
Unfortunately I don’t quite understand how some of the typing constraints passes around.
For example one persistent problem was that if `s` is not constrained to be a `string` its usage in the `continue k s s` fails to type check:
```auto
Error: This expression has type 'a but an expression was expected of type
effect
This instance of effect is ambiguous:
it would escape the scope of its equation
```
Why is it expecting the type to be an `effect`?
#### Q2. Polymorphic continuations cannot be passed via effects?
Additionally one change which would be nice to have would be to pass the continuation up through the priority effect, such that on the return the priority function would not need to be involved, ie:
```auto
effect Priority : 'a eff * ('a, 'b) continuation * string -> unit
let run f ~init =
let comp =
match f () with
| x -> (fun s -> x)
| effect (Priority (Get, k, _)) _ -> fun (s : string) -> continue k s s
in comp init
```
All variants I’ve tried to write using this unfortunately unify the `'b` with `effect`, but I am not sure why this is occurring, if I manually type `'b : int`, `run` type checks, but then it is not polymorphic.
#### Q3. Multiple effects leading to the same outcome?
Finally one nice simplification in these situations may be to have a match statement as follows:
```auto
let run f ~init =
let comp =
match f () with
| x -> (fun s -> s)
| effect (Priority (Get, k, _)) _
| effect Get k -> fun (s : string) -> continue k s s
```
However this fails with the error:
```auto
Effect patterns must be at the top level of a match case
```
Are these style of patterns just not possible using effects? I am fairly sure that it was possible to do similar patterns for exceptions, though I am probably mistaken.
### Conclusion
I’m expecting that the answer to the first two of these is that I need to better constrain the type of `Priority`, which I would love to hear how to do this 🙂 .
If there is some underlying issue with this approach that would also be great to hear!
Overall though the new effects system is very very cool, super versatile and expressive!
---
### Author:  [@lpw25](https://discuss.ocaml.org/u/lpw25)
#### Post date: [September 15, 2021, 5:37pm UTC](https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491/2 "2021-09-15T17:37:54Z")
Perhaps it would help to see an example without effects that is the same from a typing perspective:
```auto
type 'a ef = ..
type 'a ef +=
| Get : string ef
| Priority : 'a ef * string -> 'a ef
type 'b t = Eff : 'a ef * ('a -> 'b) -> 'b t;;
let run f ~init =
let comp =
match f () with
| Eff ((Priority (Get, p)), k) ->
(fun (s : string) -> print_endline p; k s s)
| _ -> assert false
in
comp init;;
```
If you remove the string type annotation you get:
```auto
5 | (fun s -> print_endline p; k s s)
^
Error: This expression has type 'a but an expression was expected of type
string
This instance of string is ambiguous:
it would escape the scope of its equation
```
---
### Author:  [@Cjen1](https://discuss.ocaml.org/u/Cjen1)
#### Post date: [September 16, 2021, 9:12am UTC](https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491/3 "2021-09-16T09:12:54Z")
Thanks for the reply!
So the removal of the string annotation would constrain the types of the continuations in an unbounded fashion?
What is confusing me is specifically, is that I would assume in the unconstrained situation that the following unifications would occur:
```auto
Get : string ef
Priority (Get, p) => Priority (_) : string ef
Eff(Priority(_), k) => Eff : string ef * (string -> 'b) -> 'b t
(fun s -> k s s) & k : string -> 'b => s : string & 'b = (string -> 'c)
```
Which should type check?
Is there something I’m missing in the modelling or calculation of these constraints?
---
### Author:  [@lpw25](https://discuss.ocaml.org/u/lpw25)
#### Post date: [September 16, 2021, 10:17am UTC](https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491/4 "2021-09-16T10:17:39Z")
The `Eff` constructor has an existential `'a`. So when you match on it you get some fresh abstract type, let’s call it `ext`. When you match on `Get` you learn that `ext` is equal to `string`. The function:
```auto
(fun s -> print_endline p; k s s)
```
then has two possible types:
```auto
string -> 'c
```
or
```auto
ext -> 'c
```
Those two types are equal whilst the equation from `Get` is in scope, but this function is being returned outside of that scope, which means that the types would become unequal and its not clear which one of them should be used. This is why the type-checker is complaining about ambiguity. If you add a type annotation then it is no longer ambiguous.
---
### Author:  [@Cjen1](https://discuss.ocaml.org/u/Cjen1)
#### Post date: [September 16, 2021, 10:54am UTC](https://discuss.ocaml.org/t/type-errors-when-intercepting-effects/8491/5 "2021-09-16T10:54:56Z")
Ah fascinating!
So this is why in the effects examples [here](https://github.com/ocaml-multicore/effects-examples/blob/master/state.ml) use concrete (?) types?
Regardless thanks for the help!