Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information