Open Lysxia opened 9 months ago
In line 1068 of the Parser
-- for now add a divergence effect to named effects/resources when there are type variables...
-- this is too conservative though; we should generate the `ediv` constraint instead but
-- that is a TODO for now
And this is from Koka's core.kk
// The predicate `:ediv<x,a,e>` signifies that if the type `:a` contains a reference to effect constant `:x",
// then the effect `:e` must contain the divergent effect (`:div`). This constraint is generated
// for operations on first-class effects where code can diverge through operations.
pub type ediv :: (X,V,E) -> P
When I use a named handler, I get both
exn
anddiv
. I get why we needexn
, because names can escape their scope. But whydiv
?For concreteness, not minimal but kinda small example: