Correct bug with invalid "Unbound module" when typing recursive functions

[samsa1]

Currently when typing the following code :

module type T = sig type t end

let rec f (x : (module T with type t = int)) =
       let (module LocalModule) = x in (3 : LocalModule.t)

OCaml fails with the error message :

Line 4, characters 44-55: 
4 |        let (module LocalModule) = x in (3 : LocalModule.t)
                                                ^^^^^^^^^^^
Error: Unbound module "LocalModule"
|}]

The culprit in the type approximation that is done when typing recursive functions. We never look inside the patterns, resulting in a smaller environment than the real when the code contains first class modules.

This patch modifies slightly approx_type to accept unknown modules.

[samsa1]

Same problem occur with the following example :

type t = C : 'a -> t
let rec f x = let C (type a) v = x in (v : a)

I'll modify this patch to be less restrictive and also accept the example just above

[Octachron]

Note that is is suspended upon #13806 merging.

[gasche]

#13806 has been merged, can we un-suspend this one?

[samsa1]

This PR is not the right way to go for fixing this issue.

The following example is rejected by type approximation and this PR does not fix this issue. A more correct way to go might be to re-use the mechanism for typing recursive modules (ie : adding modules to the environment without knowing their signatures).

module type T = sig type t = int end
module M = struct type t = float end

let rec f (x : (module T)) =
  let (module M) = x in
  (1 : M.t)

Line 6, characters 2-11:
6 |   (1 : M.t)
      ^^^^^^^^^
Error: This expression has type "int" but an expression was expected of type
         "M/2.t" = "float"
       Line 5, characters 14-15:
         Definition of module "M"
       Line 2, characters 0-36:
         Definition of module "M/2"

[johnyob]

This PR is not the right way to go for fixing this issue.

Agreed :) I'm also working with type_approx to try fix #14253, and I'm slightly hijacking this thread to discuss: 'what do we want type_approx to do?'

In my view, the two examples in this PR should not be handled by type_approx. The first example is well-typed as written, but is very close to a scope escape and becomes ill-typed under small modifications e.g.

module type T = sig type t val v : t end

let rec f (x : (module T)) =
       let (module LocalModule) = x in (LocalModule.v : LocalModule.t)

should be ill-typed.

The second example is ill-typed due to a scope escape:

type t = C : 'a -> t

let rec f x = let C (type a) (v : a) = x in (v : a)

Here a escapes its scope.

What invariants do we want type_approx G e to satisfy? At the moment, it's not clear. For example, considering @samsa1's example:

module type T = sig type t = int end
module M = struct type t = float end

let rec f (x : (module T)) =
  let (module M) = x in
  (1 : M.t)

The current approximation yields (module T) -> M.t. But this can never be the type of f. In that sense, this is not really an approximation, since it cannot be refined into the actual type of f.

A reasonable contract would be: if type_approx G e returns t, then G |- e : theta(t) for some refinement theta.

Finally, I'm not convinced we should be approximating expansive expressions at all (let, match, try, if, sequencing). Some of these approximations are fragile e.g.match/if approximations are sensitive to branch ordering. Perhaps we should only approximate non-expansive expressions (e.g. functions, tuples, etc), where the notion of approximation is better behaved?

[samsa1]

Another broken example of type_approx :

type (_, _) eq = Refl : ('a, 'a) eq

let f (type a) =
    let rec g (x : a) (Refl : (a, int) eq) : int = (x : a) in
    ()

Error: This expression has type a but an expression was expected of type int

(the example without rec is accepted)

The reason this example fails is that type approx is allowed to go under GADTs pattern matching. It just doesn't happen in practice because people tend to bind (type a) on the same function as the GADT, thus preventing such cases from happening.

[johnyob]

The reason this example fails is that type approx is allowed to go under GADTs pattern matching. It just doesn't happen in practice because people tend to bind (type a) on the same function as the GADT, thus preventing such cases from happening.

While (type a) prevents this from happening, my attempts to fix #14253 would permit us to go under (type a).

For me, the problem with this example is the combination of the GADT with the behaviour that type_approx continues approximating under a type annotation e.g. int annotation on function here is an 'outer' annotation and a is an inner annotation, if we stopped at int, then we would succeed.