feat: invoke mkSizeOfInstances from structure and inductive commands

src/Lean/Elab/Inductive.lean

@@ -7,6 +7,7 @@ import Lean.Util.ReplaceLevel
 import Lean.Util.ReplaceExpr
 import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
+import Lean.Meta.SizeOf
 import Lean.Elab.Command
 import Lean.Elab.CollectFVars
 import Lean.Elab.DefView
@@ -496,6 +497,7 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
   let ref := view0.ref
   runTermElabM view0.declName fun vars => withRef ref do
     mkInductiveDecl vars views
+    mkSizeOfInstances view0.declName  
   applyDerivingHandlers views
 
 end Lean.Elab.Command

src/Lean/Elab/Structure.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Parser.Command
 import Lean.Meta.Closure
+import Lean.Meta.SizeOf
 import Lean.Elab.Command
 import Lean.Elab.DeclModifiers
 import Lean.Elab.DeclUtil
@@ -569,6 +570,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
                 ctor              := ctor
                 fields            := fields
               }
+            mkSizeOfInstances declName  
             return declName
   derivingClassViews.forM fun view => view.applyHandlers #[declName]
 

src/Lean/Meta/SizeOf.lean

@@ -157,10 +157,10 @@ def generateSizeOfInstance (opts : Options) : Bool :=
   opts.get `genSizeOf true
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
-  if (← getEnv).contains ``SizeOf && generateSizeOfInstance (← getOptions) then
-    let fns ← mkSizeOfFns typeName
+  if (← getEnv).contains ``SizeOf && generateSizeOfInstance (← getOptions) && !(← isInductivePredicate typeName) then
     let indInfo ← getConstInfoInduct typeName
-    unless (← isProp indInfo.type) do
+    unless indInfo.isUnsafe do
+      let fns ← mkSizeOfFns typeName
       for indTypeName in indInfo.all, fn in fns do
         let indInfo ← getConstInfoInduct indTypeName
         forallTelescopeReducing indInfo.type fun xs _ =>

src/Lean/MonadEnv.lean

@@ -19,14 +19,24 @@ def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | some (ConstantInfo.inductInfo ..) => return true
   | _ => return false
 
+def isInductivePredicate [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
+  match (← getEnv).find? declName with
+  | some (ConstantInfo.inductInfo { type := type, ..}) => return visit type
+  | _ => return false
+where
+  visit : Expr → Bool
+    | Expr.sort u ..       => u == levelZero
+    | Expr.forallE _ _ b _ => visit b
+    | _                    => false
+
 def isRecCore (env : Environment) (declName : Name) : Bool :=
   match env.find? declName with
   | some (ConstantInfo.recInfo ..) => return true
   | _ => return false
 
-def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := 
+def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
   return isRecCore (← getEnv) declName
-  
+
 @[inline] def withoutModifyingEnv [Monad m] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α := do
   let env ← getEnv
   try x finally setEnv env
@@ -105,25 +115,25 @@ def addDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Decla
   | Except.ok    env => setEnv env
   | Except.error ex  => throwKernelException ex
 
-private def supportedRecursors := 
+private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
 
 private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Declaration) : m Unit := do
-  let env ← getEnv 
+  let env ← getEnv
   decl.forExprM fun e =>
-    let unsupportedRecursor? := e.find? fun 
-      | Expr.const declName .. => 
+    let unsupportedRecursor? := e.find? fun
+      | Expr.const declName .. =>
         ((isAuxRecursor env declName && !isCasesOnRecursor env declName) || isRecCore env declName)
         && !supportedRecursors.contains declName
       | _ => false
-    match unsupportedRecursor? with 
+    match unsupportedRecursor? with
     | some (Expr.const declName ..) => throwError! "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion"
     | _ => pure ()
 
 def compileDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Declaration) : m Unit := do
   match (← getEnv).compileDecl (← getOptions) decl with
   | Except.ok env   => setEnv env
-  | Except.error ex => 
+  | Except.error ex =>
     checkUnsupported decl -- Generate nicer error message for unsupported recursors
     throwKernelException ex