Is it possible to help the compiler when "In this GADT definition, the variance of some parameter cannot be checked"?

Learning
1

The question is in the title. FWIW here’s what I’m trying to type:

type term_escape =
  [ `Error of bool * string
  | `Help of Cmdliner_manpage.format * string option ]

type +'a parser =
  Cmdliner_info.eval -> Cmdliner_cline.t ->
  ('a, [ `Parse of string | term_escape ]) result

type 'a cmd = Cmd
type 'a group = Group
type +'a t =
| Args : Cmdliner_info.args * 'a parser -> 'a t
| Cmd : 'a t * Cmdliner_info.term -> 'a cmd t
| Group : 'a t option * 'a cmd t list -> 'a group t

which fails with:

Error: In this GADT definition, the variance of some parameter
       cannot be checked
1 Like
2

I don’t think you can help the compiler here, because this is unsound in the general case. Here it might be sound (?) because cmd and group happen to be the unit type. But anything more complicated and it would become unsound.

This is because matching GADT values introduces type equalities. Suppose you have a function f (v:'a t) (x:'a) = .... Then you can invoke it with f (Cmd ... : strong t :> weak t) (x: weak), but the body of f will wrongly believe that x is of type strong, once v has been matched upon. So, any definition of your cmd type that would make it possible to distinguish the types weak and strong would crash your program. You cannot have any covariance here.

1 Like
3

I suspect this has already occurred to you, but if the goal is just to restrict the term structure then this can be done in a less elegant manner with an extra type parameter (and then, if needed, an existential wrapper to hide it):

type args = |
type cmd = |
type group = |

type (+'a, _) t_ =
| Args  : Cmdliner_info.args * 'a parser        -> ('a, args) t_
| Cmd   : ('a, _) t_ * Cmdliner_info.term       -> ('a, cmd) t_
| Group : ('a, _) t_ option * ('a, cmd) t_ list -> ('a, group) t_

type +'a t = E : ('a, _) t_ -> 'a t [@@ocaml.unboxed]

Regarding your original encoding, my understanding is that the type-checker has no notion of a type operator being “provably phantom” (co-injective?) in one of its parameters, as @silene suggests. So not enough information is retained about the typing of cmd (and group) to be precise about the variance of t when typing it.

1 Like
4

Thanks for your answers.

Unfortunately it’s a little bit more than that. I wanted to be able to provide an eval function that would only act on 'a cmd Term.t values. Your t_ type would do but I’m constrained by backward compatibility (so is that variance annotation in +a Cmdliner.Term.t, I wouldn’t mind dropping it but unfortunately it was added at some point).

1 Like
5

Not a solution but I just want to mention that in the end, in this particular example, it was simply better to keep Args and commands ( Cmd and Group) separate rather than try to be typesmart®.

1 Like
6

It seems to typecheck with the new injectivity annotation type !'a t, which helps a lot for this kind of GADT where constructors produce 'a something t:

type !'a t =
| Args : Cmdliner_info.args * 'a parser -> 'a t
| Cmd : 'a t * Cmdliner_info.term -> 'a cmd t
| Group : 'a t option * 'a cmd t list -> 'a group t
1 Like
7

But would that have been backward compatible with the existing +'a t ? I don’t have time to (likely re-) read the paper now :–)

8

No. Injectivity and variance are orthogonal concepts.
Moreover, like variance annotations, injectivity annotations are always inferred for concrete type declaration. Thus the annotation only really matters for abstract types (and some private row types).

3 Likes