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

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

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

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

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

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

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

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