Elaboration failure from interaction between `GetElem?` and default instances

Description

If the index to xs[...]? notation is a natural number literal, the GetElem? instance synthesis is deferred until later. This can result in elaboration failure since the return value of xs[...]? might be forced to be something unexpected.

Context

This came up on Zulip when a user was asking about why a monadic expression wasn't elaborating.

Steps to Reproduce

Consider

def justFirst (xs : List α) : Option α :=
  xs[0]? >>= fun first => first

Expected behavior: This elaborates.

Actual behavior: There is an error on xs[0]? with "failed to synthesize GetElem? (List α) ℕ (Option α) ?m".

Versions

4.12.0-rc1, macOS 15.0, m3

Additional Information

The reason this doesn't succeed is that the OfNat instance for 0 doesn't resolve until default instances are considered. By this point fun first => first elaborates, forcing the type of xs[0]? to be Option (Option α).

One solution to this would be to have a separate typeclass whose purpose is to specify the element type of a collection, independent of the index type. For example elements of List α have type α. This would let us solve for the return type before resolving the index type.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the justFirst example from the issue in Lean 4 and confirm the GetElem? synthesis error. The issue names no repository files or tests; done means the example elaborates successfully without forcing the result to an unintended nested Option type.