Skip to content

Commit

Permalink
Fixed a stupid and hard-to-find bug about flattening effect types, wh…
Browse files Browse the repository at this point in the history
…ich eventually restores the compatibility with polymorphic operations
  • Loading branch information
thwfhk committed Sep 19, 2023
1 parent 366aaaf commit 0d3c5b9
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 6 deletions.
7 changes: 4 additions & 3 deletions core/typeSugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1688,7 +1688,8 @@ let bind_effects context r = {context with effect_row = Types.flatten_r

let lookup_effect context name =
match context.effect_row with
| Types.Row (fields, _, _) -> begin match Utility.StringMap.find_opt name fields with
| Types.Row (fields, _, _) ->
begin match Utility.StringMap.find_opt name fields with
| Some (Types.Present t) -> Some t
| _ -> None
end
Expand Down Expand Up @@ -4779,7 +4780,6 @@ and type_binding : context -> binding -> binding * context * Usage.t =
| None ->
context, make_ft lin pats effects return_type, []
| Some ft ->
(* Debug.print ("t: " ^ Types.string_of_datatype ft); *)
(* make sure the annotation has the right shape *)
let shape = make_ft lin pats effects return_type in
let quantifiers, ft_mono = TypeUtils.split_quantified_type ft in
Expand All @@ -4802,7 +4802,8 @@ and type_binding : context -> binding -> binding * context * Usage.t =
let fold_in_envs = List.fold_left (fun env pat' -> env ++ (pattern_env pat')) in
let context_body = List.fold_left fold_in_envs context_body pats in

let new_body_context = {context_body with effect_row = effects;
(* the effects are flattened and a new cont_lin is generated before type checking the body *)
let new_body_context = {context_body with effect_row = Types.flatten_row effects;
cont_lin = LinCont.getnew () } in
let body = type_check new_body_context body in

Expand Down
2 changes: 0 additions & 2 deletions tests/cfl_old_handlers.tests
Original file line number Diff line number Diff line change
Expand Up @@ -391,13 +391,11 @@ Operation polymorphism (2)
sig catch : (() {Fail:forall a.a |e}~> b) {Fail{_} |e}~> Maybe(b) fun catch(m) { handle(m()) { case <Fail => k> : (forall a. () => a) -> Nothing case x -> Just(x) } } sig f : () {Fail:forall a.a}~> Int fun f () { if (do Fail) 42 else do Fail } catch (f)
stdout : Nothing : Maybe (Int)
args : --enable-handlers
ignore : not compatible with polymorphic operations

Operation polymorphism (3)
sig h : (() {Switch:forall a,b. (a,b) => (b,a) |e}~> c) {Switch{_} |e}~> c fun h(m) { handle(m()) { case <Switch(x,y) => k> : (forall a,b. (a,b) => (b,a)) -> k ((y,x)) } } sig f : () {Switch:forall a,b. (a,b) => (b,a)}~> Int fun f () { var (d,u) = do Switch(2,4) ; 10*d+u } h(f)
stdout : 42 : Int
args : --enable-handlers
ignore : not compatible with polymorphic operations

Generalise (1)
gen0(fun(m)() { handle(m()) { case <Foo => k> -> 42 case x -> x } }(fun(){42}))
Expand Down
1 change: 0 additions & 1 deletion tests/cfl_typecheck_examples.tests
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,6 @@ Typecheck example file examples/handlers/monadic_reflection.links
examples/handlers/monadic_reflection.links
filemode : true
args : --set=effect_sugar=true --set=effect_sugar_policy=final_arrow
ignore : not compatible with polymorphic operations

Typecheck example file examples/handlers/nim.links
examples/handlers/nim.links
Expand Down

0 comments on commit 0d3c5b9

Please sign in to comment.