Issue in apply that makes it not monotone
When intersecting an arrow type whose dnf contain several conjunctions, if this intersection makes one of the conjunctions empty, it will not be simplified in the DNF.
Then, using the operator apply on this arrow type will consider the positive part of this empty conjunction and thus it will not yield the expected type but a larger one.
This can be reproduced with the following code:
module CD = Cduce_types
let cup t1 t2 = CD.Types.cup t1 t2
let cap t1 t2 = CD.Types.cap t1 t2
let diff = CD.Types.diff
let cons = CD.Types.cons
let mk_arrow = CD.Types.arrow
let true_typ = CD.Builtin_defs.true_type
let false_typ = CD.Builtin_defs.false_type
let bool_typ = cup true_typ false_typ
let int_typ = CD.Types.Int.any
let any = CD.Types.any
let empty = CD.Types.empty
let any_node = cons any
let empty_node = cons empty
let subtype = CD.Types.subtype
let pp_typ = CD.Types.Print.print_noname
let apply t args =
let t = CD.Types.Arrow.get t in
CD.Types.Arrow.apply t args
let arrow_any = CD.Types.Function.any
let domain t =
if subtype t arrow_any then
let t = CD.Types.Arrow.get t in
CD.Types.Arrow.domain t
else empty
let _ =
let simple_arrow = mk_arrow (cons int_typ) (cons int_typ) in
let test = simple_arrow in
let test = cup test (mk_arrow (cons bool_typ) any_node) in
let test = diff test (mk_arrow any_node any_node) in
let test = cap test (mk_arrow (cons (diff any bool_typ)) any_node) in
Format.printf "%a@." pp_typ test ;
Format.printf "Subtype of %a ? %b@." pp_typ simple_arrow (subtype test simple_arrow) ;
Format.printf "But when we apply an Int to it: %a@." pp_typ (apply test (domain simple_arrow)) ;
It has been tested on the branches dune-switch and polymorphic.