Agda-2.3.2.2: test/fail/SizedTypesScopeExtrusion.err
SizedTypesScopeExtrusion.agda:28,41-42 ∞ !=< i of type Size when checking that the expression x has type Nat
SizedTypesScopeExtrusion.agda:28,41-42 ∞ !=< i of type Size when checking that the expression x has type Nat