Commit bd583e85 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Refresh the type of function and argument (in that order) before tallying. This way,

when solving tallying constraints, the type of the result is defined in terms of the
variables in the argument, not the other way around.
parent 14a4dfe4
Pipeline #180 passed with stages
in 4 minutes and 13 seconds
......@@ -1332,6 +1332,8 @@ and type_check' loc env e constr precise =
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
let t1 = Types.Subst.refresh env.mono_vars t1 in
let t2 = Types.Subst.refresh env.mono_vars t2 in
match Types.Tallying.squareapply env.mono_vars t1 t2 with
| None -> raise_loc loc (Constraint (t2, dom))
| Some (_, res) -> res
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment