Спасибо, стало ясно имеется еще пара вопросов тогда: 1) почему instance {-# OVERLAPPING

#-} (KnownSymbol name, name ~ "") => Cls name where
f = "empty symbol"

instance {-# OVERLAPPABLE #-} (KnownSymbol anyName) => Cls anyName where
f = "any symbol"

не заводится и ругается на на duplicate instance declarations , хотя чисто интуитивно инстанс для пустого символа и констрейнт на равенство пустой строке должны быть эквивалентны

2) если все-таки очень хочется чтобы для значений, не известных в компайл-тайме, выбирался инстанс с empty symbol , есть ли какие-то воркэраунды?

потому что инстансы выбираются только по части после => (называется instance head)

по пункту 2 — запихать логику проверки на empty в один инстанс для KnownSymbol name => Cls name

https://hackernoon.com/typeclass-instance-selection-fea1068920e6

Насколько я понимаю OVERLAPS/OVERLAPPING решается только когда однозначно понятно, в отличии от инкохерента. Это, например, дает ошибку class Foo (x :: Nat) where x :: String instance {-# OVERLAPS #-} Foo 0 where x = "zero" instance {-# OVERLAPPING #-} KnownNat n => Foo n where x = show $ natVal $ Proxy @n foo :: forall n . KnownNat n => String foo = x @n

а на оба стула — компайл-тайм проверку для константных значений и рантайм-проверку для неизвестных в компайл-тайме значений не усесться?

Тут не работает потому что тут два интанса могут потенциально подойти, а для этого нужно знать сам тип (а в месте выбора он не известен)

Да, вопрос-то почему работает это bar :: SomeNat -> String bar (SomeNat (Proxy :: Proxy n)) = x @n При том что такое ожидаемо не работает baz :: (forall r . (forall n . KnownNat n => Proxy n -> r) -> r) -> String baz f = f \(Proxy :: Proxy n) -> x @n

Чтобы сделать то что ты тут хочешь надо name ~ “” вынести в голову (после `=>`). Читать тут: https://kseo.github.io/posts/2017-02-05-avoid-overlapping-instances-with-closed-type-families.html

А инстансы там какие?

спасибо, щас прочту

Мне кажется, он всегда будет выводить число, даже есть передать 0

Мне кажется, тут разница в том что в пером у тебя из-за GADT вводится в скоуп новый тип, а во втором ты конструируешь значение типы `forall n . KnownNat n => Proxy n -> r` и это *значение* пытает тайпчекнутся. В первом случае у тебя эта переменная не пытается тайпчекнутся извне.

сколотил что-то типа такого class Cls (name :: Symbol) where f :: String instance (IsEmpty name ~ flag, Cls' flag name) => Cls name where f = f' @flag @name (Proxy :: Proxy flag) class Cls' (flag :: Bool) (name :: Symbol) where f' :: Proxy flag -> String instance Cls' 'True name where f' _ = "empty symbol" instance Cls' 'False anyName where f' _ = "any symbol" type family (IsEmpty (a :: Symbol)) :: Bool where IsEmpty "" = 'True IsEmpty _ = 'False main :: IO () main = do let s = "" let someSymb = someSymbolVal s case someSymb of (SomeSymbol (p :: Proxy w)) -> putStrLn $ f @w при вызове f @w ругается на • Could not deduce (Cls' (IsEmpty n) n) arising from a use of ‘f’ from the context: KnownSymbol n я правильно понимаю что это из-за того, что неизвестен результат IsEmpty w в компайл-тайме?

Зарепорчу пожалуй, очень надеюсь что это баг