{-# OPTIONS --sized-types #-} module SizedTypesRigidVarClash where postulate Size : Set _^ : Size -> Size ∞ : Size {-# BUILTIN SIZE Size #-} {-# BUILTIN SIZESUC _^ #-} {-# BUILTIN SIZEINF ∞ #-} data Nat : {size : Size} -> Set where zero : {size : Size} -> Nat {size ^} suc : {size : Size} -> Nat {size} -> Nat {size ^} inc : {i j : Size} -> Nat {i} -> Nat {j ^} inc x = suc x