Unison 语言 Kind 不匹配错误详解:从 fix4397 回归用例看 Kind 推断与错误报告机制 编程语言编译器语言运行时开发工具【免费下载链接】unisonA friendly programming language from the future项目地址https://gitcode.com/gh_mirrors/un/unison点击查看免费下载Unison 是一门面向未来的友好编程语言其类型系统具备完整的 Kind种类推断能力。本文以仓库中的回归测试用例 unison-src/transcripts/idempotent/fix4397.md 为切入点深入讲解 Unison 中Kind mismatch arising fromKind 不匹配类错误的触发场景、报告格式以及其背后的约束生成与求解实现原理。读完本文你将能够准确读懂 Kind 错误信息、在定义数据类型时规避高阶参数误用并了解该错误如何从编译器内部约束求解过程映射到用户可见的错误提示。fix4397 回归用例一个最小化的 Kind 不匹配场景fix4397.md 是 Unison 仓库中 idempotent幂等转录测试集合的一员用于锁定一个特定的编译器行为当高阶类型参数被错误地应用到普通类型而非类型构造器上时编译器必须报告清晰的 Kind 不匹配错误而不是崩溃或产生难以理解的内部信息。该用例的输入代码只有短短几行structural type Foo f Foo (f ()) unique type Baz Baz (Foo Bar) unique type Bar Bar Baz对应的预期输出由 ucm 捕获Loading changes detected in scratch.u. Kind mismatch arising from 3 | unique type Baz Baz (Foo Bar) Foo expects an argument of kind: Type - Type; however, it is applied to Bar which has kind: Type.这个用例的核心在于一个跨声明的 Kind 推断问题Foo f声明了一个类型参数f其字段为f ()。由于f被应用到一个具体的类型参数()Unit 类型编译器可以推断f的 Kind 必须是Type - Type即它必须是一个类型构造器如Optional、List之类。Baz尝试用Bar来实例化Foo。而Bar是一个普通的数据类型声明其 Kind 是Type。Foo要求其参数具有Type - TypeBar却只有Type二者冲突于是产生 Kind 不匹配错误。值得注意的是Bar与Baz之间存在相互引用Bar Baz与Baz (Foo Bar)属于同一个递归声明组件这要求 Kind 推断必须跨越整个组件进行求解才能发现Foo与Bar之间的不一致。这正是该回归用例存在的意义验证编译器在组件级 Kind 推断中能正确捕获此类错误并给出精确到具体代码行第 3 行的错误定位。Kind种类在 Unison 中是什么在类型理论中Kind 是类型的类型。Unison 核心库对 Kind 的定义非常精简见 unison-core/src/Unison/Kind.hsdata Kind Star | Arrow Kind Kind deriving (Eq, Ord, Read, Show, Generic)即 Unison 的 Kind 只有两种构造Star表示普通的类型即可以承载值的那种例如Nat、Text、Bar都拥有 KindType即StarArrow Kind Kind表示类型构造器即从一种类型映射到另一种类型的构造例如Optional、List、上文中的Foo拥有 KindType - Type。此外能力ability在 Unison 中被赋予了独立的 KindAbility见下文错误分类中对EffectListMismatch的说明用来与普通类型区分。结合 fix4397 的报错文案Foo expects an argument of kind: Type - Type; however, it is applied to Bar which has kind: Type可以看到 Kind 信息被直接呈现给用户。掌握这一概念是读懂一切 Kind 错误信息的前提。错误信息的结构与解读方法报告格式拆解Kind mismatch arising from类错误的报告由三部分构成由 parser-typechecker/src/Unison/KindInference/Error/Pretty.hs 中的ArgumentMismatch分支格式化标题行Kind mismatch arising from提示这是一次 Kind 层面的类型错误定位行3 | unique type Baz Baz (Foo Bar)用带行号的源码片段精确指示冲突发生的位置说明段Foo expects an argument of kind: Type - Type; however, it is applied to Bar which has kind: Type.指出期待什么与实际给了什么之间的差距。通用解读技巧解读此类错误时只需要抓住一句话中的两个 Kindexpects an argument of kind ...给出的是目标被调用方期望的参数 Kindit is applied to ... which has kind ...给出的是实际传入参数的类型所拥有的 Kind。两者不一致即为错误根源。若把 expects ... Type - Type; however, it is applied to ... Type 翻译成直觉语言就是这里需要一个类型构造器你却给了一个普通类型。五种 Kind 错误的源码分类Unison 的 Kind 推断器将所有用户可见的 Kind 错误归纳为一个代数数据类型KindError定义在 parser-typechecker/src/Unison/KindInference/Error.hsKindError 构造子触发场景典型报错文案UnexpectedArgument把参数应用到了 Kind 为Type或Ability的东西上例如Nat NatNat doesnt expect an argument; however, it is applied to Nat.ArgumentMismatch普通类型应用非箭头的参数 Kind 不匹配Foo expects an argument of kind: Type - Type; however, it is applied to Bar which has kind: Type.即 fix4397 场景ArgumentMismatchArrow箭头类型-应用时参数 Kind 不匹配The arrow type (-) expects arguments of kind Type; however, it is applied to a which has kind: Type - Type.EffectListMismatch效果列表{...}中出现了 Kind 为Type而非Ability的东西An ability list must consist solely of abilities; however, this list contains Nat which has kind Type.ConstraintConflict其余无法归类的通用约束冲突Expected kind: ... / Given kind: ...CycleDetected类型参数的 Kind 被约束成无限循环例如T a T (a a)Cannot construct infinite kind从源码结构看KindError还有第六种形态SolveError对应求解阶段的内部错误如缺失内建类型MissingBuiltin、未知类型UnknownType一般不会出现在正常用户代码中。fix4397 用例命中的正是ArgumentMismatch分支Foo Bar是一个普通类型应用Foo的 Kind 约束要求参数具备Type - Type而Bar的实际 Kind 仅为Type。从约束求解看错误的诞生过程Unison 的 Kind 推断并非一次性完成而是遵循生成约束 → 求解约束两阶段流程对应源码模块parser-typechecker/src/Unison/KindInference/Generate.hs将类型与声明翻译为一组约束parser-typechecker/src/Unison/KindInference/Solve.hs对约束进行统一求解冲突时抛出ConstraintConflict。生成阶段类型应用如何变成约束以Foo Bar这类类型应用为例typeConstraintTree在处理Type.App abs arg时会生成两类约束见 Generate.hswellKindedAbs 约束IsArr absVar ...要求被应用者FooabsVar的 Kind 是一个箭头 KindType - Type其参数 Kind 记在absArgVar结果 Kind 为整个应用的 KindapplicationUnification 约束Unify ... absArgVar argVar要求Foo期望的参数 KindabsArgVar与实际传入参数Bar的 KindargVar统一。求解阶段当argVar被求解为TypeBar的实际 Kind而absArgVar已被Foo的字段f ()约束为Type - Type时统一失败便产生约束冲突。这一过程在 Solve.hs 中以ConstraintConflict的形式返回。改善阶段把内部冲突翻译成友好错误冲突产生后improveError会依据约束生成时的上下文ConstraintContext把通用的冲突翻译成更具体的错误形态。这个映射逻辑见 Error.hs 与上下文定义 Constraint/Context.hs上下文为AppArg普通类型应用→ArgumentMismatchfix4397 所走路径上下文为AppArrow箭头应用→ArgumentMismatchArrow上下文为EffectsList效果列表→EffectListMismatch上下文为AppAbs把参数应用到了非箭头 Kind 上→UnexpectedArgument。也就是说用户看到的每一种Kind mismatch arising from文案都对应着约束求解失败时约束是在哪种语法位置上生成的这一信息。fix4397 的报错能精确指向第 3 行unique type Baz Baz (Foo Bar)正是因为在生成阶段每个约束都携带了源码位置loc与来源上下文。组件级推断为什么Foo的 Kind 能跨声明确定从 unison-src/transcripts/idempotent/kind-inference.md 这一同目录下的姊妹转录可以看到Unison 的 Kind 推断按声明组件decl component进行相互引用的类型如Ping/Pong、Foo/Baz/Bar作为一个整体被求解一个声明中对类型参数的 Kind 约束可以传染给组件内的其他声明。例如unique type Ping a Ping Pong与unique type Pong Pong (Ping Optional)组成的组件中Pong对Ping的实例化把a的 Kind 推断为Type - Type因而Ping a合法。而 fix4397 的Baz Baz (Foo Bar)中Foo期望Type - Type、Bar却是Type组件级求解立刻暴露了这个矛盾。同族错误的更多实战样本为了帮助读者举一反三这里再给出几个与 fix4397 同属Kind mismatch arising from家族、出自仓库真实转录测试的典型场景。场景一参数被错误地应用到非箭头 Kind 上UnexpectedArgumentunique type T a T a (a Nat)Kind mismatch arising from 1 | unique type T a T a (a Nat) a doesnt expect an argument; however, it is applied to Nat.这里a被字段T a约束为普通类型Type却又在a Nat中被当作构造器使用属于对Type应用参数对应UnexpectedArgument分支。场景二类型注解中的 Kind 错误test : Nat Nat test 0Kind mismatch arising from 1 | test : Nat Nat Nat doesnt expect an argument; however, it is applied to Nat.Kind 推断同样作用于类型注解Nat本身是Type不能接收参数。场景三箭头应用与能力 KindArgumentMismatchArrow/EffectListMismatchtest : Optional - () test _ ()The arrow type (-) expects arguments of kind Type; however, it is applied to Optional which has kind: Type - Type.以及把普通类型放进能力列表test : {Nat} () test _ ()An ability list must consist solely of abilities; however, this list contains Nat which has kind Type. Abilities are of kind Ability.以上示例均收录于 kind-inference.md读者可直接对照原文复习。如何验证与复现转录测试机制fix4397.md属于 Unison 的幂等转录idempotent transcript测试体系存放在unison-src/transcripts/idempotent/目录。转录文件使用两类代码块标注 unison包含待处理的 Unison 源码:error后缀表示该代码块预期产生编译错误 ucm :added-by-ucm给出 ucmUnison Codebase Manager执行上述源码后追加到转录中的真实输出用于与后续实际运行结果比对。这套机制把预期报错文案固化在仓库中保证编译器未来重构时不会悄悄改变错误信息的格式或行号定位。运行方式见 scripts/proofs/transcripts.shstack build --fast unison-cli:exe:transcripts unison-cli-main:exe:unison --test --no-run-tests stack exec -- which transcripts随后按 development.markdown 中的说明执行转录工具即可。transcripts.sh还支持--hash、--force、--verbose、--dry-run等选项其校验哈希覆盖unison-src/**/*.md、unison-src/**/*.u以及全部 Haskell 源码**/*.hs即任何源码改动都会反映到转录产物的一致性检查中。总结fix4397.md用一段仅 7 行的源码完整覆盖了 Unison Kind 推断中跨组件高阶参数误用这一典型错误路径并锁定了Kind mismatch arising from这一错误家族的标准文案。通过本文可以掌握Kind 概念Unison 中只有Type与箭头 KindType - Type以及能力 KindAbilityFoo f Foo (f ())会把f约束为Type - Type错误解读抓住 expects an argument of kind 与 it is applied to ... which has kind 两个 Kind 的对比即可定位问题实现原理错误由约束生成 → 约束求解 → 按上下文改善文案三阶段产生相关源码集中在 Generate.hs、Solve.hs、Error.hs 与 Error/Pretty.hs验证方法借助转录测试体系复现与回归验证错误行为。掌握这套 Kind 错误体系不仅能让 Unison 用户快速修复类型定义中的高阶参数问题也能帮助编译器开发者理解 Kind 推断器内部约束上下文 → 错误形态的映射设计。赞分享编程语言编译器语言运行时开发工具【免费下载链接】unisonA friendly programming language from the future项目地址https://gitcode.com/gh_mirrors/un/unison点击查看免费下载相关推荐Unison 模式匹配中拼写错误构造器的错误诊断以 fix-3982 回归转录Transcript为例Unison 模式匹配中拼写错误构造器的错误诊断以 fix 3982 回归转录Transcript为例 导读 本文以 Unison 代码库中编号为 fix编程语言编译器语言运行时开发工具Unison 点号语法解析错误深度剖析从 fix-4536 转录测试看 UCM 错误报告机制Unison 点号语法解析错误深度剖析从 fix 4536 转录测试看 UCM 错误报告机制 本篇文章围绕 Unison 代码仓库中的回归测试转录文件 fix编程语言编译器语言运行时开发工具Unison 转录脚本错误诊断理解 missing-result-typed 与 :hide-all 块的报错机制Unison 转录脚本错误诊断理解 missing result typed 与 :hide all 块的报错机制 本篇指南以 Unison 语言仓库 uni编程语言编译器语言运行时开发工具上一篇【亲测免费】 Motif 开源项目教程下一篇2025全语言神经网络实战从零构建跨语言AI模型的终极指南创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考