Bound the size of generated implicit goals - #6274

Stack from ghstack (oldest at bottom):

• Keep elaboration decisions from the final name-resolution pass #6303
• Accept dictionary elaboration only after core verification #6302
• Resolve source givens from their completed binding schemes #6301
• Preserve source given scope across dependency grouping #6300
• Record completed given schemes for deferred resolution #6299
• Build complete dictionary plans independently of note order #6298
• Introduce dictionary parameters while checking qualified definitions #6297
• Order generated dictionary parameters within source scopes #6296
• Capture lexical givens by their active binder identities #6295
• Record dictionary goals at precise checker application sites #6294
• Require determined goal types before dictionary search #6293
• Insert dictionaries at identified expression sites #6292
• Identify lexical dictionary bindings without changing source diagnostics #6291
• Track expression identity separately from source location #6290
• Check implicit arrows without erasing dictionary requirements #6289
• Keep effect rows outside implicit constraint contexts #6288
• Track given membership in namespace metadata #6287
• Verify explicit dictionary bodies before accepting elaboration #6286
• Decompose qualified signatures into dictionary candidates #6285
• Handle implicit parameters in function-type utilities #6276
• Represent and store implicit function arrows #6275
• -> Bound the size of generated implicit goals #6274
• Prefer strictly more specific dictionary conclusions #6273
• Resolve dictionary premises with bounded, context-sensitive search #6272
• Match polymorphic dictionaries without solving goal variables #6271
• Select lexical dictionaries by binding identity and scope #6270
• Preserve reserved namespace names when parsing text #6269

A recursion-depth limit does not bound a goal that doubles at each step. Stop after a bounded traversal of a generated goal, before matching or including an oversized goal in diagnostics.

The regression uses C a requiring C (Pair a a) and verifies that the size limit terminates the search well before the depth limit.

Validation: all 13 unit suites, 22 CLI integration tests, all 391 transcripts, round-trip and manual-rewrite checks, compiled-code and documentation checks, and formatting pass.