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)