Agda: Internal error (Rewriting.hs:395) with generalize and rewrite rules

[guillaumebrunerie]

The internal error occurs at the last line and goes away if we explicitly quantify on n and m (and it fails as expected).

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

variable
  n m : Nat

postulate
  +S : {n m : Nat} → (n + suc m) ≡ suc (n + m)
  {-# REWRITE +S #-}

  P : Nat → Nat → Set
  Q : Nat → Set

  R : {n m : Nat} → P n m → Q (m + n) → Set

  bug : (p : P n m) (q : Q n) → R p q

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Rewriting.hs:395

[sattlerc]

This seems to interact with the BUILTIN feature for natural numbers. If you take away the declaration {-# BUILTIN NATPLUS _+_ #-}, the internal error disappears.

[sattlerc]

Here is a smaller test case.

{-# OPTIONS --rewriting #-}

data Nat : Set where
  zero : Nat
  suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)
{-# BUILTIN NATPLUS _+_ #-} -- Without this, the internal error disappears.

postulate
  _≡_ : Nat → Nat → Set
{-# BUILTIN REWRITE _≡_ #-}

postulate
  a b n : Nat
  Q : Nat → Set
  R : (m n : Nat) → Q (m + n) → Set
  +S : (n + a) ≡ b
{-# REWRITE +S #-}

variable
  m : Nat -- Explicitly quantifying over m, the internal error disappears.

postulate
  bug : (q : Q n) → R m n q

[guillaumebrunerie]

Good catch!