[Agda] RFC: R.B.HeterogeneousEquality + i-cong

[Helmut Grohne]

On Wed, Feb 05, 2014 at 10:59:11AM +0100, Ulf Norell wrote:
> It's not the same situation as in subst. You can infer both X and Y from
> the type of f in many cases. Here's your motivating example:
> 
> i-cong : ∀ {l m n} {I : Set l} {X : I → Set m} {Y : I → Set n}
>          (f : {i : I} → X i → Y i) {i j : I} → i P.≡ j →
>          {x : X i} {y : X j} → x ≅ y → f x ≅ f y
> i-cong f P.refl refl = refl
> 
> module _
>   (A B : Set)
>   (n m : ℕ)
>   (xs : Vec A n)
>   (ys : Vec A m)
>   (n=m : n P.≡ m)
>   (xs=ys : xs ≅ ys)
>   (f : A → B) where
> 
>   thm : map f xs ≅ map f ys
>   thm = i-cong (map f) n=m xs=ys

Here is the error message for precisely this example using Agda 2.3.2.2
with line 25 being the definitional line of thm:

Unsolved metas at the following locations:
  .../test.agda:25,9-27
  .../test.agda:25,17-20
  .../test.agda:25,28-33
  .../test.agda:25,9-33

An interactive Agda session says:

_x_72 : Vec A (_n_74 n)  [ at .../test.agda:25,9-27 ]
_y_73 : Vec A (_n_74 n)  [ at .../test.agda:25,9-27 ]
_n_74 : ℕ  [ at .../test.agda:25,17-20 ]
_75 : _x_72 A B n m xs ys n=m xs=ys f ≅ _y_73 A B n m xs ys n=m xs=ys f [ at .../test.agda:25,28-33 ]
_76 : _x_72 A B n m xs ys n=m xs=ys f ≅ _y_73 A B n m xs ys n=m xs=ys f [ at .../test.agda:25,28-33 ]
_77 : (replicate f ⊛ xs) ≅ (replicate f ⊛ ys)  [ at .../test.agda:25,9-33 ]
_78 : (replicate f ⊛ xs) ≅ (replicate f ⊛ ys)  [ at .../test.agda:25,9-33 ]

Not even for this example X and Y can be inferred. It gets worse with
larger examples, specifically when using ≅-Reasoning. Maybe it works in
the development version of Agda?

Helmut