Убедить компилятор в том, что существует допустимая цепочка экземпляров

Хорошо. Проблема здесь довольно абстрактная. Потерпите меня.

У меня есть группа «Юнитов», каждая из которых имеет определенные свойства. Эти свойства определены в классе Seq следующим образом:

class Seq a x y where
    break :: x -> (a, y)
    build :: a -> y -> x

Концептуально тип a является важным типом, x - контекст, используемый для генерации an a , а y - это контекст, используемый для генерации любых дополнительных экземпляров Seq . break разрушает Seq , build позволяет вам восстановить его.

В отдельных экземплярах Seq это работает нормально. Однако у меня также есть конструктор данных, который выглядит следующим образом:

data a :/: b = a :/: b deriving (Eq, Ord)
infixr :/:

Цель всей этой операции - создать экземпляры Seq .

Например, если у меня есть a , b и c , все экземпляры Seq такие, что a подает в b и b подает в c , тогда у меня автоматически должен быть экземпляр Seq для a: /: b: /: c . Класс для настройки этого довольно прост с помощью рекурсивного типа данных:

instance (Seq a x y, Seq b y z) => Seq (a :/: b) x z where
    break x = let
        (a, y) = break x :: (a, y)
        (b, z) = break y :: (b, z)
        in (a :/: b, z)

    build (a :/: b) z = let
        y = build b z :: y
        x = build a y :: x
        in x

Проблема в том, что я не могу его использовать. Если я определю следующие три экземпляра Seq :

data Foo
instance Seq Foo Integer Bool

data Bar
instance Seq Bar Bool Bar

data Baz
instance Seq Baz Bar ()

(детали реализации отредактированы, подробнее см. здесь )

и хорошо типизированная функция break :

myBreak :: Integer -> (Foo :/: Bar :/: Baz)
myBreak = fst . break' where
    break' = break :: Integer -> (Foo :/: Bar :/: Baz, ())

тогда я даже не могу скомпилировать:

No instances for (Seq Foo Integer y, Seq Bar y y1, Seq Baz y1 ())
  arising from a use of `break'
Possible fix:
  add instance declarations for
  (Seq Foo Integer y, Seq Bar y y1, Seq Baz y1 ())
In the expression: break :: Integer -> (Foo :/: (Bar :/: Baz), ())
In an equation for break':
    break' = break :: Integer -> (Foo :/: (Bar :/: Baz), ())
In an equation for `myBreak':
    myBreak
      = fst . break'
      where
          break' = break :: Integer -> (Foo :/: (Bar :/: Baz), ())

Мне кажется, что myBreak не может быть уверен, что существует «рабочий поток» контекстов из Foo → Bar → Baz. Как мне убедить компилятор, что это хорошо типизировано?

Это один из моих первых экскурсий в программирование типов, поэтому я, несомненно, нарушаю некоторые устоявшиеся правила. Мне очень любопытно, что я здесь делаю не так, но я также открыт для предложений о том, как лучше достичь своих целей.