Skip to content

Multiplicity polymorphic record accessor

The documentation states that

newtype T1 a = MkT1 { getT1 :: a }

can be written with multiplicity polymorphism

construct :: forall {m} a. FUN m a (T1 a)
construct = MkT1

destruct :: forall {m} a. FUN m (T1 a) a
destruct (MkT1 a) = a

But destruct can not be defined in terms of its field accessor getT1: should getT1 not get a multiplicity polymorphic type?


Side question: For a newtype, we would normally be able to use coerce (and unsafeCoerce) to implement both of these functions. But coerce isn't multiplicity polymorphic, so an error is reported: "Couldn't match type ‘m’ with ‘'Many’". Is there any way to coerce :: FUN m a b (safely or unsafely)

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