balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix in new typer: propagator for break_ctor was too permissive

Browse Source
This commit is contained in:
Suzanne Dupéron 2020-04-28 01:03:38 +01:00
parent cf492f03cb
commit 4587862da7
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/passes/8-typer-new/solver.ml
View File

@ -331,6 +331,9 @@ let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector =
with the same sort of constraint (constructor vs. constructor) with the same sort of constraint (constructor vs. constructor)
is symmetric *) is symmetric *)
let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).constructor in let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).constructor in
let other_cs = List.filter (fun (o : c_constructor_simpl) -> Var.equal c.tv o.tv) other_cs in
(* TODO double-check the conditions in the propagator, we had a
bug here because the selector was too permissive. *)
let cs_pairs = List.map (fun x -> { a_k_var = c ; a_k'_var' = x }) other_cs in let cs_pairs = List.map (fun x -> { a_k_var = c ; a_k'_var' = x }) other_cs in
WasSelected cs_pairs WasSelected cs_pairs
| SC_Alias _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *) | SC_Alias _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *)