GADT record syntax does not accept linearity annotations
In #19928 (closed) @int-index dropped the parser's support for GADT record syntax with multiplicity annotations, since the annotations were not respected. For instance:
{-# LANGUAGE UnicodeSyntax, LinearTypes #-}
module M where
data R where
D1 :: { d1 :: Int, d1' :: Int } %1 -> R
DUr :: { dur :: Int, dur' :: Int } -> R
Is rejected with a parser error.
However, I was writing a program in which I made use of the syntax as in D1
, expecting to make both d1
and d1'
linear fields.
On the other hand, I would expect dur
and dur'
to be an unrestricted field.
I suppose I'm treading on undefined behaviour, but I think it is intuitive for linearity annotations to work in this way for GADT record syntax.
Discussion welcome!