[Agda] basic question about induction/recursion & pattern-matching

[Noam Zeilberger]

let's say we begin by defining two datatypes that mirror each other,
and a coercion between them:

 open import Logic.Identity 
 open import Data.Maybe

 module Test where

  data bool : Set where
    tt : bool
    ff : bool
  
  data BOOL : Set where
    TT : BOOL
    FF : BOOL
  
  b2B : bool -> BOOL
  b2B tt = TT
  b2B ff = FF

Now, we're interested in a datatype indexed by BOOL that has
a constructor taking a bool, like so:

  data foo : BOOL -> Set where
    FOO : (b : bool) -> foo (b2B b)

but let's also define a simpler datatype, just indexed by bool:

  data bar : bool -> Set where
    BAR : (b : bool) -> bar b

The question is, can we write an equality function on foos?

  fooeq : {B : BOOL} -> (x1 x2 : foo B) -> Maybe (x1 ≡ x2)

We can certainly write one on bars:

  bareq : {b : bool} -> (x1 x2 : bar b) -> Maybe (x1 ≡ x2)
  bareq (BAR b) (BAR .b) = just refl

But if we try to give the analogous definition of fooeq:

  fooeq (FOO b) (FOO .b) = just refl

Agda gives an error, "b' != b of type bool when checking that the
pattern FOO .b has type foo (b2B b)".  Indeed, if we do any
pattern-matching at all on the two arguments

  fooeq (FOO b1) (FOO b2) = {! !}

it gives the same error, "b2 != b1 of type bool when checking that the
pattern FOO b2 has type foo (b2B b1)".

So is there any way to write fooeq?

Noam