diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -17,9 +17,9 @@
                           (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*),
                           (:-:), (:-), (%:-), (%-),
                           -- ** Type-level predicate & judgements
-                          Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance(..), leqRefl, leqSucc,
+                          Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, leqRefl, leqSucc,
                           boolToPropLeq, boolToClassLeq, propToClassLeq,
-                          LeqTrueInstance(..), propToBoolLeq,
+                          LeqTrueInstance, propToBoolLeq,
                           -- * Conversion functions
                           natToInt, intToNat, sNatToInt,
                           -- * Quasi quotes for natural numbers
@@ -52,7 +52,9 @@
                                    Show (..), error, id, otherwise, ($), (.), undefined)
 import qualified Prelude          as P
 import           Proof.Equational
+import Data.Constraint hiding ((:-))
 import Language.Haskell.TH.Quote
+import Unsafe.Coerce
 import Language.Haskell.TH
 
 --------------------------------------------------
@@ -203,8 +205,7 @@
   ZeroLeq     :: SNat m -> Leq Zero m
   SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
 
-data LeqTrueInstance a b where
-  LeqTrueInstance :: (a :<<= b) ~ True => LeqTrueInstance a b
+type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
 
 (%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)
 n   %- SZ    = n
@@ -224,33 +225,53 @@
 --------------------------------------------------
 -- * Total orderings on natural numbers.
 --------------------------------------------------
-propToBoolLeq :: Leq n m -> LeqTrueInstance n m
-propToBoolLeq (ZeroLeq _) = LeqTrueInstance
-propToBoolLeq (SuccLeqSucc leq) =
-  case propToBoolLeq leq of
-    LeqTrueInstance -> LeqTrueInstance
+propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
+propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())
+{-# INLINE propToBoolLeq #-}
 
-data LeqInstance n m where
-  LeqInstance :: (n :<= m) => LeqInstance n m
+boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
+boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())
+{-# INLINE boolToClassLeq #-}
 
-boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
-boolToPropLeq SZ     m      = ZeroLeq m
-boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
-boolToPropLeq _      _      = bugInGHC
+propToClassLeq :: Leq n m -> LeqInstance n m
+propToClassLeq _ = unsafeCoerce (Dict :: Dict ())
+{-# INLINE propToClassLeq #-}
 
+{-
+-- | Below is the "proof" of the correctness of above:
+propToBoolLeq :: Leq n m -> LeqTrueInstance n m
+propToBoolLeq (ZeroLeq _) = Dict
+propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict
+{-# RULES
+ "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .
+  propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)
+ #-}
+
 boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
-boolToClassLeq SZ     _      = LeqInstance
-boolToClassLeq (SS n) (SS m) =
-  case boolToClassLeq n m of
-    LeqInstance -> LeqInstance
+boolToClassLeq SZ     _      = Dict
+boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict
 boolToClassLeq _ _ = bugInGHC
+{-# RULES
+ "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).
+  boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
+ #-}
 
 propToClassLeq :: Leq n m -> LeqInstance n m
-propToClassLeq (ZeroLeq _) = LeqInstance
-propToClassLeq (SuccLeqSucc leq) =
-  case propToClassLeq leq of
-    LeqInstance -> LeqInstance
+propToClassLeq (ZeroLeq _) = Dict
+propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict
+{-# RULES
+ "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .
+  propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)
+ #-}
+-}
 
+type LeqInstance n m = Dict (n :<= m)
+
+boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
+boolToPropLeq SZ     m      = ZeroLeq m
+boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
+boolToPropLeq _      _      = bugInGHC
+
 leqRefl :: SNat n -> Leq n n
 leqRefl SZ = ZeroLeq sZ
 leqRefl (SS n) = SuccLeqSucc $ leqRefl n
@@ -326,9 +347,6 @@
     Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq
 plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'
 
-infer :: Proxy a
-infer = Proxy
-
 plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m'
 plusCongL _ Refl = Refl
 
@@ -394,7 +412,7 @@
 plusMinusEqL SZ     m = minusNilpotent m
 plusMinusEqL (SS n) m =
   case propToBoolLeq (plusLeqR n m) of
-    LeqTrueInstance -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)
+    Dict -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)
 
 plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n
 plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)
diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -15,6 +15,7 @@
        ) where
 import Data.Type.Monomorphic
 import Data.Type.Natural hiding (promote)
+import Data.Constraint
 
 -- | Set-theoretic (finite) ordinals:
 --
@@ -69,7 +70,7 @@
   minBound = OZ
   maxBound =
     case propToBoolLeq $ leqRefl (sing :: SNat n) of
-      LeqTrueInstance -> sNatToOrd (sing :: SNat n)
+      Dict -> sNatToOrd (sing :: SNat n)
 
 unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n
 unsafeFromInt n = 
@@ -132,8 +133,9 @@
   in case singInstance (sn %+ sm) of
        SingInstance ->
          case propToBoolLeq (plusLeqR sn sm) of
-           LeqTrueInstance -> inclusion n
+           Dict -> inclusion n
 OS n @+ m =
   case sing :: SNat n of
     SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m
     _ -> bugInGHC
+
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.0.6.0
+version:             0.1.0.0
 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
@@ -27,3 +27,4 @@
                ,       equational-reasoning     == 0.0.*
                ,       monomorphic              >= 0.0.3
                ,       template-haskell         == 2.8.*
+               ,       constraints              == 0.3.*