Экземпляры типа по умолчанию ссылаются друг на друга

Есть ли способ иметь экземпляры типа по умолчанию, определенные в терминах друг друга? Я пытаюсь сделать что-то вроде этого:

{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
data Tag = A | B | C

class Foo (a :: *) where
    type Bar a (b :: Tag)

    type Bar a A = ()
    type Bar a B = Bar a A
    type Bar a C = Bar a A

instance Foo Int where
    type Bar Int A = Bool

test :: Bar Int B
test = True

но это не работает:

Couldn't match type `Bar Int 'B' with `Bool'
In the expression: True
In an equation for `test': test = True

Обратите внимание, что это также не работает:

test :: Bar Int B
test = ()

Ответы

Ответ 1

Да, экземпляры типа по умолчанию могут быть определены в терминах друг друга (как вы можете видеть из своего собственного примера):

instance Foo Int where
--    So the default recursive definition will be used instead
--    type Bar Int A = Bool

test :: Bar Int B
test = ()

Однако, когда вы переопределяете связанный синоним типа в определении вашего экземпляра для Int, вы заменяете целую по умолчанию на 3 строки Bar (а не только type Bar a A = ()) одной строкой type Bar Int A = Bool, что означает Bar Int B и Bar Int C, больше не определены.

Итак, я предполагаю, что один из способов использования рекурсивных значений по умолчанию, как вы предполагали, - это переопределить определенные синонимы (хотя это довольно многословно):

class Foo (a :: *) where
    type Bar a (b :: Tag)
    type Bar a A = BarA a
    type Bar a B = BarB a

    type BarA a
    type BarA a = ()

    type BarB a
    type BarB a = Bar a A

-- This now works
instance Foo Int where
    type BarA Int = Bool

test :: Bar Int B
test = True

Которые могут вернуться к значениям по умолчанию:

-- As well as this one
instance Foo Int where
--    type BarA Int = Bool

test :: Bar Int B
test = ()