GADT record syntax accepts linearity annotations
GHC completely ignores multiplicity annotations on arrows in GADT record-style constructors. As a result, the following program is accepted:
{-# LANGUAGE UnicodeSyntax, LinearTypes #-}
module M where
data R where
D1 :: { d1 :: Int } %1 -> R
Dp :: { dp :: Int } %p -> R
Dl :: { dl :: Int } ⊸ R
However, this syntax does not make any sense, and the constructors are treated as if they were written with an ordinary ->
.
Patch coming.