diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,17 @@
+0.10
+----
+* Adapt to the `Semigroup`–`Monoid` Proposal (introduced in `base-4.11`):
+  * Add a `Semigroup` instance for `Dict`
+  * Add the appropriate `(:=>)` instances involving `Semigroup`, and change the
+    `Class () (Monoid a)` instance to `Class (Semigroup a) (Monoid a)` when
+    `base` is recent enough
+  * Add the appropriate `Lifting(2)` instances involving `Semigroup`
+* `Data.Constraint.Nat` now reexports the `Div` and `Mod` type families from
+  `GHC.TypeLits` on `base-4.11` or later
+* Fix the type signature of `maxCommutes`
+* Export the `no` method of `Bottom`
+* Add `NFData` instances for `Dict` and `(:-)`
+
 0.9.1
 -----
 * Correct an improper use of `unsafeCoerce` in the internals of
diff --git a/constraints.cabal b/constraints.cabal
--- a/constraints.cabal
+++ b/constraints.cabal
@@ -1,6 +1,6 @@
 name:          constraints
 category:      Constraints
-version:       0.9.1
+version:       0.10
 license:       BSD2
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -17,7 +17,7 @@
   This package provides a vocabulary for working with them.
 
 build-type:    Simple
-tested-with:   GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2
+tested-with:   GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1
 extra-source-files: README.markdown
                   , CHANGELOG.markdown
 
@@ -48,6 +48,7 @@
     ghc-prim,
     hashable >= 1.2 && < 1.3,
     mtl >= 2 && < 2.3,
+    semigroups >= 0.11 && < 0.19,
     transformers >= 0.2 && < 0.6,
     transformers-compat >= 0.4 && < 1
 
@@ -64,3 +65,16 @@
       Data.Constraint.Symbol
 
   ghc-options: -Wall
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+  hs-source-dirs: tests
+  main-is: Spec.hs
+  other-modules: GH55Spec
+  ghc-options: -Wall -threaded -rtsopts
+  build-tool-depends: hspec-discover:hspec-discover >= 2
+  build-depends:
+    base >= 4.7 && < 5,
+    constraints,
+    hspec >= 2
diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs
--- a/src/Data/Constraint.hs
+++ b/src/Data/Constraint.hs
@@ -64,7 +64,7 @@
   , strengthen1, strengthen2
   , (&&&), (***)
   , trans, refl
-  , Bottom
+  , Bottom(no)
   , top, bottom
   -- * Dict is fully faithful
   , mapDict
@@ -75,12 +75,11 @@
   ) where
 import Control.Applicative
 import Control.Category
+import Control.DeepSeq
 import Control.Monad
-#if __GLASGOW_HASKELL__ < 710
-import Data.Monoid
-#endif
 import Data.Complex
 import Data.Ratio
+import Data.Semigroup
 import Data.Data
 import qualified GHC.Exts as Exts (Any)
 import GHC.Exts (Constraint)
@@ -132,6 +131,9 @@
 deriving instance Ord (Dict a)
 deriving instance Show (Dict a)
 
+instance NFData (Dict c) where
+  rnf Dict = ()
+
 -- | From a 'Dict', takes a value in an environment where the instance
 -- witnessed by the 'Dict' is in scope, and evaluates it.
 --
@@ -238,6 +240,9 @@
 instance Show (a :- b) where
   showsPrec d _ = showParen (d > 10) $ showString "Sub Dict"
 
+instance a => NFData (a :- b) where
+  rnf (Sub Dict) = ()
+
 infixl 1 \\ -- required comment
 
 -- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
@@ -450,6 +455,7 @@
 instance () :=> Show Bool where ins = Sub Dict
 instance () :=> Show Ordering where ins = Sub Dict
 instance () :=> Show Char where ins = Sub Dict
+instance () :=> Show Int where ins = Sub Dict
 instance Show a :=> Show (Complex a) where ins = Sub Dict
 instance Show a :=> Show [a] where ins = Sub Dict
 instance Show a :=> Show (Maybe a) where ins = Sub Dict
@@ -471,6 +477,7 @@
 instance () :=> Read Bool where ins = Sub Dict
 instance () :=> Read Ordering where ins = Sub Dict
 instance () :=> Read Char where ins = Sub Dict
+instance () :=> Read Int where ins = Sub Dict
 instance Read a :=> Read (Complex a) where ins = Sub Dict
 instance Read a :=> Read [a] where ins = Sub Dict
 instance Read a :=> Read (Maybe a) where ins = Sub Dict
@@ -618,8 +625,27 @@
 instance RealFloat a :=> RealFloat (Const a b) where ins = Sub Dict
 #endif
 
+-- Semigroup
+instance Class () (Semigroup a) where cls = Sub Dict
+instance () :=> Semigroup () where ins = Sub Dict
+instance () :=> Semigroup Ordering where ins = Sub Dict
+instance () :=> Semigroup [a] where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Maybe a) where ins = Sub Dict
+instance (Semigroup a, Semigroup b) :=> Semigroup (a, b) where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Const a b) where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Semigroup a :=> Semigroup (Identity a) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,10,0)
+instance Semigroup a :=> Semigroup (IO a) where ins = Sub Dict
+#endif
+
 -- Monoid
+#if MIN_VERSION_base(4,11,0)
+instance Class (Semigroup a) (Monoid a) where cls = Sub Dict
+#else
 instance Class () (Monoid a) where cls = Sub Dict
+#endif
 instance () :=> Monoid () where ins = Sub Dict
 instance () :=> Monoid Ordering where ins = Sub Dict
 instance () :=> Monoid [a] where ins = Sub Dict
@@ -628,8 +654,6 @@
 instance Monoid a :=> Monoid (Const a b) where ins = Sub Dict
 #if MIN_VERSION_base(4,9,0)
 instance Monoid a :=> Monoid (Identity a) where ins = Sub Dict
-#endif
-#if MIN_VERSION_base(4,9,0)
 instance Monoid a :=> Monoid (IO a) where ins = Sub Dict
 #endif
 
@@ -700,7 +724,13 @@
 instance a :=> Read (Dict a) where ins = Sub Dict
 deriving instance a => Read (Dict a)
 
+instance () :=> Semigroup (Dict a) where ins = Sub Dict
+instance Semigroup (Dict a) where
+  Dict <> Dict = Dict
+
 instance a :=> Monoid (Dict a) where ins = Sub Dict
 instance a => Monoid (Dict a) where
-  mappend Dict Dict = Dict
+#if !(MIN_VERSION_base(4,11,0))
+  mappend = (<>)
+#endif
   mempty = Dict
diff --git a/src/Data/Constraint/Lifting.hs b/src/Data/Constraint/Lifting.hs
--- a/src/Data/Constraint/Lifting.hs
+++ b/src/Data/Constraint/Lifting.hs
@@ -9,7 +9,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# OPTIONS_GHC -fno-warn-deprecations #-}
-module Data.Constraint.Lifting 
+module Data.Constraint.Lifting
   ( Lifting(..)
   , Lifting2(..)
   ) where
@@ -54,6 +54,9 @@
 import Data.Monoid
 #endif
 import Data.Ratio
+#if !(MIN_VERSION_base(4,11,0))
+import Data.Semigroup
+#endif
 #if __GLASGOW_HASKELL__ < 710
 import Data.Traversable
 #endif
@@ -77,6 +80,7 @@
 instance Lifting Hashable Maybe where lifting = Sub Dict
 instance Lifting Binary Maybe where lifting = Sub Dict
 instance Lifting NFData Maybe where lifting = Sub Dict
+instance Lifting Semigroup Maybe where lifting = Sub Dict
 instance Lifting Monoid Maybe where lifting = Sub Dict
 
 instance Lifting Eq Ratio where lifting = Sub Dict
@@ -85,7 +89,7 @@
 instance Lifting Eq Complex where lifting = Sub Dict
 instance Lifting Read Complex where lifting = Sub Dict
 instance Lifting Show Complex where lifting = Sub Dict
-
+instance Lifting Semigroup ((->) a) where lifting = Sub Dict
 instance Lifting Monoid ((->) a) where lifting = Sub Dict
 
 instance Eq a => Lifting Eq (Either a) where lifting = Sub Dict
@@ -103,6 +107,7 @@
 instance Hashable a => Lifting Hashable ((,) a) where lifting = Sub Dict
 instance Binary a => Lifting Binary ((,) a) where lifting = Sub Dict
 instance NFData a => Lifting NFData ((,) a) where lifting = Sub Dict
+instance Semigroup a => Lifting Semigroup ((,) a) where lifting = Sub Dict
 instance Monoid a => Lifting Monoid ((,) a) where lifting = Sub Dict
 instance Bounded a => Lifting Bounded ((,) a) where lifting = Sub Dict
 instance Ix a => Lifting Ix ((,) a) where lifting = Sub Dict
@@ -434,6 +439,7 @@
 instance Lifting2 Hashable (,) where lifting2 = Sub Dict
 instance Lifting2 Binary (,) where lifting2 = Sub Dict
 instance Lifting2 NFData (,) where lifting2 = Sub Dict
+instance Lifting2 Semigroup (,) where lifting2 = Sub Dict
 instance Lifting2 Monoid (,) where lifting2 = Sub Dict
 instance Lifting2 Bounded (,) where lifting2 = Sub Dict
 instance Lifting2 Ix (,) where lifting2 = Sub Dict
diff --git a/src/Data/Constraint/Nat.hs b/src/Data/Constraint/Nat.hs
--- a/src/Data/Constraint/Nat.hs
+++ b/src/Data/Constraint/Nat.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -45,12 +46,20 @@
 import GHC.TypeLits
 import Unsafe.Coerce
 
-type family Min :: Nat -> Nat -> Nat where
-type family Max :: Nat -> Nat -> Nat where
-type family Div :: Nat -> Nat -> Nat where
-type family Mod :: Nat -> Nat -> Nat where
-type family Gcd :: Nat -> Nat -> Nat where
-type family Lcm :: Nat -> Nat -> Nat where
+type family Min (m::Nat) (n::Nat) :: Nat where
+    Min m m = m
+type family Max (m::Nat) (n::Nat) :: Nat where
+    Max m m = m
+#if !(MIN_VERSION_base(4,11,0))
+type family Div (m::Nat) (n::Nat) :: Nat where
+    Div m 1 = m
+type family Mod (m::Nat) (n::Nat) :: Nat where
+    Mod 0 m = 0
+#endif
+type family Gcd (m::Nat) (n::Nat) :: Nat where
+    Gcd m m = m
+type family Lcm (m::Nat) (n::Nat) :: Nat where
+   Lcm m m = m
 
 type Divides n m = n ~ Gcd n m
 
@@ -120,13 +129,13 @@
 modNat = Sub $ case magic @n @m mod of Sub r -> r
 
 plusZero :: forall n. Dict ((n + 0) ~ n)
-plusZero = axiom
+plusZero = Dict
 
 timesZero :: forall n. Dict ((n * 0) ~ 0)
-timesZero = axiom
+timesZero = Dict
 
 timesOne :: forall n. Dict ((n * 1) ~ n)
-timesOne = axiom
+timesOne = Dict
 
 minZero :: forall n. Dict (Min n 0 ~ 0)
 minZero = axiom
@@ -135,13 +144,13 @@
 maxZero = axiom
 
 powZero :: forall n. Dict ((n ^ 0) ~ 1)
-powZero = axiom
+powZero = Dict
 
 leZero :: forall a. (a <= 0) :- (a ~ 0)
 leZero = Sub axiom
 
 zeroLe :: forall a. Dict (0 <= a)
-zeroLe = axiom
+zeroLe = Dict
 
 plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)
 plusMonotone1 = Sub axiom
@@ -203,19 +212,19 @@
 minCommutes :: forall n m. Dict (Min m n ~ Min n m)
 minCommutes = axiom
 
-maxCommutes :: forall n m. Dict (Min m n ~ Min n m)
+maxCommutes :: forall n m. Dict (Max m n ~ Max n m)
 maxCommutes = axiom
 
-plusAssociates :: forall n m o. Dict (((m + n) + o) ~ (m + (n + o)))
+plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))
 plusAssociates = axiom
 
-timesAssociates :: forall n m o. Dict (((m * n) * o) ~ (m * (n * o)))
+timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))
 timesAssociates = axiom
 
-minAssociates :: forall n m o. Dict (Min (Min m n) o ~ Min m (Min n o))
+minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))
 minAssociates = axiom
 
-maxAssociates :: forall n m o. Dict (Max (Max m n) o ~ Max m (Max n o))
+maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))
 maxAssociates = axiom
 
 gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c  ~ Gcd a (Gcd b c))
@@ -225,16 +234,16 @@
 lcmAssociates = axiom
 
 minIsIdempotent :: forall n. Dict (Min n n ~ n)
-minIsIdempotent = axiom
+minIsIdempotent = Dict
 
 maxIsIdempotent :: forall n. Dict (Max n n ~ n)
-maxIsIdempotent = axiom
+maxIsIdempotent = Dict
 
 gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)
-gcdIsIdempotent = axiom
+gcdIsIdempotent = Dict
 
 lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)
-lcmIsIdempotent = axiom
+lcmIsIdempotent = Dict
 
 minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
 minDistributesOverPlus = axiom
diff --git a/tests/GH55Spec.hs b/tests/GH55Spec.hs
new file mode 100644
--- /dev/null
+++ b/tests/GH55Spec.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+#if __GLASGOW_HASKELL__ >= 800
+{-# LANGUAGE TypeApplications #-}
+#endif
+
+module GH55Spec (main, spec) where
+
+import Test.Hspec
+
+#if __GLASGOW_HASKELL__ >= 800
+import Data.Constraint
+import Data.Constraint.Nat
+import GHC.TypeLits
+
+newtype GF (n :: Nat) = GF Integer deriving (Eq, Show)
+
+instance KnownNat n => Num (GF n) where
+  xf@(GF a) + GF b = GF $ (a+b) `mod` (natVal xf)
+  xf@(GF a) - GF b = GF $ (a-b) `mod` (natVal xf)
+  xf@(GF a) * GF b = GF $ (a*b) `mod` (natVal xf)
+  abs = id
+  signum xf@(GF a) | a==0 = xf
+                   | otherwise = GF 1
+  fromInteger = GF
+
+x :: GF 5
+x = GF 3
+
+y :: GF 5
+y = GF 4
+
+foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
+foo m@(GF a) n@(GF b) = GF $ (a*b) `mod` (lcm (natVal m) (natVal n))
+
+bar :: (KnownNat m) => GF m -> GF m -> GF m
+bar (a :: GF m) b = foo a b - foo b a \\ Sub @() (lcmIsIdempotent @m) \\ lcmNat @m @m
+
+z :: GF 5
+z = bar x y
+
+spec :: Spec
+spec = describe "GH #53" $
+         it "should normalize Lcm m m" $
+           z `shouldBe` (GF 0 :: GF (Lcm 5 5))
+#else
+spec :: Spec
+spec = return ()
+#endif
+
+main :: IO ()
+main = hspec spec
diff --git a/tests/Spec.hs b/tests/Spec.hs
new file mode 100644
--- /dev/null
+++ b/tests/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}