Skip to content

Bugs in debug_ppr_ty and ppr_ty

debug_ppr_ty outputs forall k. forall (a :: k) -> () like this:

forall @k_aFj[sk:2] a_aFk[sk:3]. ()

This isn't even valid Haskell.

The problem with ppr_ty is more subtle. It purposefully reorders foralls (see #18458), but it is overeager in doing so, as it shouldn't reorder visible forall. forall k -> (k ~ k) => forall j -> k -> j -> Type becomes:

forall k j -> (k ~ k) => k -> j -> Type

But surely this isn't right (or else why don't we also float out k -> and j ->?)

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