Infer variance for GADTs without equality #7494
Comments
|
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 |
|
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 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. |
|
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. |
|
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 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. |
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).
The text was updated successfully, but these errors were encountered: