Agda-2.3.2.2: test/fail/LostTypeError.err

LostTypeError.agda:23,34-36
x != y of type A
when checking that the expression px has type P (box y)