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

Но это все равно не отвечает на вопрос

Второй ты можешь вернуть из скуопа, а первый нет по-моему

Вернуть типа какой-нибудь Vec n a? Ни в одном не могу по идее, оба экзистенциальные

сколотил что-то типа такого

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 в компайл-тайме?

да

Про него только KnownSymbol известно

Потому что оно в рантайме только появляется

что вообще сугубо идейно значит приставка Known в KnownNat , KnownSymbol и тд?

А понять IsEmpty можно только во время компиляции

Потому что после компиляции IsEmpty пропадает

я как раз таки и думал что оно значит "мы знаем, чему равно"

Что можно создать значение, соответсвующие типу

Что мы знаем это значение

Что это как бы “известный” тип

так на w же есть KnownSymbol

да

что по идее должно значить "мы знаем, что это за тип"

но по идее не знаем

Но это уже хаки компилятора