Refl for an equality type of an equality type gives a Universe Inconsistency

[pdorrell]

This code:

data ABC = A | B | C

B_equals_B_is_B_equals_B : (B = B) = (B = B)
B_equals_B_is_B_equals_B = Refl

results in:

- + Errors (1)
 `-- builtin line 0 col -1:
     Universe inconsistency.
             Working on: primitive.q
             Old domain: (4,4)
             New domain: (4,3)
             Involved constraints: 
                     ConstraintFC {uconstraint = primitive.q <= primitive.o, ufc = builtin}
                     ConstraintFC {uconstraint = ./equality_of_equality.idr.a1 < primitive.q, ufc = equality_of_equality.idr:5:26}
                     ConstraintFC {uconstraint = primitive.q < primitive.r, ufc = builtin}
                     ConstraintFC {uconstraint = primitive.q <= primitive.o, ufc = builtin}

On the other hand, the following code compiles:

data ABC = A | B | C

refl_for_value : {t : Type} -> (x : t) -> x = x
refl_for_value x = Refl

B_equals_B_is_B_equals_B : (B = B) = (B = B)
B_equals_B_is_B_equals_B = refl_for_value (B = B)

Platform info: running Idris v1.0-git:e32f5cd build with stack on Ubuntu 16.04.

(A secondary issue is that depending on what other code is in the same source file, the Universe inconsistency error message might or might not include a correct line/col position.)

[ahmadsalim]

I think the issue here is that Idris has currently some universe polymorphism for functions but not for constructors. So when you want to produce a proof Refl {x = Refl {x = B}} it fails because Refl is used at two levels.

I am not sure what the solution is, but perhaps the same rules that apply to functions w.r.t. universe checking could apply to constructors. @ozgurakgun @edwinb Any ideas?