UnequalHiding.agda:7,5-46 {A : Set} → A → A != (A : Set) → A → A because one is an implicit function type and the other is an explicit function type when checking that the expression λ (id : (A : Set) → A → A) → id One one has type ({A : Set} → A → A) → One