uom-plugin icon indicating copy to clipboard operation
uom-plugin copied to clipboard
verified publisher icon adamgundry

Probable type soundness bug

Open adamgundry opened this issue 3 years ago • 0 comments

I don't yet have a reproducer for this, but I believe it is probably possible to break type soundness if a GADT binds a unit equality, because uom-plugin may use this unit equality to prove others, but the generated evidence does not depend on the bound variable. Thus GHC may float it out from under the GADT pattern match.

adamgundry avatar Oct 08 '22 08:10 adamgundry