Agda-2.3.2.2: test/fail/SizedTypesRigidVarClash.agda

{-# 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