Skip to content

Make UnsafeSNat et al. into pattern synonyms

Matthew Craven requested to merge wip/UnsafeSNat-pattern-synonyms into master

...so that they do not cause coerce to bypass the nominal role on the corresponding singleton types when they are imported. See Note [Preventing unsafe coercions for singleton types] and the discussion at #23478.

This also introduces unsafeWithSNatCo (and analogues for Char and Symbol) so that users can still access the dangerous coercions that importing the real constructors would allow, but only in a very localized way.

Merge request reports