feat: add Check.lean

library/Init/Lean/Meta.lean

@@ -9,6 +9,7 @@ import Init.Lean.Meta.WHNF
 import Init.Lean.Meta.InferType
 import Init.Lean.Meta.FunInfo
 import Init.Lean.Meta.LevelDefEq
+import Init.Lean.Meta.ExprDefEq
 
 namespace Lean
 namespace Meta
@@ -61,5 +62,12 @@ getFunInfoAux whnf fn
 def getFunInfoNArgs (fn : Expr) (nargs : Nat) : MetaM FunInfo :=
 getFunInfoNArgsAux whnf fn nargs
 
+/-- Throws exception if `e` is not type correct. -/
+def check (e : Expr) : MetaM Unit :=
+checkAux whnf isDefEq e
+
+def isTypeCorrect (e : Expr) : MetaM Bool :=
+isTypeCorrectAux whnf isDefEq e
+
 end Meta
 end Lean

library/Init/Lean/Meta/Basic.lean

@@ -242,6 +242,9 @@ do lctx ← getLCtx;
    | some d => pure d
    | none   => throwEx $ Exception.unknownFVar fvarId
 
+def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
+getLocalDecl fvar.fvarId!
+
 def getMVarDecl (mvarId : Name) : MetaM MetavarDecl :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
@@ -344,7 +347,7 @@ resettingTypeClassCache $
 | i, k =>
   if h : i < fvars.size then do
     let fvar := fvars.get ⟨i, h⟩;
-    decl ← getLocalDecl fvar.fvarId!;
+    decl ← getFVarLocalDecl fvar;
     c?   ← isClassQuick decl.type;
     match c? with
     | LOption.none   => withNewLocalInstances (i+1) k

library/Init/Lean/Meta/Check.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.InferType
+
+/-
+This is not the Kernel type checker, but an auxiliary method for checking
+whether terms produced by tactics and `isDefEq` are type correct.
+-/
+
+namespace Lean
+namespace Meta
+
+@[specialize] private def ensureType
+    (whnf : Expr → MetaM Expr)
+    (e : Expr) : MetaM Unit :=
+do getLevelAux whnf (inferTypeAux whnf) e;
+   pure ()
+
+@[specialize] private def checkLambdaLet
+    (whnf    : Expr → MetaM Expr)
+    (isDefEq : Expr → Expr → MetaM Bool)
+    (check   : Expr → MetaM Unit)
+    (e : Expr) : MetaM Unit :=
+lambdaTelescope whnf e $ fun xs b => do
+  xs.forM $ fun x => do {
+    xDecl ← getFVarLocalDecl x;
+    match xDecl with
+    | LocalDecl.cdecl _ _ _ t _ => do
+      ensureType whnf t;
+      check t
+    | LocalDecl.ldecl _ _ _ t v => do
+      ensureType whnf t;
+      check t;
+      vType ← inferTypeAux whnf v;
+      unlessM (isDefEq t vType) $ throwEx $ Exception.letTypeMismatch x.fvarId!;
+      check v
+  };
+  check b
+
+@[specialize] private def checkForall
+    (whnf    : Expr → MetaM Expr)
+    (check   : Expr → MetaM Unit)
+    (e : Expr) : MetaM Unit :=
+forallTelescope whnf e $ fun xs b => do
+  xs.forM $ fun x => do {
+    xDecl ← getFVarLocalDecl x;
+    ensureType whnf xDecl.type;
+    check xDecl.type
+  };
+  ensureType whnf b;
+  check b
+
+@[specialize] private def checkConstant
+    (c : Name) (lvls : List Level) : MetaM Unit :=
+do env ← getEnv;
+   match env.find c with
+   | none       => throwEx $ Exception.unknownConst c
+   | some cinfo => unless (lvls.length != cinfo.lparams.length) $ throwEx $ Exception.incorrectNumOfLevels c lvls
+
+@[specialize] private def checkApp
+    (whnf    : Expr → MetaM Expr)
+    (isDefEq : Expr → Expr → MetaM Bool)
+    (check   : Expr → MetaM Unit)
+    (f a : Expr) : MetaM Unit :=
+do check f;
+   check a;
+   fType ← inferTypeAux whnf f;
+   fType ← whnf fType;
+   match fType with
+   | Expr.forallE _ d _ _ => do
+     aType ← inferTypeAux whnf a;
+     unlessM (isDefEq d aType) $ throwEx $ Exception.appTypeMismatch f a
+   | _ => unless fType.isForall $ throwEx $ Exception.functionExpected fType #[a]
+
+@[specialize] private partial def checkAuxAux
+    (whnf    : Expr → MetaM Expr)
+    (isDefEq : Expr → Expr → MetaM Bool)
+    : Expr → MetaM Unit
+| e@(Expr.forallE _ _ _ _) => checkForall whnf checkAuxAux e
+| e@(Expr.lam _ _ _ _)     => checkLambdaLet whnf isDefEq checkAuxAux e
+| e@(Expr.letE _ _ _ _ _)  => checkLambdaLet whnf isDefEq checkAuxAux e
+| Expr.const c lvls _      => checkConstant c lvls
+| Expr.app f a _           => checkApp whnf isDefEq checkAuxAux f a
+| Expr.mdata _ e _         => checkAuxAux e
+| Expr.proj _ _ e _        => checkAuxAux e
+| _                        => pure ()
+
+@[specialize] def checkAux
+    (whnf    : Expr → MetaM Expr)
+    (isDefEq : Expr → Expr → MetaM Bool)
+    (e : Expr) : MetaM Unit :=
+usingTransparency TransparencyMode.all $
+  checkAuxAux whnf isDefEq e
+
+@[specialize] def isTypeCorrectAux
+    (whnf    : Expr → MetaM Expr)
+    (isDefEq : Expr → Expr → MetaM Bool)
+    (e : Expr) : MetaM Bool :=
+catch
+  (do checkAux whnf isDefEq e; pure true)
+  (fun _ => pure false)
+
+end Meta
+end Lean

library/Init/Lean/Meta/Exception.lean

@@ -28,6 +28,8 @@ inductive Exception
 | invalidProjection    (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext)
 | revertFailure        (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext)
 | readOnlyMVar         (mvarId : Name) (ctx : ExceptionContext)
+| letTypeMismatch      (fvarId : Name) (ctx : ExceptionContext)
+| appTypeMismatch      (f a : Expr) (ctx : ExceptionContext)
 | bug                  (b : Bug) (ctx : ExceptionContext)
 | other                (msg : String)
 
@@ -47,6 +49,8 @@ def toStr : Exception → String
 | invalidProjection _ _ _ _     => "invalid projection"
 | revertFailure _ _ _           => "revert failure"
 | readOnlyMVar _ _              => "try to assign read only metavariable"
+| letTypeMismatch _ _           => "type mismatch at let-expression"
+| appTypeMismatch _ _ _         => "application type mismatch"
 | bug _ _                       => "bug"
 | other s                       => s
 

library/Init/Lean/Meta/ExprDefEq.lean

@@ -8,6 +8,7 @@ import Init.Lean.Meta.WHNF
 import Init.Lean.Meta.InferType
 import Init.Lean.Meta.FunInfo
 import Init.Lean.Meta.LevelDefEq
+import Init.Lean.Meta.Check
 
 namespace Lean
 namespace Meta
@@ -156,7 +157,7 @@ else
 | i, k =>
   if h : i < fvars.size then do
     let fvar := fvars.get ⟨i, h⟩;
-    fvarDecl ← getLocalDecl fvar.fvarId!;
+    fvarDecl ← getFVarLocalDecl fvar;
     let fvarType := fvarDecl.type;
     let d₂       := ds₂.get! i;
     condM (isDefEq fvarType d₂)
@@ -606,14 +607,6 @@ private def simpAssignmentArg (arg : Expr) : MetaM Expr :=
 do arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg;
    simpAssignmentArgAux arg
 
-/- TODO: type check `e`, move to different file -/
-def isTypeCorrect
-    (whnf              : Expr → MetaM Expr)
-    (isDefEq           : Expr → Expr → MetaM Bool)
-    (synthesizePending : Expr → MetaM Bool)
-    (e : Expr) : MetaM Bool :=
-pure true
-
 @[specialize] private partial def processAssignmentAux
     (whnf              : Expr → MetaM Expr)
     (isDefEq           : Expr → Expr → MetaM Bool)
@@ -670,7 +663,7 @@ pure true
         if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
           /- We need to type check `v` because abstraction using `mkLambda` may have produced
              a type incorrect term. See discussion at A2 -/
-          condM (isTypeCorrect whnf isDefEq synthesizePending v)
+          condM (isTypeCorrectAux whnf isDefEq v)
             (finalize ())
             (useFOApprox ())
         else

library/Init/Lean/Meta/FunInfo.lean

@@ -62,7 +62,7 @@ checkFunInfoCache fn maxArgs? $ do
     pinfo ← fvars.size.foldM
       (fun (i : Nat) (pinfo : Array ParamInfo) => do
         let fvar := fvars.get! i;
-        decl ← getLocalDecl fvar.fvarId!;
+        decl ← getFVarLocalDecl fvar;
         prop ← isPropAux whnf decl.type;
         let backDeps := collectDeps fvars decl.type;
         let pinfo    := updateHasFwdDeps pinfo backDeps;

library/Init/Lean/Meta/InferType.lean

@@ -79,7 +79,7 @@ do let failed : Unit → MetaM Expr := fun _ => throwEx $ Exception.invalidProje
            | _                    => failed ()
      | _ => failed ()
 
-@[specialize] private def getLevel
+@[specialize] def getLevelAux
     (whnf      : Expr → MetaM Expr)
     (inferType : Expr → MetaM Expr)
     (type : Expr) : MetaM Level :=
@@ -101,11 +101,11 @@ do typeType ← inferType type;
     (inferType : Expr → MetaM Expr)
     (e : Expr) : MetaM Expr :=
 forallTelescope whnf e $ fun xs e => do
-  lvl  ← getLevel whnf inferType e;
+  lvl  ← getLevelAux whnf inferType e;
   lvl  ← xs.foldrM
     (fun x lvl => do
       xType    ← inferType x;
-      xTypeLvl ← getLevel whnf inferType xType;
+      xTypeLvl ← getLevelAux whnf inferType xType;
       pure $ mkLevelIMax xTypeLvl lvl)
     lvl;
   pure $ mkSort lvl.normalize