CheckSizeMetaBounds.agda:27,1-28,30
Cannot solve size constraints
_i_17 n =< _j_16 n : Size
↑ _j_16 n =< .i : Size
when checking the definition of magic