Indeed that is the ticket.

There is one wrinkle that I should have mentioned earlier: not even all data constructor applications are admissible at the top level. In particular, constructors with strict fields may require computation to construct. The validity check would need to account for this, either by rejecting such constructors altogether or by having some of syntactic WHNF check.

Cheers,

- Ben

On January 21, 2023 5:06:13 PM EST, Tom Ellis <tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:
On Sat, Jan 21, 2023 at 10:52:33PM +0100, Jaro Reinders wrote:
On 21-01-2023 20:00, Ben Gamari wrote:
However, I suspect you do have a point when it comes to unlifted data
constructors. I think it would be fine to allow an application of a
data constructor of an unlifted type on the top-level:

   type UMaybe :: Type -> UnliftedType
   data UMaybe a = UNothing | UJust a

   x :: UMaybe Int
   x = UJust 42

Perhaps you could open a ticket for this?

This ticket seems related: #17521 Consider top-level unlifted bindings [1].

Or do you think it needs a separate ticket?

Thanks Jaro.  That ticket contains the observation

"there are other cases where unlifted types are desireable at the
 top-level (e.g. saturated data constructor applications). In
 principle it would be fairly straightforward to incorporate a
 validity check that admits top-level constructor applications which
 rejecting function applications if we wanted."

So I think that ticket subsumes my question, and filing another one
would be redundant.

Tom
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.