diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -229,7 +229,7 @@
 
 type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
 
-(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)
+(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m)
 n   %- SZ    = n
 SS n %- SS m = n %- m
 _    %- _    = error "impossible!"
diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -83,7 +83,7 @@
 
 unsafeFromInt :: forall n. SingI n => Int -> Ordinal n
 unsafeFromInt n =
-    case promote n of
+    case (promote n :: Monomorphic (Sing :: Nat -> *)) of
       Monomorphic sn ->
         case sS sn %:<<= (sing :: SNat n) of
           STrue -> sNatToOrd' (sing :: SNat n) sn
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.2.1.1
+version:             0.2.1.2
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
 homepage:            https://github.com/konn/type-natural
@@ -30,4 +30,4 @@
   if impl(ghc < 7.8)
     build-depends:     singletons               == 0.8.*
   else
-    build-depends:     singletons               >= 0.10    && < 1.1
+    build-depends:     singletons               >= 0.10    && < 1.0