The internal error is raised here:

• 2.4.2.6: works
• 2.5.1.1: works
• 2.5.2: internal error
• 2.5.3: internal error
• 2.5.4.2: internal error
• 2.6.0: works
• 2.6.1: internal error
• 2.6.2: internal error
• 2.6.3 (master): internal error

Bisection blames commit 475c7e5 (ping @jespercockx ):
Date: Tue Jan 21 11:29:47 2020 +0100
[ fix #4382 ] Call isEtaRecordType after reducing the type

This was a fun puzzle to minimize. Here is the result of about an hour of minimization work:

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Unit

postulate
  A : Set
  f : {X : Set} → X → A
  g : {X : Set} → A → X
  rew-fg : {X : Set} (a : A) → f (g {X} a) ≡ a
{-# REWRITE rew-fg #-}

postulate
  h : A → ⊤
  rew-hf : h (f tt) ≡ tt
{-# REWRITE rew-hf #-}

Error message:

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

Now I just need to fix the issue...

Here's an even smaller version:

{-# OPTIONS --rewriting -vrewriting:70 #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Unit

postulate
  A : Set
  a : A
  f : {X : Set} → X → A
  g : {X : Set} → A → X
  rew-fg : {X : Set} (a : A) → f (g {X} a) ≡ a
{-# REWRITE rew-fg #-}

test : f tt ≡ a
test = refl

Debug output:

{ attempting to rewrite term  f tt
 having head  f  of type  {X : Set} → X → A
 with rule  rew-fg {X : Set} (a₁ : A)  |- 
            (f X (g X a₁))  -->  a₁  :  A
matching elimination  X
  with                $ {_}
  eliminating head    f : {X : Set} → X → A
matching pattern  X   with term       ⊤   of type         Set
pattern vars:    {X : Set} (a₁ : A)
bound vars:     
matching a PVar:  1
matching elimination  (g X a₁)
  with                $ tt
  eliminating head    f : ⊤ → A
matching pattern  (g X a₁)   with term       tt   of type         ⊤
pattern vars:    {X : Set} (a₁ : A)
bound vars:     
matching a PDef:  g
rewrote  f tt
 to  "dummyTerm: __DUMMY_TERM__, called at src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:415:30 in Agda-2.6.3-2GgStRv6exQAe2hnultIdP:Agda.TypeChecking.Rewriting.NonLinMatch" }

It seems that the matcher is eta-expanding the term g {X} a to tt, which causes the variable a to be unbound on the left-hand side of the rewrite rule.

I'm honestly at a loss of what should be the right behaviour here. Essentially, what we have here are two functions f {⊤} : ⊤ -> A and g {⊤} : A -> ⊤ that are each others inverses definitionally: g {⊤} (f x) is definitionally equal to x because of eta-equality, and f {⊤} (g x) is definitionally equal to x because of the rewrite rule rew-fg. However, since any two elements of ⊤ are equal, this means that all elements of A are also equal. Even worse, we can do this for any type A, thus making all terms definitionally equal to all other terms. This sounds to me like a non-ideal situation to be in, and I'd rather not support this in Agda (if it is even possible to do).

Other things we could consider doing to solve this:

1. Refuse to apply the rewrite rule when some of the variables on the left are not bound. This has the disadvantage that we lose completeness (and transitivity) of conversion checking wrt definitional equality. In other words, you get type errors complaining that two terms are not equal even though they should be.
2. Throw an error (or a warning) when you define a rewrite rule where a variable is bound in a position whose type could potentially be instantiated to a definitional subsingleton type. In particular, this would reject the rule Id-AP in the OP because the variables f and t₂ are bound in the subterm (AP f t₂), whose type is ID Δ (f t₀) (f t₁), which can compute to ⊤. This has the disadvantage that detecting when a type "could potentially be instantiated to a definitional subsingleton type" is undecidable and any sound check would likely have a lot of false positives.

I think for now I will go ahead and implement option 1, which should at least get rid of the internal error and replace it with a proper error message.

I have pushed a fix to 73d146b, will merge it once CI is finished.

Good news for @mikeshulman : with this patch, the example in the OP actually goes through without errors. However, please be mindful of the fact that you might still get spurious type errors with these rules as I explained above.

Continued in #5929

Thanks! I agree that option 1 is better.

I'm happy to report that Agda master with the patch also works without errors for my original much longer development. Thanks again for the very quick fix.

I have the impression that by having syntactical matching instead of matching modulo eta this kind of problem could be prevented.

f tt does not syntactically match f (g x), so we would not have f tt = x. But we would still have a "typed" critical pair, as f (g {⊤} x) rewrites both to x and to f tt (using the eta rule). Then, we cannot fix this neither by adding x --> f tt nor f tt --> x, as neither of those are valid rules. Thus, in the ideal case in which Agda only accepts confluent rules, the rule f (g x) --> x would have to be rejected.

@jespercockx , I remember you have already explained this to me, but what was the reason why matching modulo eta was essential?

I would also be interested in hearing more about why rewriting happens modulo eta. According to issues like #2979 and #3335, it looks like it was intentional.

In my development it's important that rewriting doesn't do eta-expansion, because in my hacky implementation of HOTT that would cause infinite rewrite loops. There the "higher-dimensional explicit substitution" ap reduces on all terms, including eliminators (just like an ordinary substitution). So if ap is applied to a term s : A x B, say, and s gets eta-expanded to (fst s, snd s), then the rewrite rules for comma and fst and snd will fire and reduce the whole thing to an eta-expansion of ap s again.

Currently I'm working around this by not using actual records for things like product types. Instead I assert them and their constructors and fields as postulates, with their beta-reductions and eta-contractions (!) as postulated rewrites. This sort of works, but it would be nicer to be able to use actual records.

I don't know how Agda's conversion-checking algorithm works, but from a bidirectional point of view, it seems to me that rewrites are part of the reduction phase, which is separated from the eta-expansion phase. Ordinary beta-reduction doesn't happen modulo eta-equality (otherwise it too would loop), so I wouldn't expect rewrites to do so. If there are applications that really do need rewriting to happen modulo eta, perhaps it could be enabled and disabled by a flag, either globally or locally for individual rewrite rules?

Currently I'm working around this by not using actual records for things like product types. Instead I assert them and their constructors and fields as postulates, with their beta-reductions and eta-contractions (!) as postulated rewrites. This sort of works, but it would be nicer to be able to use actual records.

You can turn off η-equality for a given record type by using no-eta-equality.

But I want my product and sigma-types to have eta-equality.

I suppose I could make them records with ordinary eta-equality turned off, and then add eta-contraction as a rewrite on top of that?

I don't know if that would work, but you could try.

To be honest, I have never really considered the possibility that rewrite rules should not respect eta-equality. IMO it is a core principle of Agda that everything should be invariant under replacing a term with a definitionally equal one (modulo performance). Not considering eta-equality would be a lot simpler to implement than the current algorithm, but it would destroy the completeness of Agda's conversion checker, even when the rules are confluent. However, as noted by @thiagofelicissimo perhaps this could be fixed by a notion of "typed confluence" that considers eta-rules as well as rewrite rules. AFAIK this has not yet been done in any system so it would be interesting to discuss it further.

For the use case by @mikeshulman here, I guess that either you are fine with checking confluence by hand, or you do not mind working with a non-confluent system (and accept the consequences of incomplete conversion and lack of subject reduction). This has so far not been a use case I considered while implementing rewrite rules, but it perhaps does make sense to have this notion of "simple" / "even more unsafe" rewrite rules. As I mentioned above, I do not think this would be especially difficult to implement, as it amounts to basically disabling all the type-directed parts of the matching algorithm used for --rewriting. If this is something you would like to have in Agda, feel free to make a feature request so we can discuss it further.

Ordinary beta-reduction doesn't happen modulo eta-equality (otherwise it too would loop), so I wouldn't expect rewrites to do so.

Ordinary beta-reduction does not have to do any matching, so there is no need to consider eta-equality for it.

That's interesting, I hadn't thought of that.

I said:

I suppose I could make them records with ordinary eta-equality turned off, and then add eta-contraction as a rewrite on top of that?

@nad replied:

I don't know if that would work, but you could try.

I tried, and it doesn't work.

record _×_ (A B : Set) : Set where
  no-eta-equality
  constructor _,_
  field
    fst : A
    snd : B
open _×_

postulate
  η, : {A B : Set} (u : A × B) → (fst u , snd u) ≡ u

{-# REWRITE η, #-}

Leads to

η,  is not a legal rewrite rule, since the following variables are not bound by the left hand side:  u

This makes some sense: I guess fst u is not a pattern occurrence of u when fst is a projection.

But it works with data and defined projections, why should it fail with no-eta records?

{-# OPTIONS --rewriting #-}

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

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

fst : {A B : Set} (u : A × B) → A
fst (a , b) = a

snd : {A B : Set} (u : A × B) → B
snd (a , b) = b

postulate
  η, : {A B : Set} (u : A × B) → (fst u , snd u) ≡ u

{-# REWRITE η, #-}

Succeeds.

While the non-linear patterns of rewriting can represent projection patterns, they are not generated:

• data: Pattern generated from lhs: (_,_ (fst u) (snd u))
• record: Pattern generated from lhs: (_,_ .(fst u) .(snd u)) -- this means dot pattern (do not bind u)

Agda hits the case u .fst with u a variable and then does not parse this into a pattern, because it wants Miller patterns for variables.

It definitely could work, since as you say it works with datatypes and defined projections. I was assuming Agda's perspective was that for records, fst u is a spine with u as its head, since u is in "elimination position", rather than a spine with fst as its head as would be the case if fst is an ordinary function and fst u is an ordinary function application.