How can I define Ord for integralTy?

gistfile1.idr

integralTy : (signed : Bool) -> Nat -> Type
integralTy False 0 = Bits8
integralTy False 1 = Bits16
integralTy False 2 = Bits32
integralTy False 3 = Bits64
integralTy _     _ = Integer

inRange : Ord (integralTy m n) => integralTy m n -> integralTy m n -> integralTy m n -> Bool
inRange x lower upper = lower <= x && x < upper

||| An integer in the range [lower, upper). BoundedInt 0 ~= Fin, but using
||| Integers instead of Peano arithmetic, for efficiency. Suitably limited
||| values (anything that doesn’t overflow [0–2^64)) use primitive machine types
||| instead of Integer.
BoundedInt : Integer -> Nat -> Type
BoundedInt lower upper =
  (x : integralTy (lower < 0) (log2 upper) ** so (inRange x lower upper))