Agda-2.3.2.2: test/fail/SizeUnsolvedConstraintsInTypeSignature.err

SizeUnsolvedConstraintsInTypeSignature.agda:21,33-39
(↑ i) !=< i of type Size
when checking that the expression one2 i has type Nat (↑ (↑ i))