Merge PR #17924: Bidirectionality in Ltac2 typechecking + type annotations for goal/constr_matching scopes

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>