Anonymous | Login | Signup for a new account | 2018-12-16 09:08 CET |

Main | My View | View Issues | Change Log | Roadmap |

View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||

ID | Project | Category | View Status | Date Submitted | Last Update | ||||||

0007784 | OCaml | typing | public | 2018-04-25 00:15 | 2018-04-25 15:59 | ||||||

Reporter | ivg | ||||||||||

Assigned To | |||||||||||

Priority | normal | Severity | minor | Reproducibility | have not tried | ||||||

Status | new | Resolution | open | ||||||||

Platform | OS | OS Version | |||||||||

Product Version | 4.02.3 | ||||||||||

Target Version | Fixed in Version | ||||||||||

Summary | 0007784: unexpected weak type variable in GADT typing | ||||||||||

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

Tags | No tags attached. | ||||||||||

Attached Files | |||||||||||

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 |