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
GADT variance #7004
Comments
Comment author: @yallop The improvement you suggest is actually not sound, at least where the parameter appears more than once in the result type. Consider the equality GADT: type (+,) eql = Refl : ('a, 'a) eql If you make the first parameter covariant (for example) then you can coerce (x, x) t to (y, x) t whenever x is a subtype of y, which then allows you to convert freely between x and y when you match against Refl. |
Comment author: lavi Yes you are right, the parameter should only appear once. |
Comment author: @lpw25 Parameters which only appear once in the output and are not specialised can already be given a variance: type +_ t = T : 'a t If the variable is specialised: type _ t = T : <foo : int; bar : float> t then giving it a variance would be unsound: let f (type a) (x : a t) : a -> unit = f (T :> < foo: int > t) (object method foo = 4 end) |
Comment author: lavi Right, sorry, for the noise. In this case it is possible to write the cast: |
Original bug ID: 7004
Reporter: lavi
Assigned to: @lpw25
Status: closed (set by @xavierleroy on 2017-02-16T14:14:53Z)
Resolution: not a bug
Severity: feature
Category: typing
Related to: #7494
Bug description
Currently, variance on GADT are only allowed when the type is used like in a normal ADT.
I know variance in GADT is tricky, but a small and safe improvement would be to allow variance on parameters that appears only on result type.
The text was updated successfully, but these errors were encountered: