WhyWeNeedUntypedLambda.err

WhyWeNeedUntypedLambda.agda:14,22-26
((x : _13 k) → _13 k) != ({A : Set} → A → A) because one is an
implicit function type and the other is an explicit function type
when checking that the expression refl has type
((x : _13 k) → _13 k) == IdT