Unhygienic name handling

[andreasabel]

data Bool : Set where
  false : Bool
  true  : Bool

If : Set -> Set -> Bool -> Set
If x y true  = x
If x y false = y

if : (P : Bool -> Set) -> P true -> P false -> (b : Bool) -> P b
if P x y true  = x
if P x y false = y

data Sigma (A : Set)(B : A -> Set) : Set where
  wrap : [f : (b : Bool) -> If A (B (f true)) b] -> Sigma A B

pair : (A : Set) -> (B : A -> Set) -> (x : A) -> (y : B x) -> Sigma A B
pair A B x y = wrap A B (if (If A (B x)) x y)

data Empty : Set where
  {}

data Unit : Set where
  unit : Unit

T : Bool -> Set
T true  = Unit
T false = Empty

f : Sigma Bool T
f = pair Bool T true unit

Error:

fail: Expected function type, found El *126
in the application of f
to true

when checking that f true has type _

Succeeds if I rename the last f to f1, so it seems it gets confused with the locally bound f in constructor wrap.