feat: do not have meta imply partial (#11587)

This PR adjusts the new `meta` keyword of the experimental module system
not to imply `partial` for general consistency.

As the previous behavior can create confusion return types that are not
known to be `Nonempty` and few `def`s should be `meta` in the first
case, this special case does not appear to be worth the minor
convenience.

Author: Kha

src/Lean/Elab/DeclModifiers.lean

@@ -103,15 +103,6 @@ def Modifiers.isPartial : Modifiers → Bool
   | { recKind := .partial, .. }  => true
   | _                            => false
 
-/--
-Whether the declaration is explicitly `partial` or should be considered as such via `meta`. In the
-latter case, elaborators should not produce an error if partiality is unnecessary.
--/
-def Modifiers.isInferredPartial : Modifiers → Bool
-  | { recKind := .partial, .. }  => true
-  | { computeKind := .meta, .. } => true
-  | _                            => false
-
 def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false

src/Lean/Elab/PreDefinition/Main.lean

@@ -329,25 +329,13 @@ def addPreDefinitions (docCtx : LocalContext × LocalInstances) (preDefs : Array
         else if preDefs.any (·.modifiers.isUnsafe) then
           addAndCompileUnsafe docCtx preDefs
           preDefs.forM (·.termination.ensureNone "unsafe")
+        else if preDefs.any (·.modifiers.isPartial) then
+          for preDef in preDefs do
+            if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
+              withRef preDef.ref <| throwError "invalid use of `partial`, `{preDef.declName}` is not a function{indentExpr preDef.type}"
+          addAndCompilePartial docCtx preDefs
+          preDefs.forM (·.termination.ensureNone "partial")
         else
-          -- Consider partial if `partial` was given explicitly, or implied and no termination hint
-          -- was given
-          if preDefs.any (·.modifiers.isPartial) ||
-             preDefs.any (·.modifiers.isInferredPartial) && !preDefs.any (·.termination.isNotNone) then
-            let mut isPartial := true
-            for preDef in preDefs do
-              if !(← whnfD preDef.type).isForall then
-                if preDef.modifiers.isPartial then
-                  withRef preDef.ref <| throwError "invalid use of `partial`, `{preDef.declName}` is not a function{indentExpr preDef.type}"
-                else
-                  -- `meta` should not imply `partial` in this case
-                  isPartial := false
-
-            if isPartial then
-              addAndCompilePartial docCtx preDefs
-              preDefs.forM (·.termination.ensureNone "partial")
-              continue
-
           ensureFunIndReservedNamesAvailable preDefs
           try
             checkCodomainsLevel preDefs