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

。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「模块操作」之书。
寻观「编译器核心」之「编译数据」之「编译配置」之「编译期输出」之书。

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

寻观「编译器核心」之「编译数据」之「操作符」之「操作符数据结构」之书。
寻观「拓展库」之「顺序标识符」之「顺序标识符」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「模式匹配类型检查」之书。

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

「检查隐式头或子类型」乃化「命名环境」而化「表达式」而化「表达式」而化「表达式」而「表达式」也。
「检查隐式头或子类型」者会「境」而会「物」而会「物类」而会「类」而
  鉴（「物类」）而
    有（「式节点」于（「隐式派类型节点」于「忽略参数个数」）于（（「列」【「忽略值域」】）））则（鉴「类」而
      有（「式节点」于（「隐式派类型节点」于「忽略期望参数个数」）于（（「列」【「忽略期望值域」】）））则
        「对象子类型检查」于「境」于「物」于「物类」于「类」
      或有「其他期望类」则
        「进行函数应用头脊类型检查」于「境」于「物」于「类」
    ）
    或有「其他物类」则
      「对象子类型检查」于「境」于「物」于「物类」于「类」
也。

「： |-  M : A ：」
「进行对象类型检查」乃化「命名环境」而化「表达式」而化「表达式」而「表达式」也。
「进行对象类型检查」者会「境」而会「未归一物」而会「未归一类」而
  虑「无」者（「详细调试打印行」于（会「无」而『[D]正在进行对象类型检查：』附（「表达式表示」于「未归一物」）附
        『 <= 』附（「表达式表示」于「未归一类」）））而
  虑「类」者（「未归一类」）而
  虑「原物」者「未归一物」而 「：我们真的要归一化吗？如果 (\x. M) N 的语义真的和 [N/x]M 的语义一样吗？：」
  「尝试运行」于（会「无」而
    虑「结果」者（「表达式」也
      （鉴「原物」而
        有（「式节点」于（「源码范围标注节点」于「范围」）于（（「列」【「源码物」】）））
        则（虑「后物」者
              「进行对象类型检查」于
              「境」于「源码物」于
              「类」而
            虑「无」者「记录悬停文字信息」于「范围」
            于（「悬停类型文字」于「类」）而「后物」
        ）
        或有（「式节点」于（「内建节点」于「量」）于「罄」）则
          （「对象子类型检查」于「境」于「原物」于（「内建物类型」于「量」）于「类」）
        或有（「自由变量」于「名」）则（鉴（「解析单个名称及物」于「境」于「名」）而
          有「可无」则（「发生事故」于『变量·』附「名」附『·未找到47，环境：』附（「命名环境表示」于「境」））
          或有「可有」于（「未归一名类」与「名物」）则
            （虑「名类」者（「未归一名类」）而「检查隐式头或子类型」于「境」于「名物」于「名类」于「类」））
        或有（「式节点」于（「拉姆达抽象」于「拉形」）于（（「列」【「拉参」】）））则（鉴（「类」）而
          有
          （「式节点」于「箭头类型节点」于（「缀」于「定义域」于（「缀」于「次类型」于「余类型们」）））
          则（虑「值域」者（鉴「余类型们」而
              有「罄」则「次类型」
              或有「非空余类型们」则「式节点」于「箭头类型节点」
                于（「缀」于「次类型」于「余类型们」））而
              鉴「拉形」而
                有「显式」则「式节点」于（「拉姆达抽象带类型」于「显式」）
                  于（（「列」【「定义域」，（「进行绑定对象类型检查」于「境」于「拉参」
                    于（「进行无名抽象」于「值域」）于
                    「定义域」）】））
                或有「隐式」则「发生事故」于『隐式拉姆达不能检查为箭头类型』
                或有「其他」则「发生事故」于『拉姆达参数形式不匹配』
          ）
          或有（「式节点」于（「隐式派类型节点」于「参数个数」）于（（「列」【「原绑定值域」】）））
          则（虑「已有名们」者（「缀」授以「字符串」）于『』
            于（（「附加」授以「字符串」）于（「命名环境获取所有名称」于「境」）于（「读取式自由变量」于「原物」））
              而
              虑「新隐名及剩余类」者「打开首隐式派类型」于「类」于「已有名们」而
              虑「新隐名」者「新隐名及剩余类」中「零」而
              虑「剩余类」者「新隐名及剩余类」中「一」而
              虑「新境」者「添加声明不改变名」于『隐式参数』于「境」于「新隐名」于
              「内建元类型式」而
              鉴「拉形」而
                有「隐式」则（虑「拉体及范围」者「解开源码绑定范围标注」
                  于（「式替换」于（「自由变量」于「新隐名」）于「拉参」）而
                              虑「无」者「记录源码绑定悬停」
                              于（「拉体及范围」中「一」）于
                              「内建元类型式」而虑「拉体」者「拉体及范围」中「零」而
                                                虑「后拉体」者「进行对象类型检查」于「新境」于「拉体」于「剩余类」而
                                                「式节点」于（「拉姆达抽象带类型」于「隐式」）
                                                  于（（「列」【「内建元类型式」，（「进行抽象」于「新隐名」于「后拉体」）】）））
                或有「显式」则（虑「后体」者「进行对象类型检查」于「新境」于「原物」于「剩余类」
                                而
                                「式节点」于（「拉姆达抽象带类型」于「隐式」）
                                  于（（「列」【「内建元类型式」，（「进行抽象」于「新隐名」于「后体」）】）））
                或有「其他」则「发生事故」于『拉姆达参数形式不匹配』
          ）
          或有「其他类」则「发生事故」于『拉姆达只能检查为明确的函数类型：』附（「表达式表示」于「类」））
        或有（「式节点」于（「拉姆达抽象带类型」于「拉形」）于（（「列」【「原抽象类型」，「拉参」】）））
        则
          「：TODO：应该有很多可能性：」
        （虑「抽象类型」者「进行类型类型检查」于「境」于「原抽象类型」而
          鉴「类」而
            有
            （「式节点」于「箭头类型节点」于（「缀」于「定义域」于（「缀」于「次类型」于「余类型们」）））
            则（虑「值域」者（鉴「余类型们」而
                有「罄」则「次类型」
                或有「非空余类型们」则「式节点」于「箭头类型节点」
                  于（「缀」于「次类型」于「余类型们」））而
                虑「无」者（「断言类型相等」于「定义域」于「抽象类型」）而
                鉴「拉形」而
                  有「显式」则「式节点」于（「拉姆达抽象带类型」于「显式」）
                    于（（「列」【「定义域」，（「进行绑定对象类型检查」于「境」于「拉参」
                      于（「进行无名抽象」于「值域」）于
                      「抽象类型」）】））
                  或有「其他」则「发生事故」于『带类型拉姆达只能检查为显式箭头』
            ）
            或有「其他」则「发生事故」于『未有173』
        ）
        或有（「式节点」于（「爻分支节点」）于（「列」【「爻式」，「阳式」，「阴式」】））
        则（虑「后爻式」者（「进行对象类型检查」于「境」于「爻式」于（「内建」于（「内建类型爻」）））而
            虑「后阳式」者（「进行对象类型检查」于「境」于「阳式」于（「类」））而
            虑「后阴式」者（「进行对象类型检查」于「境」于「阴式」于（「类」））而
            「式节点」于（「爻分支节点」）于（「列」【「后爻式」，「后阳式」，「后阴式」】））
        或有（「式节点」于「函数调用」于「忽略项们」）则
          （「进行函数应用头脊类型检查」于「境」于「原物」于「类」）
        或有（「式节点」于「外部调用节点」于（（「列」【「名」，「参」】）））
        则（虑「函数名」
          者（鉴「名」而
            有
            （「式节点」于（「字符串节点」于「串」）于「罄」）则「串」
            或有「其他」则（「字符串」也「发生事故」于『外部调用第一个参数必须是字符串』））
            而
            （虑「确认是自由变量」者
                （化「表达式」而
                    「字符串」也会「式」而
                      虑「无标注式」者鉴「式」
                  而
                        有（「式节点」于（「源码范围标注节点」于「忽略范围」）于（（「列」【「源码式」】）））则
                          「源码式」
                        或有「其他式」则「其他式」而鉴「无标注式」而
                          有（「自由变量」于「串」）则「串」
                          或有「其他」则「发生事故」于『必须是直接变量』
                ）
              而
              递归虑「分析参数」其化
                  「表达式」而（「列」于「字符串」）者（会「式」而鉴
                    「式」而
                      有（「式节点」于（「源码范围标注节点」于「忽略范围」）于（（「列」【「源码式」】）））则
                        「分析参数」于「源码式」
                      或有（「自由变量」于「串」）则（鉴「式」而
                        有（「式节点」于（「内建节点」于「内建有元」）于「罄」）则
                          「罄」
                        或有「其他」则（（「列」【「串」】）））
                      或有（「式节点」于（「内建节点」于「内建有元」）于「罄」）则
                        「罄」
                      或有（「式节点」于（「元组构造节点」）于「元素们」）则
                        （（「态射」）于「元素们」于「确认是自由变量」）
                      或有「其他」则「发生事故」于
                        『必须是变量，元，或者绑定变量的与』
                  ）
                  而
                  虑「后参数」者「分析参数」于「参」而（「式节点」
                      于（「解析后外部调用节点带类型」于「函数名」）
                      于（（「附加」授以「表达式」）于（（（「列」于「表达式」）也（（「列」【「类」】））））
                      于（（「态射」）于「后参数」于「自由变量」）））））
        或有（「式节点」于（「整数节点」于「数」）于「罄」）
        则（虑「无」者（「断言类型相等」于（「内建」于「内建类型整数」）于「类」）而
            「式节点」
            于（「整数节点」于「数」）于「罄」
        ）
        或有（「式节点」于（「小数节点」于「数」于「整小部」）于「罄」）
        则（虑「无」者（「断言类型相等」于（「内建」于「内建类型小数」）于「类」）而
            「式节点」
            于（「小数节点」于「数」于「整小部」）于
            「罄」
        ）
        或有（「式节点」于（「字符串节点」于「串」）于「罄」）
        则（虑「无」者（「断言类型相等」于（「内建」于「内建类型字符串」）于「类」）而
            「式节点」
            于（「字符串节点」于「串」）于「罄」
        ）
        或有（「式节点」于（「文件定义引用节点」于「文件名」于「投影名」于「序数」）于「罄」）则（鉴（「进行对象类型合成」于
              「境」于「原物」
          ）而
          有（「后类」与「后物」）则
            「检查隐式头或子类型」于「境」于「后物」于「后类」于「类」
        ）
        或有（「式节点」于「内联虑」于（（「列」【「定义式」，「尾式」】）））
        则（虑「后定义式类及物」者（鉴
              「定义式」而
            有（「式节点」于「函数调用」于「忽略项们」）则
              「进行函数应用头脊类型合成」于「境」于「定义式」
            或有（「式节点」于（「递归节点」）于（（「列」【「递归定义域」，「递归值域」】）））
            则（虑「后递归定义域」者「进行类型类型检查」于「境」于「递归定义域」而
                「后递归定义域」
              与（「进行对象类型检查」于「境」于「定义式」于「后递归定义域」））
            或有「其他定义式」则
              「进行对象类型合成」于「境」于「定义式」
          ）而
            虑「后尾式」者「进行绑定对象类型检查」于「境」于「尾式」
              于（「进行无名抽象」于「类」）
              于（「后定义式类及物」中「零」）而（「式节点」于
                「内联虑带类型」
                于（「列」【「后定义式类及物」中「零」，「后定义式类及物」中「一」，「后尾式」】）））
        或有（「式节点」于「内联虑带类型」于（「列」【「定义类」，「定义式」，「尾式」】））
        则（虑「后定义类」者「进行类型类型检查」于「境」于「定义类」而
            虑「后定义式」者「进行对象类型检查」于「境」于「定义式」于「后定义类」而
            虑「后尾式」者「进行绑定对象类型检查」于「境」于「尾式」
            于（「进行无名抽象」于「类」）于（「后定义类」）
            而
            （「式节点」于「内联虑带类型」于（「列」【「后定义类」，「后定义式」，「后尾式」】）））
        或有（「式节点」于（「递归节点」）于（（「列」【「递归定义域」，「递归值域」】）））
        则（虑「后定义域」者「进行类型类型检查」于「境」于「递归定义域」而
            虑「无」者「断言类型相等」于「后定义域」于「类」而
            虑「后值域」者「进行绑定对象类型检查」于「境」于「递归值域」
            于（「进行无名抽象」于「后定义域」）于
            「后定义域」而
            （「式节点」于（「递归节点」）于（（「列」【「后定义域」，「后值域」】））））
        或有（「式节点」于（「模式匹配」）于（「缀」于「分析式」于「分支们」））则（鉴（「进行对象类型合成」于「境」于
              「分析式」
          ）而
          有（「分析类」与「分析后式」）则（虑「后分支们」者（「态射」授以「表达式」授以「表达式」）于「分支们」
            于（会「支」而「检查模式匹配分支」于「境」于「支」于「类」于「分析类」）而
                                            （「式节点」于（「模式匹配」）
                                                于（（「缀」授以「表达式」）于「分析后式」于「后分支们」））））
        或有（「式节点」于「类型判断节点」于（（「列」【「判断类」，「判断式」】）））
        则（虑「后判断类」者「进行类型类型检查」于「境」于「判断类」而
            虑「无」者「断言类型相等」于「后判断类」于「类」而
            虑「后判断式」者「进行对象类型检查」于「境」于「判断式」于「后判断类」而
            「后判断式」
        ）
        或有（「式节点」于（「元组构造节点」）于「元素们」）则（鉴「类」而
          有（「式节点」于（「元组类型节点」）于「类型们」）则（若（「不等于」
                于（「长度」于「元素们」）于（「长度」于「类型们」））
          则
            （「发生事故」于『元组元素个数和元组类型个数不匹配』）
          否则
            （「式节点」于（「元组构造节点」）于（（「态射」授以（「表达式」合「表达式」）授以「表达式」）
              于（（「拉链合并」授以「表达式」授以「表达式」）于「元素们」于「类型们」）
              于（遇
              「表达式」合「表达式」者「元素及类型」而
    「进行对象类型检查」于「境」于（「元素及类型」中「零」）于（「元素及类型」中「一」）））））
          或有「其他」则（虑「后元素类及物」者（（「态射」授以「表达式」授以（「表达式」合「表达式」））于
                「元素们」于（会「元素」而「进行对象类型合成」于「境」于「元素」））而
                          虑「后式」者
                            （「式节点」于（「元组构造节点」）
                            于（（「态射」）于「后元素类及物」
                            于（会「类及物」而（「二对子取一」授以「表达式」授以「表达式」）于「类及物」）））
                          而
                          「对象子类型检查」于「境」于「后式」
                          于（「式节点」
                          于（「元组类型节点」）于（「列」于
                          「表达式」也（「态射」）于「后元素类及物」
                          于（会「类及物」而（「二对子取零」授以「表达式」授以「表达式」）于「类及物」）））于「类」
          ））
        或有（「式节点」于（「元组解构节点」于「序数」）于（（「列」【「元组」】）））
        则（虑「后对子类及式」者
              「进行对象类型合成」于
              「境」于「元组」而
            （递归虑「获取类型」其化
              「整数」而化「表达式」而
                「表达式」者（会「数」而会
                  「式」而鉴「式」而
                    有（「式节点」于（「元组类型节点」）于「类型们」）则
                      （「第N个」于「数」于「类型们」）
                    或有「其他类型」则「发生事故」于
                      『元组解构只能从明确元组类型合成，得到：』附（「表达式表示」于「其他类型」））
                  而
                  虑「目标类型」者「获取类型」于「序数」
                    于（「后对子类及式」中「零」）而「对象子类型检查」于「境」
                    于（「式节点」于（「元组解构节点」于「序数」）于（（「列」【（「后对子类及式」中「一」）】）））于
                    「目标类型」于「类」
            ））
        或有（「式节点」于「顺序执行节点」于（（「列」【「式甲」，「式乙」】）））
        则（虑「后式甲类及式」者
              「进行对象类型合成」于
              「境」于「式甲」而
            虑「后式乙」者「进行对象类型检查」于「境」于「式乙」于「类」
            而
            （「式节点」于「顺序执行节点」
              于（（「列」【（「后式甲类及式」中「一」），（「后式乙」）】））））
        或有（「式节点」于（「唯一构造器节点」于「序数」于「文件路径」于「构造器名」）
            于（（「列」【「构造器类」】）））
            则
              （「检查隐式头或子类型」于「境」于「原物」于「构造器类」于「类」）
        或有（「式节点」于（「文件引用节点」于「新文件名」）于「罄」）则
            （「发生事故」于『文件引用不再是一等对象，不能直接进行对象类型检查：』附「新文件名」）
        或有（「式节点」于（「解析后外部调用节点带类型」于「串」）于（「缀」于「返回类」于「参」））
        则（虑「无」者「断言类型相等」于「返回类」于「类」而
            （「式节点」于（「解析后外部调用节点带类型」于「串」）于（「缀」于「返回类」于「参」）））
        或有（「式节点」于（「空缺」）于「罄」）则
            （「发生事故」于『空缺式暂时不支持类型合成，也不支持类型检查』）
        或有（「式节点」于「箭头类型节点」于「派参」）
        则（虑「后物」者「进行类型类型检查」于「境」于「原物」而
            「对象子类型检查」于「境」于「后物」
              于（「内建元类型式」）于「类」
        ）
        或有（「式节点」于（「隐式派类型节点」于「忽略参数个数」）于「派参」）
        则（虑「后物」者「进行类型类型检查」于
            「境」于「原物」而
            「对象子类型检查」于「境」于「后物」
            于（「内建元类型式」）于「类」
        ）
        或有（「式节点」于（「元组类型节点」）于「参」）
        则（虑「后物」者「进行类型类型检查」于「境」于「原物」而
            「对象子类型检查」于「境」于「后物」
            于（「内建元类型式」）于「类」
        ）
        或有「其他物」则（鉴「类」而
          有（「式节点」于（「内建节点」于（「内建类型元类型」））于「罄」）则
              （虑「后物」者「进行类型类型检查」于「境」于「原物」而「后物」）
          或有「其他」则「发生事故」于
              『库/编译器核心/编译步骤/类型检查/类型检查。豫:180 （对象类型检查）检查类型尚未实现：』
              附（「表达式表示」于「原物」）附『 <= 』附（「表达式表示」于「类」）
              附『|「：换行：」    环境：：|』附（（「命名环境表示」于「境」））附『|时』
        ）））而
              虑「无」者（「详细调试打印行」于（会「无」而『[D]完成对象类型检查：』附（「表达式表示」于「未归一物」）
                附
                『 <= 』附（「表达式表示」于「未归一类」）附『 结果：』附（「表达式表示」于「结果」）））而
              「结果」
  ）于（会「异常」而
    「发生事故」于（「异常」附『「：换行：」=======》》》》 在检查(2)表达式|』附（「表达式表示」于「原物」）
          附『|「：换行：」    拥有类型|』附（「表达式表示」于「类」）
          附『|「：换行：」    即：|』附（「表达式表示」于（「类」））附『|时』
          附『|「：换行：」    环境：：|』附（「间合」于『，』于（「命名环境获取所有名称」于「境」））附
            『|时』
    ））也。

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