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

Что мы хотим?

Чтобы решить эту проблему, мы можем сначала разбить то, что мы хотим.

Мы хотим «провалиться» в поведении закрытого семейства типов (чтобы функции и нефункции соответствовали разным экземплярам), но мы также хотим конструировать данные как класс типа (чтобы мы могли получить refunct).

То есть нам нужен типовой класс с логикой близкого семейства типов. Итак, для этого мы можем просто разделить две части и реализовать их по отдельности; логика как замкнутое семейство типов, а все остальное как типовой класс.

Теперь для этого мы берем наше семейство типов и добавляем еще один параметр

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

становится

class
  Foo'
    (flag :: Flag)
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)

Этот параметр будет действовать как флаг, сообщающий нам, какой экземпляр использовать. Поскольку это своего рода Flag, нам нужно создать этот тип данных. У него должен быть конструктор для каждого экземпляра (в некоторых случаях мы можем немного потерять его, но в целом вам понадобится один к одному)

data Flag = Instance1 | Instance2 | Instance3 ...

^{(В случае моей проблемы, поскольку мы используем только два экземпляра Bool)}

Теперь мы создаем семейство закрытых типов, которое вычисляет, какой экземпляр должен соответствовать. Он должен взять соответствующие аргументы из параметров Foo и создать Flag

type family
  FooInstance
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
      :: Flag
  where
    FooInstance ... = Instance1
    FooInstance ... = Instance2
    FooInstance ... = Instance3
    ...

^{В случае рассматриваемого вопроса мы называем это IsAtomic, поскольку это имя описывает то, что он делает.}

Теперь мы модифицируем наши экземпляры, чтобы они соответствовали правильным Flags. Это довольно просто, мы просто добавляем флаг экземпляра в объявление:

instance
  ( Foo newBar newBaz newBax
  ...
  )
    => Foo' 'Instance3 foo bar baz bax
  where
    ...

Важно отметить, что мы не меняем рекурсивные вызовы Foo на вызовы Foo'. Мы собираемся создать Foo как оболочку для Foo', которая управляет нашим семейством закрытых типов (FooInstance в данном случае), поэтому мы хотим вызывать Foo, чтобы не вызывать каждый раз одну и ту же логику.

Это построено так:

class
  Foo
    (bar :: Type)
    (baz :: Type)
    (bax :: Type)
  where
    ...
instance
  ( Foo' (FooInstance bar baz bax) bar baz bax
  )
    => Foo bar baz bax
  where
    ...

Если мы хотим быть в большей безопасности, мы можем добавить строку к каждому экземпляру Foo', чтобы проверить, что он вызывается правильно:

instance
  ( Foo newBar newBaz newBax
  , FooInstance bar baz baz ~ 'Instance3
  ...
  )
    => Foo' 'Instance3 bar baz bax
  where
    ...

Мое решение

Итак, теперь мы используем эту стратегию для решения конкретного вопроса. Вот код полностью. Соответствующий класс SeparateArgs:

type family
  IsAtomic
    ( a :: Type )
      :: Bool
  where
    IsAtomic (a -> b) = 'False
    IsAtomic a = 'True

class
  SeparateArgs
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig
  , newSig -> args goal
  where
    refunct :: (HList args -> goal) -> newSig

instance
  ( IsAtomic newSig ~ isAtomic -- For (possible? compilation time) speedup
  , SeparateArgs' isAtomic args goal newSig
  )
    => SeparateArgs args goal newSig
  where
    refunct = refunct' @isAtomic

class
  SeparateArgs'
    (isAtomic :: Bool)
    (args :: [Type])
    (goal :: Type)
    (newSig :: Type)
  | args goal -> newSig isAtomic
  , newSig isAtomic -> args goal
  where
    refunct' :: (HList args -> goal) -> newSig
instance
  ( IsAtomic goal ~ 'True -- Only exists to ensure we are not invoking this in an illegal manner
  )
    => SeparateArgs' 'True '[] goal goal
  where
    refunct' makeA = makeA HNil
instance
  ( IsAtomic (headArg -> c) ~ 'False -- Only exists to ensure we are not invoking this in an illegal manner
  , SeparateArgs tailArgs goal c
  )
    => SeparateArgs' 'False (headArg ': tailArgs) goal (headArg -> c)
  where
    refunct' hFunct x = refunct $ hFunct . (x :>)