Skip to content

Commit

Permalink
fix bug in Env.commit
Browse files Browse the repository at this point in the history
When assigning a variable using Env.commit, the new variable was a fresh
variable and therefore we could end up pointing a non arrow variable to
it. This would break the invariant that through the DAG of the
substitution the flag can only increase.
  • Loading branch information
FardaleM committed Oct 7, 2024
1 parent f030eaa commit 993e160
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion lib/unification/Env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,13 @@ let commit e =
(fun v t1 t2 ->
match t1, t2 with
| None, None -> None
| Some t, None | None, Some [t] -> Some t
| Some t, None -> Some t
| None, Some [t] -> (
match t with
| Type.Var _ ->
stack := (Type.var (tyenv e) v, t) :: !stack; (* TODO: we will create a new variable because of this. We need to work to create less variables in general. *)
None
| _ -> Some t)
| None, Some l -> Some (Type.tuple (tyenv e) (Type.NSet.of_list l))
| Some t1, Some l ->
(* TODO: Should we do something more clever here? Like look for the repr or
Expand Down

0 comments on commit 993e160

Please sign in to comment.