You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.The text was updated successfully, but these errors were encountered: