Unexpected interaction between variance and GADTs

[vicuna]

Original bug ID: 5985
Reporter: @yallop
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2013-04-13T11:46:07Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Tags: patch
Related to: #6275 #7360
Child of: #5984 #5998
Monitored by: @lpw25 mcclurmc @glondu @dra27 @alainfrisch @diremy

Bug description

The following program

type _ t = T : 'a -> 'a s t

is accepted if s is covariant (e.g. type 'a s = 'a), contravariant (e.g. type 'a s = 'a -> unit) or invariant (e.g. type 'a s = 'a -> 'a), but rejected if s is "bivariant" (e.g. type 'a s = int):

# type 'a s = int;;
type 'a s = int
# type _ t = T : 'a -> 'a s t ;;
Characters 4-27:
  type _ t = T : 'a -> 'a s t ;;
      ^^^^^^^^^^^^^^^^^^^^^^^
Error: In this definition, a type variable has a variance that
       is not reflected by its occurrence in type parameters.

However, if s is abstracted then the program is accepted, even if s is instantiated with a bivariant constructor:

# include
  (functor (S : sig type 'a s end) ->
    struct
      include S
      type _ t = T : 'a -> 'a s t
    end)
    (struct type 'a s = int end)
;;
type 'a s = int
type _ t = T : 'a -> 'a s t
#

File attachments

• pr5985-2.diff
• pr5985.diff

[vicuna]

Comment author: @garrigue

Well-spotted.

This is actually a soundness problem, as you can see by adding the code:

let x = T 3;;
match x with T y -> y;;

[vicuna]

Comment author: @lpw25

Here is a similar example:

          OCaml version 4.00.1

  # type ('a, 'b) eq = Eq: ('a, 'a) eq;;
  type ('a, 'b) eq = Eq : ('a, 'a) eq
  # module M : sig type 'a s val se: (int s, string s) eq end = struct
      type 'a s = int
      let se = Eq
    end;;
        module M : sig type 'a s val se : (int s, string s) eq end
  # type _ t = T : 'a -> 'a M.s t;;
  type _ t = T : 'a -> 'a M.s t
  # let castT (type a) (type b) (x : a t) (e: (a, b) eq) =
      ((match e with Eq -> (x : b t)) : b t);;
    val castT : 'a t -> ('a, 'b) eq -> 'b t = <fun>
  # let st : string M.s t = castT (T 3) M.se;;

  Process ocaml-toplevel segmentation fault

[vicuna]

Comment author: @lpw25

And another:

          OCaml version 4.00.1

  # module rec A : sig type 'a s val cast : int s B.t -> string s B.t end = struct
     type 'a s = int
     let cast (x: int s B.t): string s B.t = x
    end and B : sig type _ t = T : 'a -> 'a A.s t end = struct
     type _ t = T : 'a -> 'a A.s t
    end;;
            module rec A : sig type 'a s val cast : int s B.t -> string s B.t end
  and B : sig type _ t = T : 'a -> 'a A.s t end
  # A.cast (B.T 3);;

  Process ocaml-toplevel segmentation fault

[vicuna]

Comment author: @lpw25

Here is an example that doesn't use GADTs;

          OCaml version 4.00.1

  # include
        (functor (S : sig type 'a s end) ->
          struct
            include S
            type 'a t = 'b * ('a -> unit) constraint 'a = 'b s
            let x = ((3, fun _ -> ()) : int s t)
          end)
          (struct type 'a s = int end)
      ;;
                  type 'a s = int
  type 'a t = 'b * ('a -> unit) constraint 'a = 'b s
  val x : int s t = (<poly>, <fun>)
  # match x with (s, _) -> s ^ "hello";;

  Process ocaml-toplevel segmentation fault

In fact this example doesn't use any "language extensions", and is present in at least 3.12.1

[vicuna]

Comment author: @gasche

I worked with these "bivariant" type variables in the work on variance for GADTs ( http://hal.inria.fr/hal-00772993/ ) -- we called this variance "irrelevance", but "bivariance" is rather nice. I feel guilty for not spotting these problems when I did this work, as that would have been a rather natural occasion to experiment with these edge cases. I guess I have too much faith in the type-checker :-)

Jacques, do you think you can fix those unification issues? (To innocent bystanders reading the bugtracker: bivariant types ('a t) have the distinct property that the equation (foo t = bar t) does not necessarily implies (foo = bar), while types of any other variance do.).

I think it would be rather elegant if we could have explicit support of both bivariance/irrelevance and invariance as first-class variances in the type signature language. The syntax currently only allows '+' and '-' annotations (and '=' is implicitly available), but I think most of the type-system would extend gracefully to bivariance/irrelevance. Having it explicitly could also help us reason about those corner cases, and avoid such issues in the future. There is the delicate question of syntax; we used an unicode blurb in our paper, but I daringly suggest '0' or '*'.

type *'a = ...
type 0'a = ...

(Is it time to reopen discussion on #5688? #5688 . I think we properly understand the soundness question now, but it's unclear how the extended criterion we have in our article would fare without extending the OCaml signature language for upward/backward-closed types. I think it would still be useful in most actual cases, but the limitations have made me slow at asking for work on the type-checker implementation.)

[vicuna]

Comment author: @lpw25

If we add annotations for bivariance and invariance I would suggest using existing prefix operator symbols, for example:

type ?'a t (* Bivariant *)

type !'a t (* Invariant *)

Note that some bivariant definitions are safe, for example

type 'a s = S

it is only bivariant type equations that cause problems. I wonder whether there are any uses of

type 'a s = int

that couldn't be replaced by

type 'a s = S of int

without too much effort.

[vicuna]

Comment author: @garrigue

As Leo found by himself, this problem is not directly related to GADTs: it is about having type variables that are not determined by type parameters.
It is not related to variance either :-)

Actually this bug is probably in OCaml from the very beginning.
I verified that the following code typechecks in version 2.00.

module F(T:sig type 'a t end) = struct
  class ['a] c x = object constraint 'a = 'b T.t val x' : 'b = x method x = x' end
end;;
module M = F(struct type 'a t = unit end);;
let o = new M.c 3;;
o#x;;
- : 'a = <poly>

In some way the introduction of variance helped, since we at least check that in the current environment at the point of definition this problem does not occur. In 2.00, the following was also accepted:

type 'a t = unit;;
class ['a] c x = object constraint 'a = 'b t val x' : 'b = x method x = x' end;;

I have attached a patch that fixes those problems by assuming that all abstract types, except those that come from a separate compilation unit, may end up being bivariant.
This is fine, but it is going to break some programs, mainly (only?) those using GADTs
As you can see in the diff file, omega07.ml had to be modified, to make type indices concrete.
For instance
type 'a succ
becomes
type 'a succ = Succ of 'a
This may feel kind of heavy.
On the other, this is also necessary to ensure that one can prove inequalities outside of the current, so maybe this is fine.

[vicuna]

Comment author: @garrigue

Extra notes:

1. As mentioned in my previous note, this is not directly related to variance, so that extra notations for bivariance and invariance do not help here. If you want to discuss that it would be better to open another PR.

2. I wouldn't qualify this as a "child of" 5984, but indeed another way to fix it would be to recomputed variance after each signature substitution, and detect problems at this point. However, this is a rather big change, and this would mean that signature substitution can fail. I'm waiting for feedback on 5984 before doing anything in that direction.

[vicuna]

Comment author: @gasche

I have attached a patch that fixes those problems by assuming that all abstract types, except those that come from a separate compilation unit, may end up being bivariant.

I'm not sure I understand, why is it correct to deduce (foo = bar) from (foo t = bar t) when t is defined in a separate compilation unit? Couldn't you have the exact same problem if the separate compilation unit exposed, for example, a value of type

('a t, 'b t) eq

?

This is fine, but it is going to break some programs, mainly (only?) those using GADTs [...]
For instance
type 'a succ
becomes
type 'a succ = Succ of 'a

[...] this is also necessary to ensure that one can prove inequalities outside of the current module, so maybe this is fine.

I have already personally adopted that style after #5853 ( #5853 ). I believe the only robust way to make sure two types are seen as incompatible is to define them as transparent incompatible definition. I have talked about this style in e.g. ( http://stackoverflow.com/questions/15721528/type-level-arithmetics-in-ocaml ), maybe that would merit a point of its own in the manual.

I'm fine with type-checking changes that require that style.

I'm not sure what is the best way to expose (in)equalities between the primitive types (which I believe is you main rationale for handling abstract types structure items separately from the rest). Short of other solutions, one might want to consider a new way to define generative abstract types,

new type 'a foo

Transparent type definitions are of two kinds, the generative ones that are guaranteed to be incompatible with all previous definitions, and the type synonyms that may be equal to previous datatypes. There is currently no way to expose the generativeness of an abstract type, and I think that's part of the problem here.

(This may also help (partially) solve #5361, "Syntax to specify that a custom type is never a float" #5361 )

[vicuna]

Comment author: @garrigue

I'm not sure I understand, why is it correct to deduce (foo = bar) from (foo t = bar t) when t is defined in a separate compilation unit? Couldn't you have the exact same problem if the separate compilation unit exposed, for example, a value of type

('a t, 'b t) eq

This is fine, because from (int t, bool t) eq you won't be able to deduce that int = bool (at least since my fix of last saturday, which was an independent problem).
Should still double check.

For the question of "unique" types I agree this would be nice to have a syntax.
We need a discussion somewhere.
Personally, I would prefer introducing a new syntactic category of "qualifiers", so that we
are not limited by keywords for everything. This would have many applications.

type "unique" t (* different from all other nominal types )
type "final" 'a t ( cannot be instantiated in a signature *)

On the other hand, we don't want to make things too complicated.

[vicuna]

Comment author: @garrigue

The first patch had a stupid bug (didn't expand types when checking variance) so that it didn't work with the original report :-(
Now fixed.
I suppose I'm going to commit this, but not in the 4.00 branch.

[vicuna]

Comment author: @lpw25

I'm not sure I understand, why is it correct to deduce (foo = bar) from (foo t = bar t) when t is defined in a separate compilation unit? Couldn't you have the exact same problem if the separate compilation unit exposed, for example, a value of type

('a t, 'b t) eq

This is fine, because from (int t, bool t) eq you won't be able to deduce that int = bool (at least since my fix of last saturday, which was an independent problem).

But you can still deduce that int t s = bool t s, which is what causes the problem. For example, your patch still allows the following two files:

  (* s.ml *)

  type ('a, 'b) eq = Eq: ('a, 'a) eq

  module M : sig type 'a s val se: (int s, string s) eq end = struct
    type 'a s = int
    let se = Eq
  end

  (* t.ml *)

  type _ t = T : 'a -> 'a S.M.s t

  let castT (type a) (type b) (x : a t) (e: (a, b) S.eq) =
    ((match e with S.Eq -> (x : b t)) : b t)

  let st : string S.M.s t = castT (T 3) S.M.se

  let _ = match st with T s -> s ^ "hello"

which seg fault:

  $ ocamlc s.ml t.ml
  $ ./a.out 
  Segmentation fault

[vicuna]

Comment author: @lpw25

The problem is that you cannot allow

sig type 'a t = int end :> sig type 'a t end

and assume that give "type 'a t"

'a t = 'b t => 'a = 'b

I can see two possible solutions to this problem:

1. Since "bivariance" is a conservative approximation for types like:

   type 'a t = int
   

   We could add more annotations and restrictions to variance. For example,
   if ?'a meant bivariance and !'a meant invariance, we could have:

    'a t = 'b t => 'a = 'b iff t is invariant, covariant or contravariant
   

   and

   sig type ?'a t end :> sig type 'a t end
   

   but not

   sig type ?'a t end :> sig type !'a t end
   

2. We could ban type definitions of the form:

   type 'a t = typexpr
   

   where typexpr does not use the type variable 'a. Note that definitions like

   type 'a t = T of int
   

   and

   type 'a t
   

   would still be fine.

[vicuna]

Comment author: @yallop

It'd be better to avoid prohibiting irrelevant/bivariant type synonyms, which are both useful and common -- see e.g. the various instantiations of the Symantics signature in "Finally Tagless, Partially Evaluated":

R.repr (p10), L.repr (p11), R.repr (p12) etc.
http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf

or Fold_map, Rw_mutex etc. in Core

https://github.com/janestreet/core_extended/blob/master/lib/fold_map.ml#L123
https://github.com/janestreet/core_extended/blob/master/lib/rw_mutex.ml#L13

Insisting that all irrelevant type constructs define datatypes would break lots of existing code and make various common idioms clunky to write and slow to run.

[vicuna]

Comment author: @garrigue

Right.
I've uploaded a correct version that only allows abstract type constructors from pervasives,
but the restriction is severe.

And the option to check the variance after substitution is not good either:

module F (X : sig type 'a s  val e : (int s, bool s) eq end) : sig end = struct
   type _ t = T : 'a -> 'a s t
   (* ... *)
end

is sufficient to obtain a contradiction inside the body of F, which is not
visible outside...

At this point I see indeed no easy solution, short of adding a "non-bivariant"
variance annotation. I.e. if a type is marked as non-bivariant in a signature,
it cannot be substituted (or subtyped) by a bivariant one. But this requires
changing existing code.

Surprising we completely overlooked that, while we were aware of the problem
with abstraction and injectivity...