Agda-2.3.2.2: test/fail/WrongHidingInLHS.err
WrongHidingInLHS.agda:5,1-10
Found an implicit argument where an explicit argument was expected
when checking that the clause f {x} = x has type Set → Set
WrongHidingInLHS.agda:5,1-10
Found an implicit argument where an explicit argument was expected
when checking that the clause f {x} = x has type Set → Set