module Strange {A B C : Set} (a : A) (b : B) (c : C) where

open import Data.Product open import Relation.Binary.PropositionalEquality

T : Set T = A × B × C

val : T val = a , b , c

ap : {R : Set} (f : T → R) → R ap f = let x , y , z = val in f (x , y , z)

ap′ : {R : Set} (f : T → R) → R ap′ f = f (proj₁ val , proj₁ (proj₂ val) , proj₂ (proj₂ val))

test : ∀ {R} (f : T → R) → ap f ≡ f (a , b , c) test f = {!refl!}

The type of the hole in the example above reduces to:

Goal: f (a , proj₂ a , c) ≡ f (a , b , c)

even though it should reduce to

f (a , b , c) ≡ f (a , b , c)

And indeed, refl doesn't fit there. Typechecking the example where the hole has been replaced with refl produces:

D:\Agda\Strange.agda:21,10-14 proj₂ a != b of type B

when checking that the expression refl has type ap f ≡ f (a , b , c)

With ap′, the goal reduces correctly and refl is accepted.

I'm using a development version of Agda, about one day old. 64bit Windows 7, if it matters.

Fixed. The translation of nested let-patterns was incorrect, so ap f translated into

f (proj1 val, proj2 (proj1 val), proj2 (proj2 val))

(projections stacked the wrong way round). Works now.

Issue 1107 has been merged into this issue.