почему?

Вы же вроде справшивали про это в багтрекере ghc, вам там правильно сказали что элементы хлиста всегда кайнда Type, a (Symbol, Type) /= Type. Так что проверять что элементы хлиста имеют кайнд (Symbol, Type) бессмысленно - точно не имеют.

Чтобы сделать рекорд на хлистe вы можете объявить ньютайп

newtype Field (name :: Symbol) typ = Field typ

и считать рекордом такой хлист, у которого все типы элементов вида Field _ _ (кайнда Type) . Проверять тогда можно как-то так:

type family Check ts where
  Check (HList '[])           = () :: Constraint
  Check (HList (Field _ _:r)) = Check (HList r)
  Check (HList (t:_))         = TypeError ('Text "Non-Field type in record: " ':<>: 'ShowType t)

class Check ts => Record ts
instance Check ts => Record ts

Но лучше конечно сделать как Adam Gundry написал, что-нибудь типа

data Record ts where
  RNil :: Record '[]
  (:>) :: x -> Record xs -> Record ('(name, x) : xs)

Тогда у вас Record является рекордом by construction, никаких проверок не нужно. См. parse, not validate.

Или, если вы все-таки хотите сделать на хлисте, например чтобы рекорд можно было использовать как хлист, можно взять более общий хлист параметризованный типом f:

-- Data.SOP.NP из sop-core, NP Identity ~= HList
data NP f xs where
  Nil  :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x:xs)
infixr 5 :*

type Snd :: (a, b) -> b
type family Snd t where
  Snd '(_, b) = b

newtype Field nt = Field (Snd nt)

type Record = NP Field

foo :: Record [ '("foo", Bool), '("bar", Int) ]
foo = Field True :* Field 1 :* Nil

newtype Field (name :: Symbol) typ = Field typ

type family Check ts where
  Check (HList '[])           = () :: Constraint
  Check (HList (Field _ _:r)) = Check (HList r)
  Check (HList (t:_))         = TypeError ('Text "Non-Field type in record: " ':<>: 'ShowType t)

class Check ts => Record ts
instance Check ts => Record ts

data Record ts where
  RNil :: Record '[]
  (:>) :: x -> Record xs -> Record ('(name, x) : xs)

-- Data.SOP.NP из sop-core, NP Identity ~= HList
data NP f xs where
  Nil  :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x:xs)
infixr 5 :*

type Snd :: (a, b) -> b
type family Snd t where
  Snd '(_, b) = b

newtype Field nt = Field (Snd nt)

type Record = NP Field

А сделать общую версию Check возможно? Не хочется писать под каждый кейс.

И ещё смежный вопросик - почему стринги не лифтятся автоматом, как это делают числа ?

Не знаю как более точно описать, но почему у значений * нельзя проверять кайнд? Напр у Either Int String это *, но это ещё и просто Either.

Обобщенную Check в смысле higher order function All, чтобы использовать как All IsField? В принципе возможно, но нужна дефункциализация, нативных hof на уровне типов нет. Посмотрите например https://blog.poisson.chat/posts/2018-08-06-one-type-family.html, https://hackage.haskell.org/package/first-class-families

я на этом тайплевел рексхемы написал)

Я помню тайплевел линзы на синглтонах делали)

> И ещё смежный вопросик - почему стринги не лифтятся автоматом, как это делают числа ?

Не распарсил, что значит лифтятся?

вроде так же лифтятся, как и числа

Промоутятся всм? Вроде бы да, так же

все оно работает

Prelude> :t "Test"
"Test" :: [Char]
Prelude> :kind! "Test"
"Test" :: GHC.Types.Symbol
= "Test"

Ясно, спс

https://hackage.haskell.org/package/recover-rtti-0.3.0.0

смотрите какая классная штука

а оно умеет так?
▢ : ✶ ?

как им пользоваться?

> data X = X
> data Y = Y X X
> Debug.RecoverRTTI.anythingToString (Y X X)
"Y X X"

> Debug.RecoverRTTI.anythingToString (1, \x -> x)
"(1,<Fun>)"

ого, это тоже круто

можно через явный forall как-то от Proxy избавиться?
type (~>) f g = Proxy f -> Proxy g -> Type

type f ~> g = forall a. f a -> g a
?