From the bits and pieces of information I gathered about agda I'd (apparently erroneously) concluded that ∀ {A} was equivalent to {A : Set}. Now I noticed that
flip : ∀ {A B C} -> (A -> B -> C) -> (B -> A -> C)
is invalid (something about Set\omega which in turn seems to be some internal something, but
flip : {A B C : Set} -> (A -> B -> C) -> (B -> A -> C)
is fine. Can anyone clear this up for me?