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

Check that type t does not contain polymorphic variables in

e : t or e :? t.
parent e8b84eb5
...@@ -2,7 +2,7 @@ open Cduce_loc ...@@ -2,7 +2,7 @@ open Cduce_loc
open Ast open Ast
open Ident open Ident
open Debug open Debug
let (=) (x:int) y = x = y let (=) (x:int) y = x = y
let (<=) (x:int) y = x <= y let (<=) (x:int) y = x <= y
let (<) (x:int) y = x < y let (<) (x:int) y = x < y
...@@ -1212,21 +1212,33 @@ let rec type_check env e constr precise = ...@@ -1212,21 +1212,33 @@ let rec type_check env e constr precise =
and type_check' loc env ed constr precise = match ed with and type_check' loc env ed constr precise = match ed with
| Forget (e,t) -> | Forget (e,t) ->
let t = Types.Subst.freshen env.delta (Types.descr t) in if Var.Set.subset Types.(all_vars (descr t)) env.delta then begin
let te = type_check env e Types.any true in let t = Types.Subst.freshen env.delta (Types.descr t) in
let delta = Var.Set.cup (Types.all_vars t) env.delta in let te = type_check env e Types.any true in
if Type_tallying.is_squaresubtype delta te t then let delta = Var.Set.cup (Types.all_vars t) env.delta in
(ed,verify loc t constr) if Type_tallying.is_squaresubtype delta te t then
(ed,verify loc t constr)
else
raise_loc loc (Constraint(t, te))
end
else else
raise_loc loc (Constraint(t, te)) error loc "Polymorphic type variables cannot occur in static type-checks"
| Subst (e,sl) -> | Subst (e,sl) ->
let t = type_check env e constr precise in let t = type_check env e constr precise in
(ed,verify loc t constr) (ed,verify loc t constr)
| Check (t0,e,t) -> | Check (t0,e,t) ->
let te = type_check env e Types.any true in if Var.Set.subset Types.(all_vars (descr t)) env.delta then begin
t0 := Types.cup !t0 te; let te = type_check env e Types.any true in
(ed,verify loc (Types.cap te (Types.descr t)) constr) t0 := Types.cup !t0 te;
let tres = Types.cap te (Types.descr t) in
if Types.is_empty tres then
warning loc "This dynamic type-check will always fail";
(ed, verify loc tres constr)
end
else
error loc "Polymorphic type variables cannot occur in dynamic type-checks"
| Abstraction a -> | Abstraction a ->
(* freshen type variables from the environment to avoid capture with (* freshen type variables from the environment to avoid capture with
...@@ -1298,7 +1310,7 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1298,7 +1310,7 @@ and type_check' loc env ed constr precise = match ed with
in in
let vars = Types.all_vars type_pat in let vars = Types.all_vars type_pat in
if not (Var.Set.subset vars env.delta) then if not (Var.Set.subset vars env.delta) then
error br.br_loc "Polymoprhic type variables cannot occur in patterns" error br.br_loc "Polymorphic type variables cannot occur in patterns"
) b.br_branches; ) b.br_branches;
let t = type_check env e b.br_accept true in let t = type_check env e b.br_accept true in
let pargs = pat_list_of_expr e in let pargs = pat_list_of_expr e in
......
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