Internal error: non-confluent rewriting to singletons

[mikeshulman]

I did a much better job minimizing this one!

{-# OPTIONS --rewriting #-}

postulate
  _≡_ : {A : Set₁} (a : A) → A → Set
{-# BUILTIN REWRITE _≡_ #-}

record ⊤ : Set where
  constructor ★

postulate
  X Y : Set
  F : Set → Set
  FX : F X ≡ ⊤
{-# REWRITE FX #-}

postulate
  G : F X → Set
  G1 : (A : Set) → F A ≡ G ★
  G2 : G ★ ≡ Y

{-# REWRITE G1 #-}
{-# REWRITE G2 #-}

Produces

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:185:49 in Agda-2.6.3-2504eeb4755139097364d9a4622fd6cdb917d395c0018ad56c8f58f2b4d3d665:Agda.TypeChecking.Rewriting.NonLinPattern

The issue title is my amaterish attempt to guess the culprit, given that the error goes away if (1) ⊤ and ★ are made postulates, or (2) G1 is specialized to any particular A (removing the non-confluence with FX). It also goes away if the rewrite pragmas for G1 and G2 are coalesced into one.

[jespercockx]

The problem here is that Agda gets confused about the type of the ★ argument to G in the rule G2: ★ is a constructor so Agda expects its type to be a data or record type, but G2 takes an argument of type F X, which reduces to G ★ which is not a data or record type. (Of course it also reduces to ⊤, but Agda is not good at dealing with non-confluence).

While thinking about how to best fix this, I realized that it is probably not really necessary to look at the type of the patterns in a rewrite rule while checking the rule, only when applying it. This does indeed seem to fix the problem here, but there is two issues with it:

• We still need to solve the same problem when applying the rule, so we only postponed it. One possibility would be to simply refuse to apply the rule, which is better than throwing an internal error, I guess.
• We currently eta-expand the patterns of the rewrite rule while checking it. Skipping this eta-expansion breaks the (global) confluence check, in particular the test case for Subpatterns with bound variables not considered by confluence check #3816 is erroneously accepted. So implementing this fix would require making the confluence checker deal with eta-equality in a better way.

Unfortunately, due to this I think this might take a bit longer to solve. In the mean time I might replace the internal error with a failure so at least Agda gives you a better idea of what is going on.

[mikeshulman]

The current confluence checker isn't fully correct anyway in the presence of singleton eta, right? Because of #5929 ?