如我们所知，为了解决EP，我们可以使用Data types a la carte来扩展程序的构造函数和行为。本文采用了一个类型类实现的自动注入，以减轻我们的程序编写。
然而，该解决方案有局限性，因为我们不能进行回溯：对于关系f :<: g，f必须是原子的，并且g必须以链表的形式构造：

type Arith = Val :+: Add

type NonAtomic = Arith :<: (Val :+: (Add :+: Mult))

-- op1 :: Arith :<: f => Fix f -> Fix f
-- op1 f = f `add0` val0 2

type NonListLike = Val :<: ((Mult :+: Val) :+: Add)

-- op2 :: Fix ((Val :+: Mult) :+: Add)
-- op2 = val0 2

type Associativity = (Add :+: (Mult :+: Val)) :<: ((Add :+: Mult) :+: Val)

-- op3 :: Fix ((Add :+: Mult) :+: Val)
-- op3 = val0 2 <+> val0 3

如果我们想添加一些类型别名，这可能会导致问题。此外，如果某些类型在右侧出现不止一次，则无法捕获。
根据Bahr's paper，我们可以使用封闭类型族添加回溯来解决上述问题。代替类型类，我们可以使用类型级别的函数来搜索f在g中的存在性，以找到关系f :<: g。

data Pos = Here | L Pos | R Pos | Sum Pos Pos

data Res = Found Pos | NotFound | Ambiguous

-- | search the existence of f in g
type family Elem (f :: Type -> Type) (g :: Type -> Type) :: Res

-- | search all branches in g. reject if f appears more than once in g
type family Choose (f :: Type -> Type) (g :: Type -> Type) (a :: Res) (b :: Res) :: Res 

-- | search all parts of f if f is a compound expression.
type family Sum' (a :: Res) (b :: Res) :: Res

-- | relation `f :<: g`
class Subsume (res :: Res) f g

我做了一个实验，它确实适用于混凝土类型：

type Arith = Val :+: Add

op1Fixed :: (Subsume (Elem Arith f) Arith f, f ~ (Val :+: (Add :+: Mult)))
    => Fix f
    -> Fix f
op1Fixed f = f <+> val 2

但当f推广时，事情就错了：

op1Fixed :: (Subsume (Elem Arith f) Arith f)
    => Fix f
    -> Fix f
op1Fixed f = f <+> val 2

-- Could not deduce (Subsume (Elem Add f) Add f)
--  arising from a use of ‘<+>’
-- Could not deduce (Subsume (Elem Val f) Val f)
--  arising from a use of ‘val’

即使我显式地证明我们可以从f中找到对应的构造函数：

op1Fixed :: forall f a b. (Subsume ('Found ('Sum a b)) Arith f)
    => Fix f
    -> Fix f
op1Fixed f = f <+> val 2

-- Could not deduce (Subsume (Elem Add f) Add f)
--  arising from a use of ‘<+>’
-- Could not deduce (Subsume (Elem Val f) Val f)
--  arising from a use of ‘val’

由于open world assumption，这使得解决方案变得无用。如果每次我们想添加构造函数时都必须知道f，那么程序就失去了扩展的灵活性。
全源here
我错过什么了吗？