Comment author: @sliquister

ident 0 is not nonexpansive, because it's a function application (regardless of the function) and so the regular value restriction kicks in. This only thing specific to gadts is that the compiler can check but won't infer that 'a exp is covariant in 'a, which would allow the relaxed value restriction to kick in.

Now, this example is obviously generalizable even if ident did arbitrary side effects, but the typer need to be spoonfed to understand it because the value restriction is restrictive (a smarter check would only prevent generalization of variables involved in the syntactically expansive parts):

let ident x = x
let ident0 = ident 0
# Int ident0;;

Comment author: @ivg

Yep, you're right, I don't know why I've decided that ident x is nonexpansive. Probably was too tired at the end of the day. Anyway, the typer behavior now looks valid, though non-intutive (because the type of int -> 'a t looks so covariant, that it is very surprising the the type checker doesn't see this).

Besides, while investigating this issue, I found a small caveat in the non-expansivness checker, that could be shown with the following interaction:

   type _ exp = Int : 'b -> 'a exp;;
   # let f ~y x = x + y;;
   val f : y:int -> int -> int = <fun>
   let g x ~y = x + y;;
   val g : int -> y:int -> int = <fun>
   # Int (f ~y:1);;
   - : '_a exp = Int <poly>
   # Int (g ~y:1);;
   - : 'a exp = Int <poly>

Basically, the order of parameters matter, as f is considered expansive, while g is non-expansive. The problem is in the following piece of code in the typecore.ml

  | Texp_apply(e, (_,None)::el) ->
      is_nonexpansive e && List.for_all is_nonexpansive_opt (List.map snd el)

That basically requires that an application must be abstracted on the first argument only. A more complete check would be

  | Texp_apply(e, el) ->
      is_nonexpansive e && 
      List.exists (fun (_,None) -> true | _ -> false) el &&
      List.for_all is_nonexpansive_opt (List.map snd el)

Comment author: @sliquister

f ~y:1 can do arbitrary side effects (depending on the definition of f), whereas g ~y:1 cannot (because the type of g says it takes ~x first) so that's why they are generalized differently.

If the typer change you suggest generalizes [Int (f ~y:1)], then it's unsound.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

This is the expected behaviour. The confusion comes from the lack of variance inference for GADTs, which is tracked elsewhere.