Confluence checking is not invariant under expanding records

[sattlerc]

On master (https://github.com/agda/agda/commit/ee876ee229cdc2f3b1ff80f6d60568a1869f9385).

{-# OPTIONS --rewriting --confluence #-}
module Issue7035 where

postulate
  X : Set
  x : X
  Eq : X → X → Set
{-# BUILTIN REWRITE Eq #-}

postulate
  B : Set

record R : Set where
  field
    b : B
    g : B → X

postulate
  r : R
open R r

postulate
  rule : Eq (g b) x
{-# REWRITE rule #-}

Checking the above gives

B != (x₁ : _9) → _11 (_ = x₁)
when checking confluence of the rewrite rule rule with itself

Note that the problem disappears if we replace

postulate
  r : R
open R r

by

postulate
  b : B
  g : B → X

[jespercockx]

Confluence checking is very synactic by necessity, so it is not necessarily expected to be invariant under beta- or eta-equality. However, the error message here is certainly strange.

[sattlerc]

Here is a version where the confluence check triggers an internal error similar to #7034. Maybe there is a connection?

{-# OPTIONS --two-level --rewriting --confluence-check #-}
module Issue7034-2 where

open import Agda.Primitive using (SSet)

postulate
  X : SSet
  x : X
  Eq : X → X → SSet
{-# BUILTIN REWRITE Eq #-}

module _ (B : SSet) where
  record R : SSet where
    field
      b : B
      g : B → X

  postulate
    r : R
  open R r

  postulate
    rule : Eq (g b) x
{-# REWRITE rule #-}

Output:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Constraints.hs:71:11 in Agda-2.6.5-e6225bb25c63bc5db4df82dfc6332dd35c7e75b82b069e132d432fe47063d72b:Agda.TypeChecking.Constraints

[andreasabel]

Here is a version where the confluence check triggers an internal error similar to #7034. Maybe there is a connection?

Not sure. This internal error is fixed by PR

• #7039