feat: simpler error message when sorries complicate universe inference

[robsimmons]

This PR simplifies an error message encountered when universe resolution is ambiguous. The message is quite technical and can be triggered if an inductive definition includes a sorry or an error; in the event of a sorry a simpler error message almost certainly suffices.

Example

inductive Sorry2 where
  | x (a : Array Sorry2)
  | y (b : sorry)

Currently the error message is:

Resulting type is of the form
  Type ?u.5
but the universes of constructor arguments suggest that this could
accidentally be a higher universe than necessary. Explicitly providing a
resulting type will silence this error. Universe inference suggests using
  Sort (max 1 u_1)
if the resulting universe level should be at the above universe level or
higher.

Explanation: At this point in elaboration, universe level unification has
committed to using a resulting universe level of the form `?u.5+1`.
Constructor argument universe levels must be no greater than the resulting
universe level, and this condition implies the following constraint(s):
  u_1 ≤ ?u.5+1
However, such constraint(s) usually indicate that the resulting universe level
should have been in a different form. For example, if the resulting type is of
the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`,
then universe inference would yield `Sort (u + 1)`, but the resulting type
`Sort (max 1 u)` would avoid being in a higher universe than necessary.

With this PR, the error message is:

Type cannot be determined: some part of the definition contains `sorry`

which is really the heart of the matter. If the sorry is synthetic, the error message is:

Type cannot be determined: some part of the definition contains an error

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5f561bfee287eaf9f1907c8a9e67bff58acdd242 --onto dd28f005889dd2fcca6fe0638133de561a655ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 18:06:30)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5f561bfee287eaf9f1907c8a9e67bff58acdd242 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-04 18:06:31)

[robsimmons]

Suggested change

	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`"
	-- The universe level for `sorry` gets abstracted in a way that leads to this error
	-- Improving `sorry` handling when computing the universe level of an inductive type might make this case redundant.
	if indTypes.any (·.ctors.any (·.type.hasSyntheticSorry)) then
	throwError "Type cannot be determined: some part of the definition contains an error"

[kmill]

Here's another approach: #11524

For this, if a constructor field has a sorry, it uses an approximate solution to the universe level constraints for that field.

[robsimmons]

Closing in favor of #11524