search

ocaml / ocaml

The core OCaml system: compilers, runtime system, base libraries
https://ocaml.org
Other
5.46k stars 1.1k forks source link

Infer variance for GADTs without equality #7494

Closed vicuna closed 2 years ago

vicuna commented 7 years ago

Original bug ID: 7494 Reporter: @yallop Assigned to: @garrigue Status: assigned (set by @yallop on 2017-02-24T14:28:33Z) Resolution: open Priority: normal Severity: feature Category: typing Related to: #5688 #7004 Monitored by: @gasche

Bug description

The current approach to variance for GADT-style definitions is overly conservative.

For example, the following program is currently accepted:

type 'a t = T of 'a type +'a s = 'a t

but the following program, which ought to be equivalent, is rejected:

type 'a t = T : 'a -> 'a t type +'a s = 'a t

The second program can be fixed by adding a variance annotation to 't' -- i.e., variance for GADT-style definitions is checked, but not inferred.

It would be safe, consistent, and convenient to infer variance for parameters of GADT-style definitions that don't partake in any equalities (i.e. that are not refined in the return types of constructors).

vicuna commented 7 years ago

Comment author: @gasche

I thought I'd add a reference to my work on variance of GADTs, that discusses whether it is possible to also infer variances for variables that do participate in GADT equations (in short: yes, but it requires making assumptions on the language that are true today but would not necessarily be preserved by new typing features):

GADTs meet subtyping Gabriel Scherer, Didier Rémy, 2013 https://arxiv.org/abs/1301.2903

github-actions[bot] commented 4 years ago

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.

garrigue commented 4 years ago

This issue seems to be about something much simpler: currently, a variant type is consider to be a GADT as soon as one of its constructors is given with an explicit return type. But this syntax can also be used for normal constructors (involving no equation). It would be better to have a semantic criterion. This said, the syntactic criterion also has advantages, as changes In behaviour are immediately visible from the syntax.

gasche commented 4 years ago

Well I assume that @yallop would also be interested in constructors that do contain existential types, or add equality constraints on some other type parameters. The point is to ask whether the non-guarded parameters could have their variance inferred.

github-actions[bot] commented 3 years ago

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.

github-actions[bot] commented 2 years ago

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.