Unsoundness with record typing
Functions on records can be given unsound types as in the following:
# let f = fun ({..} -> 'a) x -> x;;
val f : Record -> 'a = <fun>
# f {};;
- : 'a = { }
It seems that this 'a
cannot be instantiated:
# (f {}) + 1;;
Characters 1-5:
This expression should have type:
!float | { .. } | Int
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
Atom & 'a
However, here it becomes unsound:
# f (f {});;
- : Empty = { }
Typing of field removal is also unsound:
# let g = fun ({a=Int;b=Bool;..}&'a -> {b=Bool;..}&'a) x -> x\a;;
val g : { a=Int b=Bool .. } & 'a -> { b=Bool .. } & 'a = <fun>
# g {a=2;b=`true};;
- : { a=2 b=`true } = { b=true }
# (g {a=2;b=`true}).a;;
- : 2 = true
# (g {a=2;b=`true}).b;;
- : `true = true
# (g {a=2;b=`true}).a + 2;;
File "runtime/value.ml", line 873, characters 9-15: Assertion failed