Agda-2.3.2.2: test/succeed/Issue233.agda
-- Bug: With abstraction depended on bound variable names! module Issue233 where postulate T : (Set → Set) → Set mkT : (F : Set → Set) → T F foo : T (λ A → A) foo with λ (B : Set) → B ... | F = mkT F
-- Bug: With abstraction depended on bound variable names! module Issue233 where postulate T : (Set → Set) → Set mkT : (F : Set → Set) → T F foo : T (λ A → A) foo with λ (B : Set) → B ... | F = mkT F