From 0ab4fb1e0041470185fdaf651a7fcf1c4ad944fc Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Tue, 3 May 2022 09:06:49 +0200
Subject: [PATCH] Annotate telescope notations to support literal telescope
 arguments.

---
 tests/telescopes.v    | 24 ++++++++++++++++++++++++
 theories/telescopes.v | 16 ++++++++++++++--
 2 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index e282b131..e1836724 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -52,3 +52,27 @@ 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.
+ *)
+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.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 3dad07ed..2378216e 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -52,8 +52,20 @@ Fixpoint tele_arg@{u} (t : tele@{u}) : Type@{u} :=
   | TeleS f => tele_arg_cons (λ x, tele_arg (f x))
   end.
 Global Arguments tele_arg _ : simpl never.
-Notation TargO := tt (only parsing).
-Notation TargS a b := (@TeleArgCons _ (λ x, tele_arg _) a b) (only parsing).
+
+(* Coq has no idea that [unit] and [tele_arg_cons] have anything to do with
+   telescopes. This only becomes a problem when concrete telescope arguments
+   (of concrete telescopes) need to be typechecked. To work around this, we
+   annotate the notations below with extra information to guide unification.
+ *)
+
+(* The cast in the notation below is necessary to make Coq understand that
+   [TargO] can be unified with [tele_arg TeleO]. *)
+Notation TargO := (tt : tele_arg TeleO) (only parsing).
+(* The casts and annotations are necessary for Coq to typecheck nested [TargS]
+   as well as the final [TargO] in a chain of [TargS]. *)
+Notation TargS a b :=
+  ((@TeleArgCons _ (λ x, tele_arg (_ x)) a b) : (tele_arg (TeleS _))) (only parsing).
 Coercion tele_arg : tele >-> Sortclass.
 
 Lemma tele_arg_ind (P : ∀ TT, tele_arg TT → Prop) :
-- 
GitLab