feat: simpler error message when sorries complicate universe inference

Author: robsimmons

src/Lean/Elab/MutualInductive.lean

@@ -614,6 +614,10 @@ private def collectUniverses (views : Array InductiveView) (r : Level) (rOffset
   let (_, acc) ← go |>.run {}
   if !acc.badLevels.isEmpty then
     withViewTypeRef views do
+      if indTypes.any (·.ctors.any (·.type.hasSyntheticSorry)) then
+        throwError "Type cannot be determined: some part of the definition contains an error"
+      if indTypes.any (·.ctors.any (·.type.hasSorry)) then
+        throwError "Type cannot be determined: some part of the definition contains `sorry`"
       let goodPart := Level.addOffset (Level.mkNaryMax acc.levels.toList) rOffset
       let badPart := Level.mkNaryMax (acc.badLevels.toList.map fun (u, k) => Level.max (Level.ofNat rOffset) (Level.addOffset u (rOffset - k)))
       let inferred := (Level.max goodPart badPart).normalize

tests/lean/univInference.lean

@@ -90,3 +90,15 @@ def ex7 (h : Stx = Nat) : True :=
   trivial
 
 end Induct
+
+inductive Sorry1 where
+  | x (a : Bool)
+  | y (b : sorry)
+
+inductive Sorry2 where
+  | x (a : Array Sorry2)
+  | y (b : sorry)
+
+inductive Sorry3 where
+  | x (a : Array Sorry3)
+  | y {x} (b : x Err3)

tests/lean/univInference.lean.expected.out

@@ -31,3 +31,26 @@ univInference.lean:81:48-81:62: error: Invalid universe polymorphic resulting ty
   Sort (max u v)
 
 Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:94:0-96:17: warning: declaration uses 'sorry'
+univInference.lean:98:0-100:17: error: Type cannot be determined: some part of the definition contains `sorry`
+univInference.lean:104:15-104:21: error: Function expected at
+  x
+but this term has type
+  ?m
+
+Note: Expected a function because this term is being applied to the argument
+  Err3
+univInference.lean:102:0-104:22: error: Type cannot be determined: some part of the definition contains an error