единственное, что фигачить синглетоны руками это бойлерплейт еще в добаовок к тому, что надо все по три раза писать

потому всякие пакеты singletons и делаются

Все радуйтесь я пошёл

можно попробовать написать вручную

data N = Z | S N

data SN n where
 SZ :: SN Z
 SS :: SN a -> SN (S a)

data SomeN = forall n. (Typeable n, KnownN n) => SomeN (SN n)

class KnownN (a :: N) where
 liftN :: N -> Maybe SomeN

instance KnownN Z where
 liftN Z = Just (SomeN SZ)
 liftN _ = Nothing

instance (Typeable n, KnownN n) => KnownN (S n) where
 liftN (S n) = case liftN @n n of
   Just (SomeN (n :: SN m)) | Just Refl <- eqT @n @m -> Just (SomeN (SS n))
   _ -> Nothing
 liftN _ = Nothing

О, а тут снег, круто

но такое не сработает, потому что не ясно как выбирать нужный инстанс

Always has been

вся магия тут в том, что ghc сам выбирает этот инстанс

да инстансы ноун нат и не нужны, синглетоны просто матчить потом да и все

ну нужно же как-то этот синглтон построить сначала

из обычного N

и в чем проблема?

ну это не попытка сделать самому, это вот к вопросу о том что за KnownNat и как он работает

data N = Z | S N

data SN n where
 SZ :: SN Z
 SS :: SN a -> SN (S a)

data SomeN = forall n. SomeN (SN n)

liftN :: N -> SomeN
liftN Z = SomeN SZ
liftN (S n) =
 case liftN n of
   SomeN n -> SomeN (SS n)

можно и так сделать

не могу понять почему let и case работают по-разному

почему let не достает exist типы

вот выше как вместо case сделать let

Вью паттерн напиши)

вот такой же код с нуля