基于Trees That Grow的类型族约束设计与类型类使用疑问

基于Trees That Grow惯用法设计的抽象语法树定义如下：

data Expr χ  
  = Lam  (Lamfam χ) Name (Ty χ) (Expr χ)
  | App  (Appfam χ) (Expr χ)
  | Unit (Ufam χ)

data Ty χ  
  = UnitTy (Utyfam χ)
  | Arrow (Arrfam χ) (Ty χ) (Ty χ)

type family Lamfam χ
type family Appfam χ
type family Ufam χ
type family Utyfam χ
type family Arrfam χ

为了给这套类型族添加针对性约束（论文提供的方案仅支持给所有类型添加相同约束），在实现泛化于参数χ的双向类型检查算法时，需要lamToArr :: Lamfam χ -> Arrfam χ这类函数传递扩展信息，于是尝试用类型类封装这些转换：

class Checker χ where  
  lamToArr :: Lamfam χ -> Arrfam χ
  unitToTy :: Ufam χ -> Utyfam χ

但编译时触发了类型歧义错误：

• Couldn't match type: Lamfam χ0
with: Lamfam χ
Expected: Lamfam χ -> Arrfam χ
Actual: Lamfam χ0 -> Arrfam χ0
NB: ‘Lamfam’ is a non-injective type family
The type variable ‘χ0’ is ambiguous
• In the ambiguity check for ‘lamToArr’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method:
lamToArr :: forall χ. Checker χ => Lamfam χ -> Arrfam χ
In the class declaration for ‘Checker’
|
41 | lamToArr :: Lamfam χ -> Arrfam χ
| ^^^^^^^^

核心疑问：开启AllowAmbiguousTypes禁用歧义检查，或是将类型族声明为injective，哪种方案更合理？哪种更适配需求——约束需描述特定算法的类型间信息流，仅提供当前阶段所需内容，同时支持无需修改核心算法即可扩展语法树？

1. 开启AllowAmbiguousTypes #

这是更贴合Trees That Grow设计目标的方案：

• 无需修改现有类型族定义，完全保留语法树的扩展性：Trees That Grow的核心就是通过χ参数自由定制节点的附加信息，而injective类型族会强制χ与Lamfam χ等一一对应，限制了扩展的灵活性（比如无法让不同的χ对应相同的附加信息类型）。
• 歧义问题仅在调用类方法时需要显式指定χ类型（借助TypeApplications扩展），但这是可控的，且符合“仅提供算法阶段所需内容”的需求：核心类型检查逻辑无需改动，新增扩展χ时只需实现对应的Checker实例即可。

2. 声明injective类型族 #

这种方案的局限性明显：

• 要求类型族是单射的（即若Lamfam χ1 = Lamfam χ2则χ1 = χ2），这会大幅压缩χ的设计空间，违背了Trees That Grow“自由扩展语法树”的初衷。
• 虽然能消除编译歧义，但牺牲了扩展性，无法满足“无需修改核心算法即可扩展”的核心需求。

优先选择开启AllowAmbiguousTypes配合TypeApplications的方案，既能保留Trees That Grow的扩展性，又能满足类型检查算法中类型间信息流的约束要求。

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