Agda-2.3.2.2: test/fail/Issue644.err
Issue644.agda:28,13-14 R !=< ((x : A) → P x) of type Set₁ when checking that the expression r has type (x : A) → P x
Issue644.agda:28,13-14 R !=< ((x : A) → P x) of type Set₁ when checking that the expression r has type (x : A) → P x