In your "intuition" section (btw. there is a typo here, it should be (type s) (x : s t)), you seem to present GADT as directly related to the new (type s) construct. It's a bit surprising because it's difficult to know the difference between this and classic type variables. I suppose it is because only (type s) guarantee that the variable remains polymorphic, and you use that to ensure that branch-local unifications don't "escape" to the outer level ? Could you be a bit more explicit on this ?

It's also a bit difficult to know what's the big deal about "exhaustiveness checks". As I understand it, you remark that with GADTs some case cannot happen due to typing reasons, but the exhaustive check doesn't know about it. Could you be a bit more explicit about what the exhaustiveness checker does :

- is it exactly the same behavior as before, ignoring GADT specificities ? (ie. you haven't changed anything)

- if not, what have you changed and how can we try to predict its reaction to a given code ?

- what can we do when it doesn't detect an impossible case ? I suppose we can't a pattern clause for it, as the type checker would reject it.

I'm not sure I understand the example of the "Variance" section.

Why is the cast in that direction ? It seems to me that even if we could force t to be covariant, this cast (to a less general type) shouldn't work :

  # type +'a t = T of 'a;;

Again, you "Objects and variants" and "Propagation" subsections are a bit vague. Could you give example of code exhibiting possible problems ?

Finally, a few syntax trolls, in decreasing order of constructivity :

- is it a good idea to reproduce the "implicit quantification" of ordinary types ? It seems it could be particularly dangerous here.

  for example, changing

    type _ t = Id : 'a -> 'a t

  to 

    type 'a t = Id : 'a -> 'a t | Foo of 'a

  introduce, if I'm not mistaken, a semantic-changing variable captures.

  (I thought other dark corners of the type declarations already had this behavior, but right now I can't remember which ones)

- if I understand it correctly, (type a . a t -> a) is yet another syntax for type quantification. Why ? I thought (type a) was used to force generalization, but ('a . ...)-style annotation already force polymorphism (or don't they ?). Is it a semantic difference with ('a . 'a t -> 'a), other than its interaction with gadts ? Can we use (type a . a t -> a) in all places where we used ('a . 'a t -> 'a) before ?

- is there a rationale for choosing Coq-style variant syntax instead of just adding a blurb to the existing syntax, such as

    | IntLit of int : int t

  or

    | IntList of int return int t

  ?

Thanks.