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

Change the Forget operator so that it uses the tallying and not the subtyping.

For instance :
  let f : Int -> Int = (fun ('a -> 'a) x -> x)
is now accepted.
parent f666e8bd
......@@ -1212,10 +1212,13 @@ 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
ignore (type_check env e t false);
(ed,verify loc t constr)
let t = Types.descr t in
let te = type_check env e Types.any true in
let delta = Var.Set.cup (Types.all_vars t) env.delta in
if Type_tallying.is_squaresubtype delta te t then
(ed,verify loc t constr)
else
raise_loc loc (Constraint(t, te))
| Subst (e,sl) ->
let t = type_check env e constr precise in
(ed,verify loc t constr)
......
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