Annotate telescope notations to support literal telescope arguments.

!368 (merged) had the unfortunate consequence that literal telescope arguments would not typecheck any more. This MR fixes this by adding copious (but nonetheless minimal) amounts of casts and annotations to make the [tele_arg ..] notation work again. I added tests for both new and old unification.

I am currently running a full test with these changes on all BedRock proofs which should tell us a bit about the compatibility. I expect no problems here.

Something that is not reflected in the MR but is still interesting is that old unification, i.e. apply and friends, work even without the cast in the TargS notation. New unification, i.e. refine, does not. There might be a Coq bug to report here but I don't have time to dig into that right now.

tests/telescopes.v

@@ -52,3 +52,30 @@ Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
 Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
   texist P ↔ ex P.
 Proof. by rewrite texist_exist. Qed.
+
+(** [tele_arg ..] notation tests.
+    These tests mainly test type annotations and casts in the [tele_arg]
+    notations.
+    We test that Coq can typecheck literal telescope arguments in two ways:
+    - tactic unification/old unification using [exact]
+    - evarconv/new unification using [refine]
+ *)
+Example tele_arg_notation_0 : [tele].
+assert_succeeds exact [tele_arg].
+assert_succeeds refine [tele_arg].
+Abort.
+
+Example tele_arg_notation_1 : [tele (_:nat)].
+assert_succeeds exact [tele_arg 0].
+assert_succeeds refine [tele_arg 0].
+Abort.
+
+Example tele_arg_notation_2 : [tele (_ : bool) (_ : nat)].
+assert_succeeds exact [tele_arg true; 0].
+assert_succeeds refine [tele_arg true; 0].
+Abort.
+
+Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False)].
+assert_succeeds exact [tele_arg true; 0].
+assert_succeeds refine [tele_arg true; 0].
+Abort.