Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

unexpected weak type variable in GADT typing #7784

vicuna opened this Issue Apr 24, 2018 · 3 comments


None yet
1 participant
Copy link

vicuna commented Apr 24, 2018

Original bug ID: 7784
Reporter: @ivg
Status: new
Resolution: open
Priority: normal
Severity: minor
Version: 4.02.3
Category: typing
Monitored by: @gasche

Bug description

Consider the following minimized example:

type _ exp = Int : int -> 'a exp

In the following, the type variable 'a is generalized

 Int 0;;
 - : 'a exp = Int 0

However if we will substitute the constructor argument with a nonexpansive expression ident 0, where identis fun x -> x, then the type variable is not generalized:

let ident x = x 
# Int (ident 0);;
- : '_a exp = Int 0

Expected result - either both expressions should not be generalized or both generalized.

Steps to reproduce

the steps above are reproducible in all compilers starting with 4.02.3 till 4.06. I didn't test other versions.

Additional information

Of course, we can use variance annotations and everything will work as expected. But as always this is a simplified example, a less simplified example is the following:

type _ exp = 
 | Int : int -> [> rhs] exp
 | Var : int -> [> lhs] exp
 | Cat : ('a exp * 'a exp) -> 'a exp

Unfortunately, variance checker can't cope with the [> rhs] exp part.

Even when I explicitly specify the variance of the rhs type constructor, with

type +'a rhs = 'a constraint 'a = [> `rhs]

I'm still getting

type +'a exp = Int : int -> 'a rhs exp;;
Characters 17-55:
type +'a exp = Int : int -> 'a rhs exp;;
Error: In this GADT definition, the variance of some parameter
   cannot be checked

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Apr 25, 2018

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;;


This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Apr 25, 2018

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 =
let g x ~y = x + y;;
val g : int -> y:int -> int =

Int (f ~y:1);;

  • : '_a exp = Int

Int (g ~y:1);;

  • : 'a exp = Int

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

| Texp_apply(e, (_,None)::el) ->
is_nonexpansive e && List.for_all is_nonexpansive_opt ( 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 ( snd el)


This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Apr 25, 2018

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.

@vicuna vicuna added the typing label Mar 14, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.