add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat add x y = x + y Actually, (GHC) Haskell can express something like this type if you turn on

add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat add x y = x + y Actually, (GHC) Haskell can express something like this type if you turn on the required extensions. data Nat = Z | S Z deriving (Eq, Ord, Show) data SNat (n :: Nat) where SZ :: SNat Z SS :: SNat n -> SNat (S n) type family Compare (a :: Nat) (b :: Nat) :: Ordering where Compare Z Z = EQ Compare (S a) Z = GT Compare Z (S a) = LT Compare (S a) (S b) = Compare a b type a < b = Compare a b ~ LT type family (+) (a :: Nat) (b :: Nat) :: Nat where Z + a = a a + Z = a (S a) + b = S (a + b) add :: (a < b) => SNat a -> SNat b -> SNat (a+b) add = ...