4. [16 points] In this problem, suppose we add record subtyping and function subtyping to ML. Because ML records are immutable (there is no way to assign to a field after a record is created), depth subtyping is sound for records. So assume record subtyping supports width, permutation, and depth, and that function subtyping supports contravariant arguments and covariant results. For each of the function calls below, check the box if and only if the function call should type-check assuming these variables have the types indicated:
(* assume these variables are bound to functions with the given types; they are used below *)
val f1 : { a:int, b : { c:int, d:int } } -> { a:int } = ...
val f2 : { a:int } -> { a:int, b : { c:int, d:int } } = ...
val f3 : { a:int, b : { c:int, d:int } } -> { a:int, b : { c:int, d:int } } = ...
val f4 : (({ a:int, b : { c:int} } -> { a:int }) * int) -> { a:int } = ...
val r1 : { a:int } = { a = 1 }
val r2 : { a:int, b : { c:int} } = { a=1, b = { c=2 } }
val r3 : { a:int, b : { c:int, d:int}, e:int } = { a=1, b = { c=2, d=3}, e=4 }
val r4 : { a:int, b : { c:int, d:int, e:int }} = { a=1, b = { c=2, d=3, e=4} }