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 (closed).

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