基于闭类型族的Data Types a la Carte泛型类型失效问题问询

为解决表达式问题（EP），我们可以使用Data Types a la Carte扩展分离构造器与行为，该方案通过类型类实现自动注入以简化开发。但它存在无法回溯的局限：对于f :<: g的子类型关系，f必须是原子类型，g需要是链表结构，这会给类型别名的添加带来问题，也无法检测右侧的重复类型。

根据Bahr的论文，我们可以通过闭类型族添加回溯功能解决上述问题，用类型级函数搜索f在g中的存在性来实现f :<: g关系：

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

data Res = Found Pos | NotFound | Ambiguous

-- | 搜索f在g中的存在性
type family Elem (f :: Type -> Type) (g :: Type -> Type) :: Res

-- | 搜索g的所有分支，若f出现多次则拒绝
type family Choose (f :: Type -> Type) (g :: Type -> Type) (a :: Res) (b :: Res) :: Res 

-- | 若f是复合表达式，搜索其所有部分
type family Sum' (a :: Res) (b :: Res) :: Res

-- | `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’

由于开放世界假设，这个方案失去了实用性——如果每次添加构造器都需要明确指定f，程序就会失去扩展性。请问我遗漏了什么？

内容的提问来源于stack exchange，提问作者pe200012