Unsoundness involving non-injective types + gadts

[v-gb]

The following program is wrongly accepted by the typechecker, which can be turned into a segfault:

module F(X : sig type 'a t end) = struct
  type (_, _) gadt = T : ('a X.t, 'a) gadt
  
  (*
    let __ (type a b) (Equal : (a X.t, b X.t) Type.eq) =
      (Equal : (a, b) Type.eq)
   *)

  let equate_param2_based_on_param1 (type tt m1 m2)
        (T : (tt, m1) gadt) (T : (tt, m2) gadt) : (m1, m2) Type.eq =
     Equal
  ;;
end

module Z = F(struct type 'a t = unit end)

let () =
  let t1 = (Z.T : (unit, int) Z.gadt) in
  let t2 = (Z.T : (unit, string) Z.gadt) in
  let eq : (int, string) Type.eq = Z.equate_param2_based_on_param1 t1 t2 in
  let cast (type a b) (Equal : (a, b) Type.eq) (a : a) : b = a in
  print_string (cast eq 1)
;;

The problem is that the function equate_param2_based_on_param1 is considered well-typed by the typechecker, but in reality it's well-typed iff X.t is injective in 'a. By contrast, the commented-out injectivity function is correctly accepted iff X.t is injective in 'a.

(this came up while @mbarbin and I were thinking about the type safety in https://github.com/mbarbin/provider/).

[garrigue]

Thank you for at last finding a counter-example for why equations_generation = Forbidden is wrong.
It was based on the wrong assumption that, in a non-injective context, it was still fine to do normal unification, as long as it didn't fail. Thinking more about it, this was utterly broken, as it allows the kind of sharing of existentials that you are observing here.
The fix is a one-liner and does not seem to break the testsuite, but I wonder if some people were not using that unwittingly.

[v-gb]

Thanks for the quick fix !

[mbarbin]

Thank you for releasing 5.3.0~beta1. I'm trying it on a few examples related to that report there. I see this difference now:

annot53.ml:

type 'a ext = ..

module M (X : sig
    type 'a t
  end) =
struct
  type _ ext += T : 'a X.t ext

  let f (t2 : _ X.t ext) =
    match t2 with
    | T -> ()
    | _ -> ()
  ;;
end

$ .opam/5.2.0/bin/ocamlopt annot53.ml
[0]

$ .opam/5.3.0~beta1/bin/ocamlopt annot53.ml 
File "annot53.ml", line 11, characters 6-7:
11 |     | T -> ()
           ^
Error: This pattern matches values of type $0 X.t ext
       but a pattern was expected which matches values of type $1 X.t ext
       The type constructor $1 would escape its scope

Binding the variable is accepted by both typers:

  let f (type a) (t2 : a X.t ext) =
    match t2 with
    | T -> ()
    | _ -> ()
  ;;

If the type X.t doesn't come from a functor argument, the annotation is not needed by either typers:

annot2_53.ml:

type 'a ext = ..
type 'a x
type _ ext += T : 'a x ext

let f (t2 : _ x ext) =
  match t2 with
  | T -> ()
  | _ -> ()
;;

I just wanted to make sure this is all expected. This difference may come from other changes not related to this fix, I don't know. Thank you.

[Octachron]

This is a known change of behaviour (there is an example in #13583).

There is a proposal ( #13585) to make the typechecker works more to undo the change of behavior.

Nevertheless, I would generally advise to not mix unification variables with GADT pattern matching and always write let f (type a) (t2 : a X.t ext) = ....

[mbarbin]

Thank you for your answer and the links. In the examples I was looking into, I found the added annotations to make the intent more explicit. It looks like I am going to put your general advise to good use. Thanks a lot!