Skip to content

Linear types: multiplicity in pattern synonyms

Linear types currently do not support pattern synonyms. Currently, multiplicity annotations are ignored and replaced by normal unrestricted functions.

{-# LANGUAGE PatternSynonyms, GADTs, LinearTypes #-}

pattern J :: x %1 -> Maybe x
pattern J a = Just a
-- J is given type x -> Maybe x

Instead, we should reject. Later, we can add support for linear pattern synonyms.

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