two definitionally equal terms are not equal

[SimonForest]

Consider the excerpt coming from this

C : MyS State Operation Change
MyS.comp C (Operation-both (Left-id a) (Right-id d)) (Operation-both B D) = Operation-both B D
MyS.comp C (Operation-both (Left-id a) (Right-step)) (Operation-both B (Right-id .Right-done)) = Operation-both B (Right-step)
MyS.comp C (Operation-both (Left-step) (Right-id a)) (Operation-both (Left-id .Left-done) D) = Operation-both (Left-step) D
MyS.comp C (Operation-both (Left-step) (Right-step)) (Operation-both (Left-id .Left-done) (Right-id .Right-done)) = Operation-both (Left-step) (Right-step)

MyS.comp' C (Change-id (Operation-both (Left-step) (Right-id a))) (Change-id (Operation-both (Left-id .Left-done) D)) = Change-id (Operation-both (Left-step) D)

The context does not matter that much to understand the problem. A record C of type MyS State Operation Change is defined. The definition of C requires defining MyS.comp C and MyS.comp' C. MyS.comp C is accepted by Agda but MyS.comp' is not because of the following problem:

Operation-both Left-step D !=
MyS.comp C (Operation-both Left-step (Right-id a))
(Operation-both (Left-id Left-done) D)
of type
Operation (State-both Left-notdone a) (State-both Left-done d)
when checking that the expression
Change-id (Operation-both Left-step D) has type
Change
(MyS.comp C (Operation-both Left-step (Right-id a))
 (Operation-both (Left-id Left-done) D))

I think it is a bug since the problem can be reformulated as:

MyS.comp C (Operation-both Left-step (Right-id a)) (Operation-both (Left-id Left-done) D) != Operation-both Left-step D

but the definition of MyS.comp C says:

MyS.comp C (Operation-both (Left-step) (Right-id a)) (Operation-both (Left-id .Left-done) D) = Operation-both (Left-step) D

The problem seems related to using records since an alternative .agda without record does not trigger it (Agda fails but because the definition of MyS.comp' is not complete, as expected).

The problem is present in Agda 2.6.0.

[andreasabel]

Shrank this to

{-# OPTIONS --exact-split #-}

data Bool : Set where
  false : Bool
  true  : Bool

data R : Bool → Bool → Set where
  same : (a : Bool) → R a a
  diff : R false true

data Pair : Set where
  pair : Bool → Bool → Pair

data R2 : (a b : Pair) → Set where
  congPair : {a b c d : Bool} → R a b →  R c d → R2 (pair a c) (pair b d)

data Sing {a b : Pair} : (O : R2 a b) → Set where
  sg : (O : R2 a b) → Sing O

record MyS : Set where
  field
    comp  : {f f' f'' : Pair} (F : R2 f f') (G : R2 f' f'') → R2 f f''
    comp' : {f f' f'' : Pair} {F : R2 f f'} {G : R2 f' f''} (φ : Sing F) (ψ : Sing G) → Sing (comp F G)

test : MyS
MyS.comp test (congPair (same a) (same d)) (congPair B            D)            = congPair B D
MyS.comp test (congPair (same a) diff)     (congPair B            (same .true)) = congPair B diff
MyS.comp test (congPair diff     (same a)) (congPair (same .true) D)            = congPair diff D  -- This should fire, shouldn't it!?
MyS.comp test (congPair diff     diff)     (congPair (same .true) (same .true)) = congPair diff diff

MyS.comp' test (sg (congPair diff (same a))) (sg (congPair (same .true) D))     = sg (congPair diff D)   -- Can give, but fails on reload
MyS.comp' test (sg (congPair diff diff))     (sg (congPair C D))                = {!!}
MyS.comp' test (sg (congPair (same a) B))    (sg (congPair C D))                = {!!}

-- congPair diff D !=
--   MyS.comp test (congPair diff (same a)) (congPair (same true) D)
-- of type R2 (pair false a) (pair true d)
-- when checking that the expression sg (congPair diff D) has type
--   Sing (MyS.comp test (congPair diff (same a)) (congPair (same true) D))

This passes in Agda 2.5.3 and fails in Agda 2.5.4. I added option --exact-split to see whether there is a good reason for the reduction not to fire, but there isn't. Agda thinks this is an exact split, but still fails to reduce (using the clause pattern matcher, not the case trees).

[andreasabel]

@jespercockx : Could you have a look?

[jespercockx]

This is probably just #3054 again. The clause pattern matcher used to over-approximate the final case tree which lead to loss of subject reduction, so I fixed that by making it an under-approximation instead, which now causes some reductions not to fire.

Rather than trying to fix the clause pattern matcher to better approximate the case tree, we should just use the case tree always. But copatterns require us to evaluate the function already while it's being typechecked, so we need some notion of partial case tree that's used while the function is still incomplete

Maybe a cheap fix would be to run the clause compiler already after checking each individual clause (but ignoring coverage)? That way we would have the case tree available so we don't need to rely on the clause pattern matcher anymore.

But that's really fixing the problem by doing more work where we should rather be doing less, so I'd rather work on making the clause compiler incremental so we can add the clauses one by one.

[SimonForest]

Ok thanks for your help @andreasabel @jespercockx !