Zero Multiplicities for Linear Haskell

[Zullo, Joseph Anthony]

Hello GHC developers,

I am Joseph Zullo, a PhD student at Purdue University. I am newly subscribed to this mailing list and my approval for GitLab is awaiting approval: my username is jazullo. I may be interested in adding Zero as a multiplicity to Linear Haskell as discussed in the source code notes<https://github.com/ghc/ghc/blob/e258ad546d96fcfffd525f9b51d237cee467ad73/compiler/GHC/Core/Multiplicity.hs#L144>. My current use-case is with Liquid Haskell: I have Liquid Haskell proof terms embedded in linearly typed procedures, but the "ghost" proof terms consume terms nonlinearly even though they have no bearing on the linear style of the procedure (a binary "?" operator is used with terms to the left and proofs to the right). I am looking for any work arounds for this issue, or for any help or interest in adding zero as a multiplicity so that proof terms can be casted as non-consuming. Let me know if there are any proper avenues for this problem and/or proposal. I greatly appreciate any direction or assistance.

Joseph

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240801/8bae9e35/attachment.html>