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
nonrec misbehaves with GADTs #6934
Comments
Comment author: @diml I'd be in favor of just updating the error message to say that you can't use [nonrec] when defining a GADT. I don't like the idea of allowing [type nonrec t = A : t -> t] where the last two [t]s means two different things. |
Comment author: @mmottl @dim I agree that the syntax of GADTs doesn't compose nicely with "nonrec" here, and we don't want to break existing syntax. Maybe it would have been better to do something like: type t as u = t * u where the "t" on the RHS refers to the previous definition of "t", and "u" is the recursive alias for the current definition of "t". |
Comment author: @mmottl It's surely not a big problem. It's conceivable that a developer has opened a module and just wants to define type "t" in terms of a type "t" in the opened module. Though dropping "nonrec" and using an explicit module path would easily solve the issue, the error message will likely confuse the developer. |
I would like to be able to use
but sometimes the reason I'm wrapping it up is to use it as an argument of a functor like
and then call e.g. |
Given @mikeshulman's reasonable example above, I would be in favor of implementing the natural meaning of This allows for some somewhat confusing cases, such as:
but there is no ambiguity. On the other hand, I find So my recommendation:
|
Note that at the signature level, I have the impression than writing: type 'a inner_t := 'a t
type t = Wrap: 'a inner_t -> t works well enough and I am not sure complexifying the scoping rule for However, the structure level variant open struct type 'a inner_t = 'a t end
type t = Wrap: 'a inner_t -> t feels less lightweight. I would be more tempted to add |
I am also okay with going that route, but to be done properly (as a proper AST node with its own type-checking code) is more work, I expect, than just extending (Let me "reopen" this issue to indicate that a need for a different resolution has emerged.) |
Original bug ID: 6934
Reporter: @mmottl
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-03-15T23:38:28Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.2
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Monitored by: runhang @gasche @yallop @hcarty @mmottl
Bug description
Consider the following example:
type nonrec t = A : t
The above will fail with an unbound type constructor for "t". But it isn't really a recursive type, it's a GADT. I think "nonrec" shouldn't apply to the return type of a GADT, at least not to the outermost type constructor defining the GADT, though possibly to types in its parameters.
The text was updated successfully, but these errors were encountered: