Commit 8ff33414 authored by Kim Nguyễn's avatar Kim Nguyễn

Properly check constraints on monomprhic variable during constraint generation:

when a constraint 'a < t or t < 'a with 'a being monomorphic occurs during constraint generation, we check whether
it holds for all 'a, that is we use plain subtyping.
(It generalizes the fact that 'a < Any or Empty < 'a hold for monomorphic variables, but also accounts for constraints such as 'a < 'a | t and so on).
parent 148cae0c
......@@ -3156,19 +3156,27 @@ module Tallying = struct
type sl = sigma list
let singleton delta = function
|Pos (v,s) ->
if Var.Set.mem v delta then
(*if equal s any || equal (var v) s then *)S.singleton M.empty
(*else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v))) *)
else
S.singleton (M.singleton v (empty,s))
|Neg (s,v) ->
if Var.Set.mem v delta then
(*if equal s any || equal (var v) s then *)S.singleton M.empty
(*else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v))) *)
let singleton delta c =
let constr, do_check, t1, t2 =
match c with
|Pos (v,s) ->
if Var.Set.mem v delta then M.empty, true, (var v), s
else M.singleton v (empty,s), false, empty, empty
|Neg (s,v) ->
if Var.Set.mem v delta then M.empty, true, s, (var v)
else M.singleton v (s,any), false, empty, empty
in
let res = S.singleton constr in
if do_check then
if subtype t1 t2 then res
else
S.singleton (M.singleton v (s,any))
raise (UnSatConstr
(Format.sprintf
"Constraint (%s) <= (%s) on monomorphic variable failed"
(Utils.string_of_formatter Print.pp_type t1)
(Utils.string_of_formatter Print.pp_type t2)
))
else res
let pp_s = S.pp
let pp_m = M.pp
......
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