Require determined goal types before dictionary search - #6293

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

Reject goals containing unresolved inference variables before invoking dictionary search. A matching dictionary cannot infer a goal type; callers must first apply ordinary inference substitutions and require an annotation when variables remain unresolved. Rigid universals remain valid goals for polymorphic dictionary matching.

Regression tests cover a concrete dictionary with an unknown goal, nested and quantified unknowns, ordinary solved goals, and rigid-variable matching. This implements the agreed conservative inference boundary.

Full validation: all 13 unit suites, 22 CLI integration tests, 391 transcripts, edit/load round trips, manual rewrites, docs HTML generation, compiled fix5507 regression, and formatting passed.