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

Correctly refresh the type of the variables of t in a Forget(e,t) expression to

avoid a clash with variables in e.
parent f0ab9a87
......@@ -1211,7 +1211,7 @@ let rec type_check env e constr precise =
and type_check' loc env ed constr precise = match ed with
| Forget (e,t) ->
let t = Types.descr t in
let t = Types.Subst.freshen (Types.descr t) in
let te = type_check env e Types.any true in
let delta = Var.Set.cup (Types.all_vars t) in
if Type_tallying.is_squaresubtype delta te t then
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