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

。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「模块操作」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「检查后定义处理」之书。
寻观「编译器核心」之「编译数据」之「编译配置」之「编译期输出」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「命名环境术」之书。
寻观「编译器核心」之「编译数据」之「语言服务信息」之书。

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

寻观「编译器核心」之「编译步骤」之「类型检查」之「类型检查工具」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「类型检查基础」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「函数应用隐式参数合成」之书。
寻观「编译器核心」之「编译步骤」之「总体过程」之「编译文件缓存工具」之书。

「元类型式」者「内建元类型式」也。

「类型式是元类型」乃化「命名环境」而化「表达式」而「爻」也。
「类型式是元类型」者会「境」而会「式」而
  鉴「式」而
    有
      （「式节点」于（「内建节点」于（「内建类型元类型」））于「罄」）则
        「阳」
    或有（「自由变量」于「变名」）则（鉴（「解析单个名称及物」于「境」于「变名」）而
      有（「可有」于（「变名类」与「忽略变名物」））则「类型式是元类型」于「境」于「变名类」
      或有「其他」则「阴」
    ）
    或有「其他」则「阴」
也。

「确认类型构造器」乃化「表达式」而化「表达式」而「表达式」合「表达式」也。
「确认类型构造器」者会「类」而会「物」而
  鉴「物」而
    有（「式节点」于（「唯一构造器节点」于「忽略序数」于「忽略文件路径」于「忽略构造器名」）
      于（（「列」【「忽略构造器类」】）））则
      「类」与「物」
    或有「其他」则
      「发生事故」于『类型应用的头必须是构造器：』附（「表达式表示」于「其他」）附『，类型：』附（「表达式表示」于
        「类」
      ）
也。

「解析类型构造器头」乃化「命名环境」而化「表达式」而「表达式」合「表达式」也。
「解析类型构造器头」者会「境」而会「头」而
  鉴「头」而
    有（「式节点」于（「源码范围标注节点」于「范围」）于（（「列」【「源码头」】）））
    则（虑「头类及物」者
          「解析类型构造器头」于
          「境」于「源码头」而
        虑「无」者「记录悬停文字信息」于「范围」
        于（「悬停类型文字」于（「头类及物」中「零」））而
        「头类及物」
    ）
    或有（「自由变量」于「名」）则（鉴（「解析单个名称及物」于「境」于「名」）而
      有（「可有」于（「头类」与「头物」））则
        「确认类型构造器」于「头类」于「头物」
      或有「可无」则
        「发生事故」于『类型构造器未找到：』附「名」
    ）
    或有（「式节点」于（「文件定义引用节点」于「文件名」于「定义名」于「忽略序数」）于「罄」）则（鉴（「文件定义引用类及物」于
          「境」于「文件名」于「定义名」
      ）而
      有（「头类」与「头物」）则「确认类型构造器」于「头类」于「头物」
    ）
    或有（「式节点」于（「唯一构造器节点」于「序数」于「文件路径」于「构造器名」）于（（「列」【「构造器类」】）））
    则
      「构造器类」与「头」
    或有「其他」则
      「发生事故」于『类型应用的头必须是可解析的构造器：』附（「表达式表示」于「其他」）
也。

「进行类型构造器应用检查」乃化「命名环境」而化「表达式」而「表达式」也。
「进行类型构造器应用检查」者会「境」而会「类」而
  虑「头及脊」者「收集函数调用头脊」于「类」而
  虑「头」者「头及脊」中「零」而
  虑「脊」者「头及脊」中「一」而
  虑「头类及物」者「解析类型构造器头」于「境」于「头」而
  递归虑「处理」其化「表达式」而化「表达式」而化（「列」于（「参数形式」合「表达式」））而「表达式」者
        （会「当前类」而会「当前物」而会「剩余脊」而
          鉴「剩余脊」而
            有「罄」则（若（「类型式是元类型」于「境」于「当前类」）
            则
              「展开透明定义引用」于「境」于「当前物」
            否则
              「发生事故」于『类型构造器没有完全应用到类型：』附（「表达式表示」于「当前物」）附
                『，剩余类型：』附（「表达式表示」于「当前类」））
            或有（「缀」于（「形」与「参数」）于「后脊」）则（鉴「当前类」而
              有（「式节点」于「箭头类型节点」于（「缀」于「定义域」于（「缀」于「次类型」于「余类型们」）））
              则（鉴「形」而
                有「显式」则（若（「类型式是元类型」于「境」于「定义域」）
                则
                  （虑「后参数」者（「读引用」于「进行类型类型检查引用」）于「境」于「参数」而
                    虑「后物」者「添加函数调用参数」于「当前物」于
                      「显式」于「后参数」而虑「后类」者（鉴「余类型们」而
                        有「罄」则「次类型」
                        或有「非空余类型们」则「式节点」于「箭头类型节点」
                          于（「缀」于「次类型」于「余类型们」））
                                            而
                                            「处理」于「后类」于「后物」于「后脊」
                  ）
                否则
                  「发生事故」于『类型构造器参数必须是类型，但定义域是：』附（「表达式表示」于「定义域」））
                或有「隐式」则「发生事故」于『箭头类型构造器不接受隐式类型参数』
                或有「其他」则「发生事故」于『类型构造器参数形式不匹配』
              ）
              或有（「式节点」于（「隐式派类型节点」于「参数个数」）于（（「列」【「原绑定值域」】）））
              则（鉴「形」而
                有「隐式」则（虑「后参数」者（「读引用」于「进行类型类型检查引用」）于「境」于「参数」而
                              虑「后类」者「应用首隐式类型参数」于「当前类」于「后参数」而
                              虑「后物」者
                                「添加函数调用参数」于「当前物」于
                                「隐式」于「后参数」而「处理」于
                                「后类」于「后物」于「后脊」
                ）
                或有「显式」则「发生事故」于『隐式类型构造器参数必须显式写成隐式调用』
                或有「其他」则「发生事故」于『隐式类型构造器参数形式不匹配』
              ）
              或有「其他类」则
                  「发生事故」于『类型构造器参数过多，当前类型不是函数：』附（「表达式表示」于「其他类」）））
      而
      「处理」于（「头类及物」中「零」）于（「头类及物」中「一」）于「脊」
也。

「：|-  A : Type ：」
「进行类型类型检查」乃化「命名环境」而化「表达式」而「表达式」也。
「进行类型类型检查」者会「境」而会「类」而
  虑「无」者「详细调试打印行」于（会「无」而『[D]正在检查(1)表达式|』附（「表达式表示」于「类」）附『|是一个类型』）而
  「尝试运行」于（会「无」而
    虑「结果」者（「表达式」也
      鉴「类」而
        有（「式节点」于（「源码范围标注节点」于「范围」）于（（「列」【「源码类」】）））
        则（虑「后类」者
              「进行类型类型检查」于
              「境」于「源码类」而
            虑「无」者「记录悬停文字信息」于「范围」
            于（「悬停类型文字」于「后类」）而「后类」
        ）
        或有（「式节点」于「箭头类型节点」于「类型们」）
        则（虑「无」者（鉴「类型们」而
            有（「缀」于「忽略定义域」于（「缀」于「忽略值域」于「忽略余类型们」））则「元」
            或有「其他」则「发生事故」授以「有」于
              『箭头类型节点必须至少包含一个定义域和一个值域』
          ）而
            「式节点」于「箭头类型节点」
              于（（「态射」）于「类型们」于（会「类型」而「进行类型类型检查」于「境」于「类型」）））
        或有（「式节点」于（「隐式派类型节点」于「参数个数」）于（（「列」【「值域」】）））
        则（虑「查后值域」者
              「多个隐式抽象参数类型类型检查」于
              「进行类型类型检查」于
              「境」于
              「参数个数」于
              「值域」而「式节点」
              于（「隐式派类型节点」于「参数个数」）
              于（（「列」【「查后值域」】）））
        或有（「式节点」于（「拉姆达抽象带类型」于「形式」）于（（「列」【「定义域」，「值域」】）））
        则（虑「查后定义域」者（「进行类型类型检查」于「境」于「定义域」）而
            虑「无」者（「断言类型相等」于「查后定义域」于「元类型式」）而
            虑「新绑定及新环境」者（「添加声明」于「境」于（「获取可能绑定名」于「值域」）于「查后定义域」）而
            虑「新环境」者「新绑定及新环境」中「一」而
            虑「新绑定」者「新绑定及新环境」中「零」而
            虑「开值域及范围」者「解开源码绑定范围标注」于（「式替换」于（「自由变量」于「新绑定」）于「值域」）而
            虑「无」者「记录源码绑定悬停」于（「开值域及范围」中「一」）于「查后定义域」而
            虑「查后值域」者（「进行类型类型检查」于「新环境」于（「开值域及范围」中「零」））而
            「式节点」于（「拉姆达抽象带类型」于「形式」）于（（「列」【「查后定义域」，（「进行抽象」于「新绑定」于「查后值域」）】）））
        或有（「式节点」于「函数调用」于「忽略项们」）则
          （「进行类型构造器应用检查」于「境」于「类」）
        或有（「式节点」于（「结构投影」于「名」）于「参」）则
          「发生事故」于『名称解析后的类型中仍存在结构投影：』附「名」附『，参数：』附（「表达式列表示」于「参」）
        或有（「式节点」于（「文件定义引用节点」于「文件名」于「定义名」于「忽略序数」）于「罄」）则（鉴（「文件定义引用类及物」于
              「境」于「文件名」于「定义名」
          ）而
          有（「定义类」与「定义物」）则
            若（「类型式是元类型」于「境」于「定义类」）
            则
              「展开透明定义引用」于「境」于「定义物」
            否则
              「发生事故」于（「表达式表示」于「类」）附『，类型：』附（「表达式表示」于「定义类」）附
              『，不是一个类型！』
        ）
        或有（「自由变量」于「名」）则（鉴（「解析单个名称及物」于「境」于「名」）而
          有「可无」则（「发生事故」于『变量·』附「名」附『·未找到65，环境：』附（「命名环境表示」于「境」））
          或有（「可有」于（「名类」与「名物」））则（（「表达式」也
                鉴「名类」而 「：如果：」
                  有（「自由变量」于「类型名」）则（若「类型式是元类型」于「境」于「名类」则
                      「展开透明定义引用」于「境」于「名物」
                  否则
                    「发生事故」
                      于（「表达式表示」于「类」）附
                      『，类型：』附（「表达式表示」于「名类」）附
                      『，不是一个类型！』
                  ）
                  或有「其他」则（若「类型式是元类型」于「境」于「名类」则「名物」否则「发生事故」
                      于（「表达式表示」于「类」）附『，类型：』附（「表达式表示」于「名类」）附
                      『，不是一个类型！』
                  ））））

        或有（「式节点」于「待定节点」于「罄」）则
          「发生事故」于『待定类型节点不能进入类型类型检查；请给出明确类型』
        或有（「式节点」于（「内建节点」于（「内建类型元类型」））于「罄」）则
          （「式节点」于（「内建节点」于（「内建类型元类型」））于「罄」）
        或有（「式节点」于（「元组类型节点」）于「类们」）则（「式节点」
          于（「元组类型节点」）于（（「态射」）于
          「类们」于（会「待检查类」而「进行类型类型检查」于「境」于「待检查类」）））
        或有（「式节点」于（「唯一构造器节点」于「序数」于「文件路径」于「构造器名」）
          于（（「列」【「构造器类」】）））
          则（虑「后构造器类」者「进行类型类型检查」于「境」于「构造器类」而
              「式节点」于（「唯一构造器节点」于「序数」于「文件路径」于「构造器名」）
              于（（「列」【「后构造器类」】）））
        或有（「式节点」于（「内建节点」于「量」）于「罄」）则（鉴「量」而
          有「内建类型字符串」则「类」
          或有「内建类型整数」则「类」
          或有「内建类型小数」则「类」
          或有「内建类型动态分类值」则「类」
          或有「内建类型有」则「类」
          或有「内建类型爻」则「类」
          或有「内建类型元类型」则「类」
          或有「其他」则「发生事故」于『不是内建类型』附（「表达式表示」于「类」））
        或有「其他」则「发生事故」于『（类型类型检查）类型尚未实现：』附（「表达式表示」于「类」））而
    「结果」
  ）于（会「异常」而
    「发生事故」于（「异常」附『「：换行：」在检查(1)表达式|』附（「表达式表示」于「类」）附『|是一个类型时』））
也。

「写引用」于「进行类型类型检查引用」于「进行类型类型检查」。
