nonrec misbehaves with GADTs

[vicuna]

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.

[vicuna]

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.

[vicuna]

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".

[vicuna]

Comment author: @garrigue

My understanding is that nonrec is essentially intended for type abbreviations.
So is its not working with GADTs really a problem?
I tend to concur with @dim.

[vicuna]

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.

[vicuna]

Comment author: @garrigue

Fixed in commit f900888 by introducing a new error message:

type nonrec t = A : t;;
Line _, characters 16-21:
Error: GADT case syntax cannot be used in a 'nonrec' block.