Agda-2.3.2.2: test/fail/UnequalRelevance.err
UnequalRelevance.agda:11,7-8 (A → A) !=< (.A → A) because one is a relevant function type and the other is an irrelevant function type when checking that the expression f has type .A → A
UnequalRelevance.agda:11,7-8 (A → A) !=< (.A → A) because one is a relevant function type and the other is an irrelevant function type when checking that the expression f has type .A → A