Cache in env extension

src/Lean/Elab/MutualInductive.lean

@@ -67,6 +67,12 @@ register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
     This option may be deleted in the future after we improve the validator"
 }
 
+register_builtin_option debug.inductiveCheckPositivity : Bool := {
+  defValue := true
+  descr    := "Run elaborator checks for positivity of inductive types. Disabling this can be \
+    useful for debugging the elaborator or when stress-testing the kernel with invalid inductive types."
+}
+
 /-- View of a constructor. Only `ref`, `modifiers`, `declName`, and `declId` are required by the mutual inductive elaborator itself. -/
 structure CtorView where
   /-- Syntax for the whole constructor. -/
@@ -779,6 +785,84 @@ where
         /- Underconstrained, but not an error. -/
         pure ()
 
+
+structure PositivityExtState where
+  map : PHashMap (Name × Nat) (Except Exception Unit) := {}
+  deriving Inhabited
+
+/- Simple local extension for caching/memoization -/
+builtin_initialize positivityExt : EnvExtension PositivityExtState ←
+  -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`.
+  -- The resulting state can still be accessed on the generated declarations using `findStateAsync`;
+  -- see below
+  registerEnvExtension (pure {}) (asyncMode := .local)
+
+private def positivityExt.getOrSet (key : Name × Nat) (act : CoreM Unit) := do
+  match (positivityExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := key.1) (← getEnv)).map.find? key with
+  | some r =>
+    liftExcept r
+  | none =>
+    let r ← observing act
+    modifyEnv fun env =>
+      positivityExt.modifyState env (fun s => { s with map := s.map.insert key r })
+    liftExcept r
+
+/--
+Throws an exception unless the `i`th parameter of the inductive type only occurrs in
+positive position.
+-/
+partial def isIndParamPositive (info : InductiveVal) (i : Nat) : CoreM Unit := do
+  -- Consistently use the info of the first inductive in the group
+  if info.name != info.all[0]! then
+    return (← isIndParamPositive (← getConstInfoInduct info.all[0]!) i)
+
+  positivityExt.getOrSet (info.name, i) do MetaM.run' do
+    trace[Elab.inductive] "checking positivity of #{i+1} in {.ofConstName info.name}"
+    for indName in info.all do
+      let info ← getConstInfoInduct indName
+      for con in info.ctors do
+        let con ← getConstInfoCtor con
+        forallTelescopeReducing con.type fun xs _t => do
+          -- TODO: Check for occurrences in the indices of t?
+          let params := xs[0...info.numParams]
+          let p := params[i]!.fvarId!
+          for conArg in xs[info.numParams...*] do
+            forallTelescopeReducing (← inferType conArg) fun conArgArgs conArgRes => do
+              for conArgArg in conArgArgs do
+                if (← inferType conArgArg).hasAnyFVar (· == p) then
+                  throwError "Non-positive occurrence of parameter `{mkFVar p}` in type of {.ofConstName con.name}"
+              let conArgRes ← whnf conArgRes
+              if conArgRes.hasAnyFVar (· == p) then
+                  conArgRes.withApp fun fn args => do
+                    if fn == mkFVar p then
+                      for arg in args do
+                        if arg.hasAnyFVar (· == p) then
+                          throwError "Non-positive occurrence of parameter `{mkFVar p}` in type of {.ofConstName con.name}, \
+                            in application of the parameter itself."
+                    else if let some fn := fn.constName? then
+                      if info.all.contains fn then
+                        -- Recursive occurrence of an inductive type of this group.
+                        -- Params must match by construction but check indices
+                        for idxArg in args[info.numParams...*] do
+                          if idxArg.hasAnyFVar (· == p) then
+                            throwError "Non-positive occurrence of parameter `{mkFVar p}` in type of {.ofConstName con.name}, \
+                              in index of {.ofConstName fn}"
+                      else if (← isInductive fn) then
+                        let info' ← getConstInfoInduct fn
+                        for i in 0...info'.numParams, pe in args[0...info'.numParams] do
+                          if pe.hasAnyFVar (· == p) then
+                            try
+                              isIndParamPositive info' i
+                            catch _ =>
+                              throwError "Non-positive occurrence of parameter `{mkFVar p}` in type of {.ofConstName con.name}, \
+                                in parameter #{i+1} of {.ofConstName fn}"
+                      else
+                        throwError "Non-positive occurrence of parameter `{mkFVar p}` in type of {.ofConstName con.name}, \
+                          cannot nest through {.ofConstName fn}"
+                    else
+                      throwError "Non-positive occurrence of parameter `{mkFVar p}` in type of {.ofConstName con.name}, \
+                        cannot nest through {fn}"
+
 /-- Checks the universe constraints for each constructor. -/
 private def checkResultingUniverses (views : Array InductiveView) (elabs' : Array InductiveElabStep2)
     (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
@@ -803,6 +887,84 @@ private def checkResultingUniverses (views : Array InductiveView) (elabs' : Arra
               which is not less than or equal to the inductive type's resulting universe level{indentD u}"
             withCtorRef views ctor.name <| throwError msg
 
+private partial def checkPositivity (views : Array InductiveView) (indFVars : Array Expr) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
+  unless debug.inductiveCheckPositivity.get (← getOptions) do return
+  for h : i in *...indTypes.length do
+    let view := views[i]!
+    let indType := indTypes[i]
+    for ctor in indType.ctors do
+      withCtorRef views ctor.name do
+        forallTelescopeReducing ctor.type fun xs retTy  => do
+          let params := xs[*...numParams]
+          for x in xs, i in *...xs.size do
+            prependError m!"In argument #{i+1} of constructor {ctor.name}:" do
+              go params (← inferType x)
+          isValidIndApp retTy
+where
+  hasIndOcc (t : Expr) : Option Expr :=
+    indFVars.find? (fun indFVar => t.hasAnyFVar (· == indFVar.fvarId!))
+
+  -- cf. is_valid_ind_app in inductive.cpp
+  isValidIndApp (e : Expr) : TermElabM Unit := do
+    e.withApp fun fn args => do
+      if let some i := indFVars.findIdx? (fun indFVar => fn == indFVar) then
+        -- The parameters are already checked in `checkParamOccs`
+        for arg in args[numParams...*] do
+          if let some indFVar := hasIndOcc arg then
+            throwError "Invalid occurrence of inductive type `{indFVar}`: The indices in the \
+              occurrence may not mention the inductive type itself."
+      else
+        throwError "Non-positive occurrence of the inductive type in constructor argument:{inlineExpr e}"
+
+  -- cf. check_positivity in inductive.cpp
+  go (params : Array Expr) (t : Expr) : TermElabM Unit := do
+    let t ← instantiateMVars (← whnf t)
+    if let some indFVar := hasIndOcc t then
+      -- Argument has recursive occurrences
+      forallTelescopeReducing t fun xs t => do
+        for x in xs do
+          if let some indFVar := hasIndOcc (← inferType x) then
+            throwError "Non-positive occurrence of inductive type `{indFVar}`"
+        let t ← whnf t
+        t.withApp fun fn args => do
+          if let some fn := fn.constName? then
+            -- Check for valid nested induction
+            unless (← isInductive fn) do
+              throwError "Non-positive occurrence of inductive type `{indFVar}`: \
+                Nested occurrences can only occur in inductive types, not in `{.ofConstName fn}`."
+            let info ← getConstInfoInduct fn
+            unless args.size = info.numParams + info.numIndices do
+              throwError "Non-positive occurrence of inductive type `{indFVar}`: \
+                Invalid occurrence of {indFVar} in unsaturated call of {.ofConstName fn}."
+            for i in 0...info.numParams, pe in args[0...info.numParams] do
+              if let some indFVar := hasIndOcc pe then
+                try isIndParamPositive info i
+                catch e =>
+                  let msg := m!"Invalid occurrence of inductive type `{indFVar}`, parameter #{i+1} of \
+                    `{.ofConstName fn}` is not positive."
+                  let msg := msg ++ .note m!"That parameter is not positive:{indentD e.toMessageData}"
+                  throwError msg
+                -- Here, we allow lambdas in parameters. The kernel actually substitutes these while
+                -- doing the transformation for nested inductives, and may reduce these lambdas away.
+                -- We approximate this behavior for now. See `lean/run/nestedInductiveUniverse.lean`
+                -- for an example
+                lambdaTelescope pe fun _xs pe => do
+                  -- We do not consider the domains of the lambda-bound variables
+                  -- as negative occurrences, as they will be reduced away.
+                  go params pe
+
+              -- The kernel admits no local variables in the parameters (#1964)
+              -- so check for any fvar that isn't one of the indFVars or params
+              if let some e := pe.find? (fun e => e.isFVar && !indFVars.contains e && !params.contains e) then
+                throwError "Nested inductive datatype parameters cannot contain local variable `{e}`."
+            for ie in args[info.numParams...args.size] do
+              if let some indFVar := hasIndOcc ie then
+                throwError "Invalid occurrence of inductive type `{indFVar}`, must not occur in \
+                  index of `{.ofConstName fn}`"
+          else
+            isValidIndApp t
+
+
 private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
   indTypes.forM fun indType => do
     indType.type.collectFVars
@@ -911,6 +1073,8 @@ private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep
             propagateUniversesToConstructors numParams indTypes
             levelMVarToParam indTypes none
         checkResultingUniverses views elabs' numParams indTypes
+        unless isUnsafe do
+          checkPositivity views indFVars numParams indTypes
         elabs'.forM fun elab' => elab'.finalizeTermElab
         let usedLevelNames := collectLevelParamsInInductive indTypes
         match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with

tests/lean/2125.lean

@@ -4,6 +4,22 @@ noncomputable def f (α : Type) : Bool :=
   Nonempty α
 
 -- The following inductive is unsound:
+
 inductive C : Bool → Type
   -- Must be rejected because `C` occurs inside an index.
   | c : C (f (C false))
+
+-- Same, in arguments of the constructors
+
+inductive D : Bool → Type
+  -- Must be rejected because `D` occurs inside an index.
+  | c : D (f (D false)) → D true
+
+-- Same, but hidden behind nested induction
+
+inductive Nest (G : Bool → Type) where
+  | mk : G (f (G false)) → Nest G
+
+inductive E : Bool → Type where
+  -- Must be rejected because `D` occurs inside an index.
+  | c : Nest E → E true

tests/lean/2125.lean.expected.out

@@ -1 +1,8 @@
-2125.lean:7:0-9:23: error: (kernel) invalid return type for 'C.c'
+2125.lean:10:2-10:23: error: Invalid occurrence of inductive type `C`: The indices in the occurrence may not mention the inductive type itself.
+2125.lean:16:2-16:32: error: In argument #1 of constructor D.c:
+  Invalid occurrence of inductive type `D`: The indices in the occurrence may not mention the inductive type itself.
+2125.lean:25:2-25:23: error: In argument #1 of constructor E.c:
+  Invalid occurrence of inductive type `E`, parameter #1 of `Nest` is not positive.
+  
+  Note: That parameter is not positive:
+    Non-positive occurrence of parameter `G` in type of Nest.mk, in application of the parameter itself.

tests/lean/run/issue6371.lean

@@ -0,0 +1,10 @@
+set_option inductive.autoPromoteIndices false in
+inductive Foo (A : Type) : (A -> A) → Type where
+
+/--
+error: In argument #1 of constructor Bar.bar:
+  Invalid occurrence of inductive type `Bar`, must not occur in index of `Foo`
+-/
+#guard_msgs in
+inductive Bar where
+  | bar : Foo Bar (fun x => x) → Bar

tests/lean/run/issue8960.lean

@@ -0,0 +1,32 @@
+import Std.Data.HashMap
+
+open Std
+
+/--
+error: (kernel) application type mismatch
+  DHashMap.Raw.WF inner
+argument has type
+  _nested.Std.DHashMap.Raw_3
+but function has type
+  (DHashMap.Raw String fun x => Maze) → Prop
+-/
+#guard_msgs in
+structure Maze where
+  description : String
+  passages : HashMap String Maze
+
+structure TestThingy (α : Type u) where
+  data : List α
+  invariant : data ≠ []
+
+/--
+error: In argument #2 of constructor Maze'.mk:
+  Invalid occurrence of inductive type `Maze'`, parameter #1 of `TestThingy` is not positive.
+  ⏎
+  Note: That parameter is not positive:
+    Non-positive occurrence of parameter `α` in type of TestThingy.mk
+-/
+#guard_msgs in
+structure Maze' where
+  description : String
+  passages : TestThingy Maze'

tests/lean/run/issue9018.lean

@@ -69,24 +69,22 @@ inductive BaseFoo (t : Type u -> Type v) (α : Type u)
 | some (v : t α)
 
 /--
-error: (kernel) application type mismatch
-  Eq.trans (congrArg (Nat.add 1) (Foo3._sizeOf_3_eq v))
-    (Eq.symm
-      (@BaseFoo.some.sizeOf_spec Box Foo3 (fun a => @Box._sizeOf_inst a (instSizeOfDefault a)) Foo3._sizeOf_inst v))
-argument has type
-  1 + sizeOf v = sizeOf (@BaseFoo.some Box Foo3 v)
-but function has type
-  Nat.add 1 (sizeOf v) = sizeOf (@BaseFoo.some Box Foo3 v) →
-    Nat.add 1 (Foo3._sizeOf_3 v) = sizeOf (@BaseFoo.some Box Foo3 v)
+error: In argument #1 of constructor Foo3.mk:
+  Invalid occurrence of inductive type `Foo3`, parameter #2 of `BaseFoo` is not positive.
+  ⏎
+  Note: That parameter is not positive:
+    Non-positive occurrence of parameter `α` in type of BaseFoo.some, cannot nest through t
 -/
 #guard_msgs(pass trace, all) in
 structure Foo3 where
   raw : BaseFoo Box Foo3
 
 /--
-error: maximum recursion depth has been reached
-use `set_option maxRecDepth <num>` to increase limit
-use `set_option diagnostics true` to get diagnostic information
+error: In argument #1 of constructor Foo4.mk:
+  Invalid occurrence of inductive type `Foo4`, parameter #2 of `BaseFoo` is not positive.
+  ⏎
+  Note: That parameter is not positive:
+    Non-positive occurrence of parameter `α` in type of BaseFoo.some, cannot nest through t
 -/
 #guard_msgs(pass trace, all) in
 structure Foo4 where

tests/lean/run/nestedInductivePositivity.lean

@@ -0,0 +1,144 @@
+import Lean
+/-!
+This test exercises the elaborator's positivity check for inductive data types, and related
+checks around nested induction.
+-/
+
+/--
+error: In argument #1 of constructor Bad.mk:
+  Non-positive occurrence of inductive type `Bad`
+-/
+#guard_msgs in
+inductive Bad where
+  | mk : (Bad → Bad) → Bad
+
+/--
+error: In argument #1 of constructor Bad1.mk:
+  Non-positive occurrence of inductive type `Bad2`
+-/
+#guard_msgs in
+mutual
+inductive Bad1 where
+  | mk : (Bad2 → Bad2) → Bad1
+inductive Bad2 where
+  | mk : (Bad1 → Bad1) → Bad2
+end
+
+inductive Ok1 where
+  | mk : id Ok1 → Ok1
+
+
+axiom T : Type → Type
+
+/--
+error: In argument #1 of constructor Bad3.mk:
+  Non-positive occurrence of inductive type `Bad3`: Nested occurrences can only occur in inductive types, not in `T`.
+-/
+#guard_msgs in
+inductive Bad3 where
+  | mk : T Bad3 → Bad3
+
+inductive Ok2 where
+  | mk : List Ok2 → Ok2
+
+/--
+error: Mismatched inductive type parameter in
+  Bad4 (α × α)
+The provided argument
+  α × α
+is not definitionally equal to the expected parameter
+  α
+
+Note: The value of parameter 'α' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+-/
+#guard_msgs in
+inductive Bad4 (α : Type) : Type where
+  | mk : Bad4 (α × α) → Bad4 α
+
+inductive Nest5 (f : Nat → Type) where
+  | mk : f 5 → Nest5 f
+
+inductive Ok5 : Nat → Type where
+  | mk : Nest5 Ok5 → Ok5 n
+
+inductive Nest6 (f : Nat → Type) where
+  | mk : f n → Nest6 f
+
+inductive Ok6 : Nat → Type where
+  | mk : Nest6 Ok6 → Ok6 n
+
+inductive Nest7 (n : Nat) (f : Nat → Type) where
+  | mk : f n → Nest7 n f
+
+/--
+error: In argument #2 of constructor Bad7.mk:
+  Nested inductive datatype parameters cannot contain local variable `n`.
+-/
+#guard_msgs in
+inductive Bad7 : Nat → Type where
+  | mk : Nest7 n Bad7 → Bad7 n
+
+inductive Good7 (n : Nat) : Nat → Type where
+  | mk : Nest7 n (Good7 n) → Good7 n n
+
+inductive Nest8 (α : Type) : (β : Type) → Type  where
+  | mk : α → Nest8 α Bool
+
+inductive Ok8 : Type where
+  | mk : Nest8 Ok8 Unit → Ok8
+
+/--
+error: In argument #1 of constructor Bad8.mk:
+  Invalid occurrence of inductive type `Bad8`, must not occur in index of `Nest8`
+-/
+#guard_msgs in
+inductive Bad8 : Type where
+  | mk : Nest8 Unit Bad8 → Bad8
+
+inductive Nest9 (α : Type) : Type  where
+  | mk : (α → α) → Nest9 α
+
+/--
+error: In argument #1 of constructor Bad9.mk:
+  Invalid occurrence of inductive type `Bad9`, parameter #1 of `Nest9` is not positive.
+  ⏎
+  Note: That parameter is not positive:
+    Non-positive occurrence of parameter `α` in type of Nest9.mk
+-/
+#guard_msgs in
+inductive Bad9 where
+  | mk : Nest9 Bad9 → Bad9
+
+
+inductive Nest10 (α : Type) : Type  where
+  | mk : α  → Nest10 α
+
+inductive Ok10 where
+  | mk : Nest10 (Bool -> Ok10) → Ok10
+
+inductive Nest11 (α : Bool → Type) : Type  where
+  | mk : α true → Nest11 α
+
+inductive Ok11  : Bool → Type where
+  | mk : Nest11 Ok11 → Ok11 true
+
+/-
+The following code tried to check if positivity checking blows up exponentially
+with nested types, but it still seems fast compared to other things happening, so
+this test does not actually blow up as desired.
+We still memoize the queries, as can manually be checked using `set_option trace.Elab.inductive
+true`.
+-/
+
+-- set_option trace.Elab.inductive true
+-- set_option debug.inductiveCheckPositivity false
+
+inductive Ok12a α where | mk : α → Ok12a α
+inductive Ok12b α where | mk : Ok12a α → Ok12a α → Ok12a α → Ok12a α → Ok12a α → Ok12a α →  Ok12b α
+inductive Ok12c α where | mk : Ok12b α → Ok12b α → Ok12b α → Ok12b α → Ok12b α → Ok12b α →  Ok12c α
+inductive Ok12d α where | mk : Ok12c α → Ok12c α → Ok12c α → Ok12c α → Ok12c α → Ok12c α →  Ok12d α
+inductive Ok12e α where | mk : Ok12d α → Ok12d α → Ok12d α → Ok12d α → Ok12d α → Ok12d α →  Ok12e α
+inductive Ok12f α where | mk : Ok12e α → Ok12e α → Ok12e α → Ok12e α → Ok12e α → Ok12e α →  Ok12f α
+
+inductive Ok12 where | mk : Ok12c Ok12 → Ok12
+-- inductive Ok12 where | mk : Ok12f Ok12 → Ok12