A bug in Agda ?

bug.agda

record MyS
  (State : Set)
  (Operation : (f g : State) → Set)
  (Change : {f g : State} (O : Operation f g) → Set)
  :
  Set
  where
  field
    comp : {f f' f'' : State} (F : Operation f f') (G : Operation f' f'') → Operation f f''
    comp' : {f f' f'' : State} {F : Operation f f'} {G : Operation f' f''} (φ : Change F) (ψ : Change G) → Change (comp F G)

data Left-state : Set where
  Left-notdone : Left-state
  Left-done : Left-state

data Right-state : Set where
  Right-notdone : Right-state
  Right-done : Right-state

data State : Set where
  State-both : Left-state → Right-state → State

data Left : Left-state → Left-state → Set where
  Left-id : (a : Left-state) → Left a a
  Left-step : Left Left-notdone Left-done

data Right : Right-state → Right-state → Set where
  Right-id : (a : Right-state) → Right a a
  Right-step : Right Right-notdone Right-done

data Operation : (a b : State) → Set where
  Operation-both : {a b : Left-state} {c d : Right-state} (A : Left a b) (C : Right c d) → Operation (State-both a c) (State-both b d)

data Change : {a b : State} (O : Operation a b) → Set where
  Change-id : {a b : State} (O : Operation a b) → Change O

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)