Skip to content

Add a note about non-deferrable constraints

It would be nice to add a Note that explains the current way we avoid deferring certain errors, using nonDeferrableOrigin. There currently is Note [No deferring for multiplicity errors], but it should be expanded to cover the representation-polymorphism checks (and IsRefl#, which currently only uses FixedRuntimeRep origins, but that could change).

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