This code does not work since polarity of Nat (monotone in i) is only inferred when the constructors are given. But it is already needed for checking sub.

  data Nat : {i : Size} -> Set

  sub : {i : Size} -> Nat {i} → Nat {↑ i}
  sub x = x

  data Nat where
    zero : {i : Size}            -> Nat {↑ i}
    suc  : {i : Size} -> Nat {i} -> Nat {↑ i}

Original issue reported on code.google.com by andreas....@gmail.com on 19 Feb 2012 at 10:21

Attachments:

• NewMutualSized.agda