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

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

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

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

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

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

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

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

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

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

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

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

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

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