foo:Set→Setfoo⦃x⦄=x-- error: [WrongHidingInLHS]-- Unexpected implicit argument-- ^~~~~~~~~~~~~~~~~ really!?bar:Set→Setbar=λ⦃x⦄→x-- error: [WrongHidingInLambda]-- Found an implicit lambda where an explicit lambda was expected-- ^~~~~~~~~~~~~~~~~~~~~~~~ oh did you?baz:(Set→Set)→Set→Setbazfg=f⦃g⦄-- error: [WrongHidingInApplication]-- Found an implicit application where an explicit application was-- ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ yeah? tell me more!-- expectedThe fix here is to record both the expected and actual hidings, and report them with verbalize.
```agda
foo : Set → Set
foo ⦃ x ⦄ = x
-- error: [WrongHidingInLHS]
-- Unexpected implicit argument
-- ^~~~~~~~~~~~~~~~~ really!?
```
```agda
bar : Set → Set
bar = λ ⦃ x ⦄ → x
-- error: [WrongHidingInLambda]
-- Found an implicit lambda where an explicit lambda was expected
-- ^~~~~~~~~~~~~~~~~~~~~~~~ oh did you?
```
```agda
baz : (Set → Set) → Set → Set
baz f g = f ⦃ g ⦄
-- error: [WrongHidingInApplication]
-- Found an implicit application where an explicit application was
-- ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ yeah? tell me more!
-- expected
```
The fix here is to record both the expected and actual hidings, and report them with `verbalize`.