Universe inconsistency in Test.idr with Idris 0.9.19

[eckart]

compiling lightyear tests... Test.idr:18:1:Universe inconsistency. Working on: o39 Old domain: (7,7) New domain: (7,6) Involved constraints: ConstraintFC {uconstraint = o39 < p39, ufc = Test.idr:18:1} ConstraintFC {uconstraint = o39 < p39, ufc = Test.idr:18:1} ConstraintFC {uconstraint = k39 <= o39, ufc = Test.idr:18:1} ConstraintFC {uconstraint = m39 <= o39, ufc = Test.idr:18:1}

• could not compile tests *

[jfdm]

@eckart An upstream fix to Idris addresses this issue. Lightyear was updated to work with the latest version. In the mean time you can roll back the latest commit so that --typeintype is used to compile the tests. With this fix lightyear will work as inteded.

[eckart]

ah. cool. thank you.