Internal error rewriting with holes

[mikeshulman]

While trying to adapt the rest of my code to the restriction of #5996, I ran into another internal error.

{-# OPTIONS --type-in-type --rewriting #-}

infix 10 _≡_
infixl 30 _∷_
infixr 40 _⊚_
infixl 30 _▸_ _▹_
infix 60 _₀ _₁

data _≡_ {A : Set} (a : A) : A → Set where
  reflᵉ : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

data Tel : Set

el : Tel → Set

postulate
  _⇨_ : (Δ : Tel) (T : Set) → Set
  Λ⇨ : {Δ : Tel} {T : Set} → (el Δ → T) → (Δ ⇨ T)
  _⊘_ : {Δ : Tel} {T : Set} (B : Δ ⇨ T) (x : el Δ) → T
  ⊘β : {Δ : Tel} {T : Set} (B : el Δ → T) (x : el Δ) → (Λ⇨ {Δ} B) ⊘ x ≡ B x

{-# REWRITE ⊘β #-}

data _▹_ (Δ : Tel) (B : Δ ⇨ Set) : Set where
  _∷_ : (x : el Δ) → B ⊘ x → Δ ▹ B
open _▹_

data Tel where
  _▸_ : (Δ : Tel) (A : Δ ⇨ Set) → Tel

el (Δ ▸ A) = Δ ▹ A

pop : {Δ : Tel} {B : Δ ⇨ Set} → Δ ▹ B → el Δ
pop (δ ∷ _) = δ

top : {Δ : Tel} {B : Δ ⇨ Set} (δ : Δ ▹ B) → B ⊘ (pop δ)
top (_ ∷ b) = b

postulate
  _⊚_ : {Γ Δ : Tel} {T : Set} (g : Δ ⇨ T) (f : Γ ⇨ el Δ) → (Γ ⇨ T)
  ⊚⊘ : {Γ Δ : Tel} {T : Set} (g : Δ ⇨ T) (f : Γ ⇨ el Δ) (x : el Γ) →
    (g ⊚ f) ⊘ x ≡ g ⊘ (f ⊘ x)

{-# REWRITE ⊚⊘ #-}

ID : Tel → Tel

_₀ : {Δ : Tel} → el (ID Δ) → el Δ
_₁ : {Δ : Tel} → el (ID Δ) → el Δ

Λ₀ : {Δ : Tel} → (ID Δ) ⇨ el Δ
Λ₀ = (Λ⇨ λ x → x ₀)

Λ₁ : {Δ : Tel} → (ID Δ) ⇨ el Δ
Λ₁ = (Λ⇨ λ x → x ₁)

postulate
  Id : {Δ : Tel} (A : Δ ⇨ Set) (δ : el (ID Δ)) (a₀ : A ⊘ (δ ₀)) (a₁ : A ⊘ (δ ₁)) → Set

ID▸▸ : {Δ : Tel} (A : Δ ⇨ Set) → Tel
ID▸▸ {Δ} A = ID Δ ▸ (A ⊚ Λ₀) ▸ (A ⊚ Λ₁ ⊚ (Λ⇨ λ x → pop x))

Id/ : {Δ : Tel} (A : Δ ⇨ Set) → ID▸▸ A ⇨ Set
Id/ A = (Λ⇨ λ x → Id A (pop (pop x)) (top (pop x)) (top x))

ID (Δ ▸ A) = ID▸▸ A ▸ Id/ A

_₀ {Δ ▸ A} (δ ∷ a₀ ∷ a₁ ∷ a₂) = δ ₀ ∷ a₀

_₁ {Δ ▸ A} (δ ∷ a₀ ∷ a₁ ∷ a₂) = δ ₁ ∷ a₁

postulate
  AP : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) → el (ID Δ)
  AP₀ : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) → (AP f γ)₀ ≡ f ⊘ (γ ₀)
  AP₁ : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) → (AP f γ)₁ ≡ f ⊘ (γ ₁)

{-# REWRITE AP₀ AP₁ #-}

postulate
  Id-AP⊚ : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) (A : Δ ⇨ Set)
          (a₀ : A ⊘ (f ⊘ (γ ₀))) (a₁ : A ⊘ (f ⊘ (γ ₁))) →
    Id (A ⊚ f) γ a₀ a₁ ≡ Id A (AP f γ) a₀ a₁

{-# REWRITE Id-AP⊚ #-}

SQ : Tel → Tel
SQ Δ = ID (ID Δ)

module Square
  {Δ : Tel} (A : Δ ⇨ Set) (δ : el (SQ Δ))
  {a₀₀ : A ⊘ (δ ₀ ₀)} {a₀₁ : A ⊘ (δ ₁ ₀)} (a₀₂ : Id A (AP Λ₀ δ) a₀₀ a₀₁)
  {a₁₀ : A ⊘ (δ ₀ ₁)} {a₁₁ : A ⊘ (δ ₁ ₁)} (a₁₂ : Id A (AP Λ₁ δ) a₁₀ a₁₁)
  (a₂₀ : Id A (δ ₀) a₀₀ a₁₀) (a₂₁ : Id A (δ ₁) a₀₁ a₁₁) where

  Sq : Set
  Sq = Id {ID▸▸ A} (Id/ A) (δ ∷ a₀₀ ∷ a₀₁ ∷ a₀₂ ∷ a₁₀ ∷ a₁₁ ∷ {!a₁₂!}) a₂₀ a₂₁

  sq∷ : (a₂₂ : Sq) → el (SQ (Δ ▸ A))
  sq∷ a₂₂ = δ ∷ a₀₀ ∷ a₀₁ ∷ a₀₂ ∷ a₁₀ ∷ a₁₁ ∷ {!a₁₂!} ∷ a₂₀ ∷ a₂₁ ∷ a₂₂

  postulate
    sq∷₀₂ : (a₂₂ : Sq) → AP (Λ₀ {Δ ▸ A}) (sq∷ a₂₂) ≡ (AP Λ₀ δ) ∷ a₀₀ ∷ a₀₁ ∷ a₀₂

  {-# REWRITE sq∷₀₂ #-}

In Agda 2.6.3-5d2d77a this yields

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs:191:27 in Agda-2.6.3-K939Rz0lK6d4Qhz5rVu9uS:Agda.TypeChecking.Rewriting.NonLinPattern

I don't know whether this has to do with the presence of unfilled holes in Sq and sq. I plan to comment out the final REWRITE, which is what produces the error, and figure out how to fix things so those holes can be filled, and then I'll report on whether the error still appears (if it hasn't been fixed already).

[plt-amy]

@jespercockx It seems like the check for "no metavariables in rewrite rules" can be defeated by hiding the metavariable in the RHS of a function. Here's a minimal reproducer:

{-# OPTIONS --type-in-type --rewriting #-}

infix 10 _≡_

data _≡_ {A : Set} (a : A) : A → Set where
  reflᵉ : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

postulate
  T : Set
  C : T
  F : T → T

a : T → T
a x = ?

postulate
  r : ∀ x → F (a x) ≡ C

{-# REWRITE r #-}

If we change the type of r to r : ∀ x → F ? ≡ C then we get the intended, user-facing error

/home/amelia/default/Projects/etc/agda/test2.agda:25,1-18
r  is not a legal rewrite rule, since it contains unsolved meta variables
when checking the pragma REWRITE r

but if we use F (a x), then we get the internal error above.

[mikeshulman]

Ah, I suspected it might be something like that.

[andreasabel]

Works correctly in Agda 2.6.0.