Issue292-16b.agda

-- 2011-09-15 posted by Nisse, variant of Issue292e
-- {-# OPTIONS --show-implicit -v tc.lhs.unify:15 #-}
module Issue292-16b where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate
  A : Set
  f : A → A

data C (A : Set)(f : A → A) : A → Set where
  c : ∀ x → C A f (f x)

record Box : Set where
  constructor box
  field
    a : A
    b : C A f a

test : ∀ {x₁ x₂} → box (f x₁) (c x₁) ≡ box (f x₂) (c x₂) → x₁ ≡ x₂
test refl = refl

-- We recover from the heteogenerous
--
--   c x₁ : C A f (f x₁) =?= c₂ x₂ : C A f (f x₂)
--
-- to the homogeneous
--
--   x₁ =?= x₂ : A
--
-- since the parameters to C are syntactically equal on lhs and rhs