Issue259c.agda

{- This example used to fail but after the point-free evaluation fix
   it seems to work #-}
module Issue259c where

postulate
  A : Set
  a : A
  b : ({x : A} → A) → A
  C : A → Set

d : {x : A} → A
d {x} = a

e : A
e = b (λ {x} → d {x})

F : C e → Set₁
F _ with Set
F _ | _ = Set