UnequalHiding.err

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