GitLab

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