Open
Description
SNat
is part of base-4.18.0.0
and later. Up to this point, we've defined our own version:
data SNat (n :: Nat) where
SNat :: KnownNat n => SNat n
base
's version is a bit more complex:
newtype SNat (n :: Nat) = UnsafeSNat Natural
type role SNat nominal
pattern SNat :: forall n. () => KnownNat n => SNat n
pattern SNat <- (knownNatInstance -> KnownNatInstance)
where SNat = natSing
{-# COMPLETE SNat #-}
data KnownNatInstance (n :: Nat) where
KnownNatInstance :: KnownNat n => KnownNatInstance n
knownNatInstance :: SNat n -> KnownNatInstance n
knownNatInstance sn = withKnownNat sn KnownNatInstance
Could we re-export for newer bases and expect everything to JustWork(tm)?