Fix #1: Bugfix of checking function types

Signed-off-by: anqurvanillapy <[email protected]>

lyzh/concrete/elab.py

@@ -99,12 +99,12 @@ def infer(self, e: cst.Expr) -> typing.Tuple[ast.Term, ast.Term]:
                 #  Γ , A : type ⊢ M : type
                 # -------------------------- function type introduction rule
                 # Γ ⊢ π (A: type) → M : type
-                p_typ, _ = self.infer(p.type)  # 参数类型的类型一定是 Univ, 所以忽略了
+                p_typ = self.check(p.type, ast.Univ())  # 参数类型的类型一定是 Univ, 但我们仍需要确保这一点
                 inferred_p = core.Param[ast.Term](p.name, p_typ)
-                # 在参数 p 的保护下, 推导 body 的类型.
-                b_tm, b_ty = self.guarded_infer(inferred_p, b)
+                # 在参数 p 的保护下, 检查 body 的类型.
+                b_tm = self.guarded_check(inferred_p, b, ast.Univ())
                 # 重新拼回去组成一个 ast.FnType.
-                return ast.FnType(inferred_p, b_tm), b_ty
+                return ast.FnType(inferred_p, b_tm), ast.Univ()
             case cst.App(_, f, x):
                 # Γ ⊢ f : π (x : A) → B    x : A
                 # ------------------------------ function elimination rule
@@ -130,7 +130,7 @@ def infer(self, e: cst.Expr) -> typing.Tuple[ast.Term, ast.Term]:
         raise AssertionError("impossible")
 
     def guarded_check(
-        self, p: core.Param[ast.Term], e: cst.Expr, typ: ast.Term
+            self, p: core.Param[ast.Term], e: cst.Expr, typ: ast.Term
     ) -> ast.Term:
         """在 p 的保护下 (即将 p 加入到本地变量中, 检查完毕后删除), 检查表达式 e 的类型是否为 typ."""
         self.locals[p.name.id] = p.type
@@ -142,7 +142,7 @@ def guarded_check(
         return ret
 
     def guarded_infer(
-        self, p: core.Param[ast.Term], e: cst.Expr
+            self, p: core.Param[ast.Term], e: cst.Expr
     ) -> typing.Tuple[ast.Term, ast.Term]:
         """在 p 的保护下 (即将 p 加入到本地变量中, 推导完毕后删除), 推导表达式 e 的类型."""
         self.locals[p.name.id] = p.type