寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「模式合一」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「抽象语法树」之「总集」之书。

。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「模块操作」之书。
寻观「编译器核心」之「编译步骤」之「总体过程」之「编译文件缓存工具」之书。

寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「命名环境术」之书。
寻观「编译器核心」之「编译数据」之「语言服务信息」之书。
寻观「编译器核心」之「编译数据」之「编译配置」之「编译期输出」之书。

寻观「编译器核心」之「编译数据」之「操作符」之「操作符数据结构」之书。

寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「检查后定义处理」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「类型检查基础」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「函数应用隐式参数合成」之书。

「解开源码绑定范围标注」乃化「表达式」而「表达式」合（「或可有」于「源码范围」）也。
「解开源码绑定范围标注」者会「式」而
  鉴「式」而
    有（「式节点」于（「源码绑定范围标注节点」于「范围」）于（（「列」【「原式」】）））则「原式」与（「可有」于
      「范围」
    ）
    或有「其他」则「式」与「可无」
也。

「记录源码绑定悬停」乃化（「或可有」于「源码范围」）而化「表达式」而「有」也。
「记录源码绑定悬停」者会「可能范围」而会「绑定类型」而
  鉴「可能范围」而
    有（「可有」于「范围」）则「记录悬停文字信息」于「范围」于（「悬停类型文字」于「绑定类型」）
    或有「可无」则「元」
也。

「单个抽象参数类型类型检查」乃化（化「命名环境」而化「表达式」而「表达式」）而化「命名环境」而化「表达式」而化「表达式」而
  （「列」于「表达式」）也。
「单个抽象参数类型类型检查」者会「类型类型检查」而会「境」而会「定义域」而会「值域」而
  （虑「查后定义域」者（「类型类型检查」于「境」于「定义域」）而
    虑「新绑定及新环境」者（「添加声明」于「境」于（「获取可能绑定名」于「值域」）于「查后定义域」）而
    虑「新环境」者「新绑定及新环境」中「一」而
    虑「新绑定」者「新绑定及新环境」中「零」而
    虑「开值域及范围」者「解开源码绑定范围标注」于（「式替换」于（「自由变量」于「新绑定」）于「值域」）而
    虑「无」者「记录源码绑定悬停」于（「开值域及范围」中「一」）于「查后定义域」而
    虑「查后值域」者（「类型类型检查」于「新环境」于（「开值域及范围」中「零」））而
    （「列」【「查后定义域」，（「进行抽象」于（「新绑定」）于「查后值域」）】））也。

「多个隐式抽象参数类型类型检查」乃化（化「命名环境」而化「表达式」而「表达式」）而化「命名环境」而化「整数」而化
  「表达式」而「表达式」也。
「多个隐式抽象参数类型类型检查」者会「类型类型检查」而会「境」而会「参数个数」而会「绑定值域」而
  递归虑「检查」其化「命名环境」而化「整数」而化「表达式」而「表达式」者
        会「当前境」而会「剩余个数」而会「当前绑定值域」而
          若（「等」于「剩余个数」于「零」）
          则
            「类型类型检查」于「当前境」于「当前绑定值域」
          否则
            （虑「新绑定及新环境」者「添加声明」于「当前境」
              于（「获取可能绑定名」于「当前绑定值域」）于
              「内建元类型式」而
              虑「新绑定」者「新绑定及新环境」中「零」而
              虑「开值域及范围」者「解开源码绑定范围标注」于（「式替换」
                于（「自由变量」于「新绑定」）于
                「当前绑定值域」）
              而
              虑「无」者「记录源码绑定悬停」于（「开值域及范围」中「一」）于「内建元类型式」而
              虑「查后开值域」者「检查」于（「新绑定及新环境」中「一」）
                于（「减」于「剩余个数」于「一」）于（「开值域及范围」中「零」）而
              「进行抽象」于「新绑定」于「查后开值域」
            ）
      而
      「检查」于「境」于「参数个数」于「绑定值域」
也。

「进行绑定对象类型检查」乃化「命名环境」而
  化「表达式」 「：对象（是一个绑定）：」而
  化「表达式」 「：对象类型（是一个绑定）：」而
  化「表达式」 「：绑定类型：」而
  「表达式」 「：检查过的对象（是一个绑定）：」
也。
「进行绑定对象类型检查」者会「境」而
  会「绑定物」而会「绑定物类型」而会「绑定类型」而
    （虑「绑名」者「获取可能绑定名」于「绑定物」而
      虑「新绑名及新境」者「添加声明」于「境」于「绑名」于「绑定类型」而
      虑「新绑名」者（「新绑名及新境」）中「零」而
      虑「绑体及范围」者「解开源码绑定范围标注」于（「式替换」
        于（「自由变量」于（「新绑名及新境」）中「零」）于（「绑定物」））
      而
      虑「无」者「记录源码绑定悬停」于（「绑体及范围」中「一」）于「绑定类型」而
      虑「绑体」者「绑体及范围」中「零」而
      虑「绑类体」者「式替换」于（「自由变量」于（「新绑名及新境」）中「零」）
        于（「绑定物类型」）而
      虑「后拉体」者（「读引用」于「进行对象类型检查引用」）于（「新绑名及新境」中「一」）于「绑体」于「绑类体」而
      「进行抽象」于「新绑名」于「后拉体」
    ）也。

「进行绑定对象类型合成」乃化「命名环境」而
  化「表达式」 「：对象（是一个绑定）：」而
  化「表达式」 「：绑定类型：」而
  「表达式」 「：对象类型（是一个绑定）：」
    合「表达式」 「：检查过的对象（是一个绑定）：」
也。
「进行绑定对象类型合成」者会「境」而
  会「绑定物」而会「绑定类型」而
    （虑「绑名」者「获取可能绑定名」于「绑定物」而
      虑「新绑名及新境」者「添加声明」于「境」于「绑名」于「绑定类型」而
      虑「新绑名」者（「新绑名及新境」）中「零」而
      虑「绑体及范围」者「解开源码绑定范围标注」于（「式替换」于（「自由变量」于「新绑名」）于「绑定物」）而
      虑「无」者「记录源码绑定悬停」于（「绑体及范围」中「一」）于「绑定类型」而
      虑「绑体」者「绑体及范围」中「零」而
      虑「体类及物」者（「读引用」于「进行对象类型合成引用」）
        于（「新绑名及新境」中「一」）于「绑体」而
      （「进行抽象」于「新绑名」于（「体类及物」中「零」））与
        （「进行抽象」于「新绑名」于（「体类及物」中「一」）））
也。

「进行对象类型合成」乃化「命名环境」而化「表达式」而「表达式」 「：类型：」
  合「表达式」 「：返回结果：」
也。
「进行对象类型合成」者会「境」而会「物」而
  鉴「物」而
    有（「式节点」于（「源码范围标注节点」于「范围」）于（（「列」【「源码物」】）））
    则（虑「类及物」者
          「进行对象类型合成」于
          「境」于「源码物」而
        虑「无」者「记录悬停文字信息」于「范围」
        于（「悬停类型文字」于（「类及物」中「零」））而「类及物」
    ）
    或有（「式节点」于（「内建节点」于「量」）于「罄」）则
      （（「内建物类型」于「量」））与「物」
    或有（「式节点」于（「整数节点」于「数」）于「罄」）则
      （「内建」于「内建类型整数」）与「物」
    或有（「式节点」于（「小数节点」于「数」于「整小部」）于「罄」）则
      （「内建」于「内建类型小数」）与「物」
    或有（「式节点」于（「字符串节点」于「串」）于「罄」）则
      （「内建」于「内建类型字符串」）与「物」
    或有（「自由变量」于「名」）则（鉴（「解析单个名称及物」于「境」于「名」）而
      有「可无」则（「发生事故」于『变量·』附「名」附『·未找到84，环境：』附（「命名环境表示」于「境」））
      或有（「可有」于（「未归一名类」与「名物」））则（ 「：TODO真的未归一吗？：」
        （「未归一名类」）与「名物」
      ））
    或有（「式节点」于（「文件定义引用节点」于「文件名」于「投影名」于「原先序数」）于「罄」）则
      （鉴（「文件定义引用类及物」于「境」于「文件名」于「投影名」）而有（「后类」与「后物」）则（「后类」）与「后物」）
    或有（「式节点」于（「拉姆达抽象带类型」于「拉形」）于（（「列」【「原抽象类型」，「拉参」】）））
    则（虑「抽象类型」者（「读引用」于「进行类型类型检查引用」）于「境」于「原抽象类型」而
        虑「绑名」者「获取可能绑定名」于「拉参」而
        虑「新绑名及新境」者「添加声明」于「境」于「绑名」于「抽象类型」而
        虑「新绑名」者（「新绑名及新境」）中「零」而
        虑「绑体及范围」者「解开源码绑定范围标注」于（「式替换」于（「自由变量」于「新绑名」）于「拉参」）而
        虑「无」者「记录源码绑定悬停」于（「绑体及范围」中「一」）于「抽象类型」而
        虑「绑体」者「绑体及范围」中「零」而
        虑「体类及物」者（「读引用」于「进行对象类型合成引用」）
        于（「新绑名及新境」中「一」）于「绑体」而
        鉴「拉形」而
          有「显式」则
            （「函数类型」于「抽象类型」于（「体类及物」中「零」））与
      （「式节点」于（「拉姆达抽象带类型」于「显式」）
        于（（「列」【「抽象类型」，（「进行抽象」于「新绑名」于（「体类及物」中「一」））】）））
          或有「隐式」则（虑「无」者「断言类型相等」于「抽象类型」于「内建元类型式」而
                          （「隐式类型函数类型」于「新绑名」于（「体类及物」中「零」））与
            （「式节点」于（「拉姆达抽象带类型」于「隐式」）
              于（（「列」【「内建元类型式」，（「进行抽象」于「新绑名」于（「体类及物」中「一」））】））））
          或有「其他」则「发生事故」于『拉姆达参数形式不匹配』
    ）
    或有（「式节点」于（「唯一构造器节点」于「序数」于「文件路径」于「构造器名」）于（（「列」【「构造器类」】）））
    则
      （「构造器类」）与「物」
    或有（「式节点」于（「元组构造节点」）于「元素们」）
    则（虑「结果」者（「从左折叠」授以「表达式」授以（（「列」于「表达式」）合（「列」于「表达式」）））
      于（会
        「元素」而会「已有」而
          虑「类物」者「进行对象类型合成」于「境」于「元素」而
          （「缀」于（「类物」中「零」）于（「已有」中「零」））与
          （「缀」于（「类物」中「一」）于（「已有」中「一」）））
          于（「罄」与「罄」）于「元素们」而
        （「式节点」于（「元组类型节点」）于（「反转」于（「结果」中「零」）））与（「式节点」
          于（「元组构造节点」）
          于（「反转」于（「结果」中「一」））））
    或有（「式节点」于「类型判断节点」于（（「列」【「判断类」，「判断式」】）））
    则（虑「后判断类」者（「读引用」于「进行类型类型检查引用」）于「境」于「判断类」而
        虑「后判断式」者（「读引用」于「进行对象类型检查引用」）于
        「境」于「判断式」于「后判断类」而「后判断类」与
      「后判断式」
    ）
    或有（「式节点」于「内联虑」于（（「列」【「定义式」，「尾式」】）））
    则（虑「后定义式类及物」者（鉴
          「定义式」而
        有（「式节点」于「函数调用」于「忽略项们」）则
          「进行函数应用头脊类型合成」于「境」于「定义式」
        或有（「式节点」于（「递归节点」）于（（「列」【「递归定义域」，「递归值域」】）））
        则（虑「后递归定义域」者（「读引用」于「进行类型类型检查引用」）于「境」于「递归定义域」而
            「后递归定义域」与（（「读引用」于「进行对象类型检查引用」）于「境」于「定义式」于「后递归定义域」））
        或有「其他定义式」则
          「进行对象类型合成」于「境」于「定义式」
      ）而
        虑「尾类及物」者「进行绑定对象类型合成」于「境」于「尾式」
          于（「后定义式类及物」中「零」）而
        虑「结果类」者「式替换」
          于（「后定义式类及物」中「一」）
          于（「尾类及物」中「零」）而「结果类」与（「式节点」于
            「内联虑带类型」
            于（「列」【「后定义式类及物」中「零」，「后定义式类及物」中「一」，「尾类及物」中「一」】）））
    或有（「式节点」于（「元组解构节点」于「序数」）于（（「列」【「元组」】）））
    则（虑「元组类及物」者
          「进行对象类型合成」于「境」于
          「元组」而
        鉴（（「元组类及物」中「零」））
      而
          有（「式节点」于（「元组类型节点」）于「类型们」）则
            （「第N个」于「序数」于「类型们」）与（「式节点」
              于（「元组解构节点」于「序数」）
                于（（「列」【（「元组类及物」中「一」）】）））
          或有「其他类型」则「发生事故」于
            『元组解构只能从明确元组类型合成，得到：』附（「表达式表示」于「其他类型」））
    或有（「式节点」于（「爻分支节点」）于（「列」【「爻式」，「阳式」，「阴式」】））
    则（虑「后爻式」者（「读引用」于「进行对象类型检查引用」）于「境」于「爻式」
      于（「内建」于「内建类型爻」）
        而
        「尝试运行」于（会「无」而
          虑「阳类及物」者「进行对象类型合成」于「境」于「阳式」而
          虑「后阴式」者（「读引用」于「进行对象类型检查引用」）于「境」于「阴式」
            于（「阳类及物」中「零」）
          而
          （「阳类及物」中「零」）与（「式节点」于（「爻分支节点」）
              于（「列」【「后爻式」，「阳类及物」中「一」，「后阴式」】）））
              于（会「阳支异常」而
                虑「阴类及物」者「进行对象类型合成」于「境」于「阴式」而
                虑「后阳式」者（「读引用」于「进行对象类型检查引用」）于「境」于「阳式」
                  于（「阴类及物」中「零」）
                而
                （「阴类及物」中「零」）与（「式节点」于（「爻分支节点」）
                    于（「列」【「后爻式」，「后阳式」，「阴类及物」中「一」】））））
    或有（「式节点」于（「模式匹配」）于（「缀」于「分析式」于「分支们」））则（鉴（「进行对象类型合成」于「境」于
          「分析式」
      ）而
      有（「分析类」与「分析后式」）则（鉴「分支们」而
        有「罄」则「发生事故」于『模式匹配没有分支，无法合成返回类型』
        或有（「缀」于「首分支」于「后分支们」）则（鉴（（「读引用」于「模式匹配分支类型合成引用」）于「境」于「首分支」于
              「分析类」
          ）
          而
          有（「返回类」与「后首分支」）则（虑「后后分支们」者（「态射」授以「表达式」授以「表达式」）于「后分支们」
            于（会「支」而（「读引用」于「检查模式匹配分支引用」）于「境」于「支」于「返回类」于「分析类」）而
                                            「返回类」与（「式节点」
                                                于（「模式匹配」）
                                                于（（「缀」授以「表达式」）于「分析后式」
                                                于（（「缀」授以「表达式」）于「后首分支」于「后后分支们」）））））））
    或有（「式节点」于「顺序执行节点」于（（「列」【「式甲」，「式乙」】）））
    则（虑「后式甲类及式」者
          「进行对象类型合成」于
          「境」于「式甲」而
        虑「后式乙类及式」者「进行对象类型合成」于「境」于「式乙」而
        （「后式乙类及式」中「零」）与（「式节点」于
          「顺序执行节点」
          于（（「列」【（「后式甲类及式」中「一」），（「后式乙类及式」中「一」）】））））
    或有（「式节点」于「函数调用」于「忽略项们」）则
      （「进行函数应用头脊类型合成」于「境」于「物」）
    或有「其他」则
      「发生事故」于『无法合成对象类型，请添加类型标注或改走检查模式：』附（「表达式表示」于「物」）
也。

「写引用」于「进行对象类型合成引用」于「进行对象类型合成」。

「对象子类型检查」乃化「命名环境」而化「表达式」 「：对象：」而
  化「表达式」 「：对象的合成类型：」而
  化「表达式」 「：对象的检查类型：」而
  「表达式」 「：检查过的对象：」
也。
「对象子类型检查」者会「境」而会「原物」而会「子类」而会「父类」而
  虑「无」者（「详细调试打印行」于（会「无」而『[D]正在进行对象子类型检查，对象：』附（「表达式表示」于「原物」）附
        『，合成类型：』附（「表达式表示」于「子类」）附『，检查类型：』附（「表达式表示」于「父类」）））而
  虑「无」者「断言类型相等」于「子类」于「父类」而
  「原物」
也。
