Commit d58c722c authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: check soundness of polymorphic recursion

parent 77bea804
module Bad
use import ref.Ref
function comp ~'a 'a : ()
let test z =
let rec f x =
(* the argument of [g] shares the type vairable with [z], but we
don't know it yet, and specialize [g] as fully type polymorpic,
because of its explicit type signature. Since we do not compute
the fixed point during type inference, the type of [f] will be
erroneously over-generalized, the types of [x] and [z] won't be
unified, and we will have a type mismatch on [g x] when building
the expression. This is why recursive functions with explicit
signatures must either be polymorphic in a given type variable
or that type variable must appear explicitly in the context of
the recursive definition (here, in the type of [z]). *)
g x
with g (u : 'a) : unit =
comp u z
......@@ -245,6 +245,14 @@ let add_dvty tvs (argl,res) = res :: List.rev_append argl tvs
let tv_in_tvars tv tvs =
try List.iter (occur_check tv) tvs; false with Exit -> true
let free_user_vars tvs (argl,res) =
let rec add s = function
| Dvar { contents = Dval d } -> add s d
| Dvar { contents = Dtvs _ } -> s
| Duvar (tv,_) -> if tv_in_tvars tv tvs then s else Stv.add tv s
| Dits (_,dl,_) | Dts (_,dl) -> List.fold_left add s dl in
List.fold_left add (add Stv.empty res) argl
let specialize_scheme tvs (argl,res) =
let htvs = Htv.create 17 in
let hreg = Htv.create 17 in
......@@ -35,7 +35,11 @@ val ts_app: tysymbol -> dity list -> dity
val opaque_tvs: Stv.t -> dity -> Stv.t
val is_chainable: dvty -> bool (* non-bool * non-bool -> bool *)
val is_chainable: dvty -> bool
(* non-bool * non-bool -> bool *)
val free_user_vars: tvars -> dvty -> Stv.t
(* user type variables not bound in the context *)
exception DTypeMismatch of dity * dity
......@@ -277,6 +277,10 @@ let add_mono id dvty denv =
let locals = Mstr.add (None, dvty) denv.locals in
{ denv with locals = locals; tvars = add_dvty denv.tvars dvty }
let add_rec_poly id dvty tvs denv =
let locals = Mstr.add (Some tvs, dvty) denv.locals in
{ denv with locals = locals }
let add_rec_mono id dvty denv =
(* fix type variables but not regions *)
let tvars = add_dvty denv.tvars dvty in
......@@ -703,6 +707,7 @@ and de_desc denv loc = function
DEfor (id, efrom, dir, eto, inv, e1), e1.de_type
and dletrec ~top denv fdl =
let tvars = denv.tvars in
(* add all functions into the environment *)
let add_one denv (_,id,_,bl,tr) =
let _,argl,tyl = dbinders denv (pass_opacity tr bl) in
......@@ -710,23 +715,27 @@ and dletrec ~top denv fdl =
let dvty = tyl, match rpty with
| Some pty -> dity_of_pty denv pty
| None -> create_type_variable () in
let check (_,_,_,apty) = apty = None in
let denv = if rpty = None || List.exists check bl
then add_rec_mono id dvty denv
else add_poly id dvty denv in
denv, (argl, dvty) in
let check (_,_,_,apty) = apty <> None in
let denv, freetvs = if rpty <> None && List.for_all check bl
then add_rec_poly id dvty tvars denv, free_user_vars tvars dvty
else add_rec_mono id dvty denv, Stv.empty in
denv, (argl, dvty, freetvs) in
let denv, dvtyl = Lists.map_fold_left add_one denv fdl in
(* then type-check the bodies *)
let type_one (loc,id,gh,bl,tr) (argl,((tyl,tyv) as dvty)) =
let type_one (loc,id,gh,bl,tr) (argl,((tyl,tyv) as dvty),freetvs) =
let add denv (_,id,_,_) dity = match id with
| Some id -> add_var id dity denv
| None -> denv in
let denv = List.fold_left2 add denv bl tyl in
let id, gh = add_lemma_label ~top id gh in
let tr, (badl, res) = dtriple denv tr in
if badl <> [] then errorm ~loc
if badl <> [] then Loc.errorm ~loc
"The body of a recursive function must be a first-order value";
unify_loc unify loc tyv res;
let freenow = free_user_vars tvars dvty in
if not (Stv.subset freetvs freenow) then Loc.errorm ~loc
"This function is expected to be polymorphic in type variable %a"
Pretty.print_tv (Stv.choose (Stv.diff freetvs freenow));
id, gh, dvty, argl, tr in
List.map2 type_one fdl dvtyl
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