Remove unused pattern constructor A.AnnP

[andreasabel]

Original introduced in PR #5006 commit 22e9a12

See also:

• Supply implicit argument for agda/agda#7390 cubical#1143

[andreasabel]

This PR triggers a regression in the type checker.
The type argument B = A tt to the defStrictEquiv macro is no longer inferred:
https://github.com/agda/cubical/blob/6d6870cbf537294fc3fdf9c5a34909bde30ba914/Cubical/Data/Sigma/Properties.agda#L333
@jespercockx Do you have some intuition as to why this happens?

[andreasabel]

Here is an extracted test case:

{-# OPTIONS --safe --cubical #-}

open import Agda.Primitive using (Level) renaming (Set to Type; _⊔_ to ℓ-max)
open import Agda.Primitive.Cubical using (PathP)
  renaming ( primIMin to _∧_  -- I → I → I
           ; primIMax to _∨_  -- I → I → I
           ; primINeg to ~_   -- I → I
           )

open import Agda.Builtin.Cubical.Glue using ( equiv-proof ; _≃_ )
open import Agda.Builtin.Cubical.Path using (_≡_)
open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd)
open import Agda.Builtin.Unit using (tt) renaming ( ⊤ to Unit )

import Agda.Builtin.Reflection as R

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    B : A → Type ℓ
    C : (a : A) → B a → Type ℓ
    x y : A

refl : x ≡ x
refl {x = x} _ = x
{-# INLINE refl #-}

cong : (f : (a : A) → B a) (p : x ≡ y) →
       PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)
{-# INLINE cong #-}

fiber : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) (y : B) → Type (ℓ-max ℓ ℓ')
fiber {A = A} f y = Σ A λ x → f x ≡ y

strictContrFibers : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} (g : B → A) (b : B)
  → Σ (fiber f (f (g b))) λ t →
    ((t' : fiber f b) → PathP (λ _ → fiber f (f (g b))) t (g (f (t' .fst)) , cong (λ x → f (g x)) (t' .snd)))
strictContrFibers {f = f} g b .fst = (g b , refl)
strictContrFibers {f = f} g b .snd (a , p) i = (g (p (~ i)) , λ j → f (g (p (~ i ∨ j))))

infixl 4 _>>=_
_>>=_ = R.bindTC

infixr 5 _v∷_
pattern varg t = R.arg (R.arg-info R.visible (R.modality R.relevant R.quantity-ω)) t
pattern _v∷_ a l = varg a ∷ l

strictEquivClauses : R.Term → R.Term → List R.Clause
strictEquivClauses f g =
  R.clause []
    (R.proj (quote fst) v∷ [])
    f
  ∷ R.clause []
    (R.proj (quote snd) v∷ R.proj (quote equiv-proof) v∷ [])
    (R.def (quote strictContrFibers) (g v∷ []))
  ∷ []

defStrictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → (A → B) → (B → A) → R.TC Unit
defStrictEquiv idName f g =
  R.quoteTC f >>= λ `f` →
  R.quoteTC g >>= λ `g` →
  R.defineFun idName (strictEquivClauses `f` `g`)

module _ {ℓ : Level} (A : Unit → Type ℓ) where

  ΣUnit : Σ Unit A ≃ A tt
  unquoteDef ΣUnit = defStrictEquiv {-B = A tt-} ΣUnit snd λ{ x → (tt , x) }

The current master can find the solution B = A tt, but not this PR.

NB: When I change the last term from pattern-lambda λ{ x → (tt , x) } to ordinary lambda or section (tt ,_), then B is no longer solved even on master. So the pattern-lambda seems some kind of hack here to enhance the type checker, but it is a bit brittle.

[andreasabel]

I filed agda/cubical#1143. This one change makes this PR go through with cubical.

• Supply implicit argument for agda/agda#7390 cubical#1143