As a bit of an aside, there’s a good reason for not providing structural subtyping of first-class modules: their run-time representation (effectively a record of values) depends on the *order* in which the values appear in the module type. For example:

```
(* test_order.ml *)
module type A_then_B = sig val a : int val b : int end
module type B_then_A = sig val b : int val a : int end
module X = struct let a = 1000 let b = 2000 end
let x = (module X : A_then_B)
let x' = (module X : B_then_A)
```

```
$ ocamlc -dlambda test_order.ml
(setglobal Test_order!
(let
(T/88 =
(module-defn(T/88) Test_order test_order.ml(3):110-157
(let (a/86 =[int] 1000 b/87 =[int] 2000) (makeblock 0 a/86 b/87)))
x'/94 = (makeblock 0 (field 1 T/88) (field 0 T/88)))
(makeblock 0 T/88 T/88 x'/94)))
```

Our `Test_order`

module gets compiled down to a block with three fields: `T`

, `x`

and `x'`

. We see that `x`

is represented as exactly `T`

(with no computation at runtime), but evaluating `x'`

requires making a *new* heap block in which the fields have been swapped. (Something similar happens when running under `ocamlopt`

, but with a bit more noise.)

In your example, the runtime implementation of `f'`

depends on the order of fields in `B`

:

```
-f' = (function m : int (apply g (makeblock 0 (field 0 m))))
+f'_reversed = (function m : int (apply g (makeblock 0 (field 1 m)))))
```

Thus, `f'`

can’t in general be implemented as exactly `g`

(and the inference to check whether it can would require some notion of row polymorphism, and not just plain structural subtyping). The type-checker thus requires going via the module language (as @kantian describes), with the corresponding run-time operations that this implies.