Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007784OCamltypingpublic2018-04-25 00:152018-04-25 15:59
Reporterivg 
Assigned To 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusnewResolutionopen 
PlatformOSOS Version
Product Version4.02.3 
Target VersionFixed in Version 
Summary0007784: unexpected weak type variable in GADT typing
DescriptionConsider 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 `ident`is `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 Reproducethe steps above are reproducible in all compilers starting with 4.02.3 till 4.06. I didn't test other versions.
Additional InformationOf 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

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019057)
sliquister (reporter)
2018-04-25 03:05
edited on: 2018-04-25 03:08

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

(0019061)
ivg (reporter)
2018-04-25 15:05

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)
(0019062)
sliquister (reporter)
2018-04-25 15:59

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.

- Issue History
Date Modified Username Field Change
2018-04-25 00:15 ivg New Issue
2018-04-25 03:05 sliquister Note Added: 0019057
2018-04-25 03:08 sliquister Note Edited: 0019057 View Revisions
2018-04-25 15:05 ivg Note Added: 0019061
2018-04-25 15:59 sliquister Note Added: 0019062


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker