Можно ли определить типы данных с переменным числом родов?

Question

Я могу определить многогранное естественное преобразование следующим образом:

type family (~>) :: k -> k -> *
type instance (~>) = (->)

newtype NT a b = NT { apply :: forall x. a x ~> b x }
type instance (~>) = NT

Который работает во всех видах, поэтому я могу определить, например,

left :: Either ~> (,)
left = NT (NT (Left . fst))

Это круто и вдохновляет. Но независимо от того, сколько трюков я играю, я не могу получить что-то вариативное в возвращаемом типе. Например, я хотел бы

type family (:*:) :: k -> k -> k
type instance (:*:) = (,)
type instance (:*:) = ???

Кажется, что это невозможно, так как семейства типов должны быть полностью насыщенными, а конструкторы типов можно вводить только в *,

Я даже попробовал несколько неприятных трюков

type instance (:*:) = Promote2 (:*:)

type family Promote2 :: (j -> k -> l) -> (a -> j) -> (a -> k) -> (a -> l) where

promote2_law :: Promote2 f x y z :~: f (x z) (y z)
promote2_law = unsafeCoerce Refl

fstP :: forall (a :: k -> *) (b :: k -> *) (c :: k). (a :*: b) c -> a c
fstP = case promote2_law @(:~:) @a @b @c of Refl -> NT (\(a,b) -> a)

И я не знаю, есть ли у этого хоть какая-то надежда на работу, так как я не продумал, как "представленные" вещи более высокого рода. Но GHC знает, что я все равно лгу

• Couldn't match type ‘(,)’ with ‘Promote2 (,) a’
  Inaccessible code in
    a pattern with constructor: Refl :: forall k (a :: k). a :~: a,

Есть ли другие хитрости для этого?

Answer 1

"Аксиоматический" подход действительно работает, я просто неправильно использовал равенство:

fstP :: forall (a :: j -> k) (b :: j -> k) (x :: j). (a :*: b) x -> a x
fstP = castWith (Refl ~% promote2_law @(:*:) @a @b @x ~% Refl) fst
    where
    infixl 9 ~%
    (~%) = Data.Type.Equality.apply

С помощью Equality.apply Важно сообщить контролеру типа, где применить аксиому. Я сделал полную разработку продукции более высокого класса для справки.

Будьте предупреждены, поскольку я играл с этим, я однажды испытал панику GHC. Так что неприятные трюки могут быть неприятными. Все еще интересуются другими подходами.