diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,4 @@
+# Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package
+
+## 0.1 *October 21st 2015*
+* Initial release
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright (c) 2015, Christiaan Baaij
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the
+   distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,11 @@
+# ghc-typelits-extra
+
+[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-extra.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-extra)
+[![Hackage](https://img.shields.io/hackage/v/ghc-typelits-extra.svg)](https://hackage.haskell.org/package/ghc-typelits-extra)
+[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-extra.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-extra)
+
+Extra type-level operations on GHC.TypeLits.Nat and a custom solver implemented
+as a GHC type-checker plugin:
+
+* `GHC.TypeLits.Extra.GCD`: a type-level `gcd`
+* `GHC.TypeLits.Extra.CLog`: type-level equivalent of `clog x y = ceiling (logBase x y)`
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal
new file mode 100644
--- /dev/null
+++ b/ghc-typelits-extra.cabal
@@ -0,0 +1,71 @@
+name:                ghc-typelits-extra
+version:             0.1
+synopsis:            Additional type-level operations on GHC.TypeLits.Nat
+description:
+  Additional type-level operations on @GHC.TypeLits.Nat@:
+  .
+  * @GHC.TypeLits.Extra.GCD@: a type-level @gcd@
+  .
+  * @GHC.TypeLits.Extra.CLog@: type-level equivalent of
+    "@clog x y = ceiling (logBase x y)@"
+  .
+  And a custom solver for the above operations defined in
+  @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin,
+  add the
+  .
+  @
+  OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver
+  @
+  .
+  pragma to the header of your file.
+homepage:            http://www.clash-lang.org/
+bug-reports:         http://github.com/clash-lang/ghc-typelits-extra/issues
+license:             BSD2
+license-file:        LICENSE
+author:              Christiaan Baaij
+maintainer:          christiaan.baaij@gmail.com
+copyright:           Copyright © 2015 University of Twente
+category:            Type System
+build-type:          Simple
+extra-source-files:  README.md
+                     CHANGELOG.md
+cabal-version:       >=1.10
+
+source-repository head
+  type: git
+  location: https://github.com/clash-lang/ghc-typelits-extra.git
+
+flag deverror
+  description:
+    Enables `-Werror` for development mode and TravisCI
+  default: False
+  manual: True
+
+library
+  exposed-modules:     GHC.TypeLits.Extra,
+                       GHC.TypeLits.Extra.Solver
+  other-modules:       GHC.TypeLits.Extra.Solver.Unify
+                       GHC.TypeLits.Extra.Solver.Operations
+  build-depends:       base                >= 4.8  && <4.9,
+                       ghc                 >= 7.10 && <7.12,
+                       ghc-tcplugins-extra >= 0.1
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  if flag(deverror)
+    ghc-options:         -Wall -Werror
+  else
+    ghc-options:         -Wall
+
+test-suite test-ghc-typelits-extra
+  type:                exitcode-stdio-1.0
+  main-is:             Main.hs
+  Other-Modules:       ErrorTests
+  build-depends:       base                      >= 4.8 && <4.9,
+                       ghc-typelits-extra        >= 0.1,
+                       ghc-typelits-natnormalise >= 0.3,
+                       tasty                     >= 0.10,
+                       tasty-hunit               >= 0.9
+  hs-source-dirs:      tests
+  default-language:    Haskell2010
+  if flag(deverror)
+    ghc-options:       -O0 -dcore-lint
diff --git a/src/GHC/TypeLits/Extra.hs b/src/GHC/TypeLits/Extra.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Extra.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE DataKinds    #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-# OPTIONS_HADDOCK show-extensions #-}
+
+{-# LANGUAGE Safe #-}
+
+{-|
+Copyright  :  (C) 2015, University of Twente
+License    :  BSD2 (see the file LICENSE)
+Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
+
+Additional type-level operations on 'GHC.TypeLits.Nat':
+
+  * 'GCD': a type-level 'gcd'
+
+  * 'CLog': type-level equivalent of
+    \"@clog x y = 'ceiling' ('logBase' x y)@\"
+
+A custom solver for the above operations defined is defined in
+"GHC.TypeLits.Extra.Solver" as a GHC type-checker plugin. To use the plugin,
+add the
+
+@
+{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
+@
+
+pragma to the header of your file.
+-}
+module GHC.TypeLits.Extra where
+
+import GHC.TypeLits (Nat)
+
+-- | Type-level greatest common denominator (GCD).
+--
+-- Note that additional equations are provided by the type-checker plugin solver
+-- "GHC.TypeLits.Extra.Solver".
+type family GCD (x :: Nat) (y :: Nat) :: Nat where
+  GCD 0 x = x -- Additional equations are provided by the custom solver
+
+-- | Type-level equivalent of:
+--
+-- @
+-- clog x y = 'ceiling' ('logBase' x y)
+-- @
+--
+-- Note that additional equations are provided by the type-checker plugin solver
+-- "GHC.TypeLits.Extra.Solver".
+type family CLog (x :: Nat) (y :: Nat) :: Nat where
+  CLog 2 1 = 0 -- Additional equations are provided by the custom solver
diff --git a/src/GHC/TypeLits/Extra/Solver.hs b/src/GHC/TypeLits/Extra/Solver.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Extra/Solver.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE TupleSections #-}
+
+{-# OPTIONS_HADDOCK show-extensions #-}
+
+{-|
+Copyright  :  (C) 2015, Christiaan Baaij
+License    :  BSD2 (see the file LICENSE)
+Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
+
+-}
+module GHC.TypeLits.Extra.Solver
+  ( plugin )
+where
+
+-- external
+import Data.Maybe          (catMaybes, mapMaybe)
+import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, lookupModule,
+                            lookupName, newGiven, newWantedWithProvenance,
+                            tracePlugin)
+
+-- GHC API
+import FastString (fsLit)
+import Module     (mkModuleName)
+import OccName    (mkTcOcc)
+import Outputable (Outputable (..), (<+>), ($$), text)
+import Plugins    (Plugin (..), defaultPlugin)
+import TcEvidence (EvTerm)
+import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt)
+import TcRnTypes  (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence,
+                   ctEvPred, ctLoc, isGiven, isWanted, mkNonCanonical)
+import TcType     (mkEqPred, typeKind)
+import Type       (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,
+                   mkTyVarTy)
+import TysWiredIn (typeNatKind)
+
+-- internal
+import GHC.TypeLits.Extra.Solver.Operations
+import GHC.TypeLits.Extra.Solver.Unify
+
+-- | A solver implement as a type-checker plugin for:
+--
+--   * @GHC.TypeLits.Extra.GCD@: a type-level 'gcd'
+--
+--   * @GHC.TypeLits.Extra.CLog@: type-level equivalent of
+--     \"@clog x y = 'ceiling' ('logBase' x y)@\"
+--
+-- To use the plugin, add
+--
+-- @
+-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
+-- @
+--
+-- To the header of your file.
+plugin :: Plugin
+plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }
+
+normalisePlugin :: TcPlugin
+normalisePlugin = tracePlugin "ghc-typelits-extra"
+  TcPlugin { tcPluginInit  = lookupExtraDefs
+           , tcPluginSolve = decideEqualSOP
+           , tcPluginStop  = const (return ())
+           }
+
+decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+decideEqualSOP _    _givens _deriveds []      = return (TcPluginOk [] [])
+decideEqualSOP defs givens  _deriveds wanteds = do
+  -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
+  let wanteds' = filter (isWanted . ctEvidence) wanteds
+  let unit_wanteds = mapMaybe (toNatEquality defs) wanteds'
+  case unit_wanteds of
+    [] -> return (TcPluginOk [] [])
+    _  -> do
+      unit_givens <- mapMaybe (toNatEquality defs) <$> mapM zonkCt givens
+      sr <- simplifyExtra (unit_givens ++ unit_wanteds)
+      tcPluginTrace "normalised" (ppr sr)
+      case sr of
+        Simplified subst evs ->
+          TcPluginOk (filter (isWanted . ctEvidence . snd) evs) <$>
+            mapM (substItemToCt defs) (filter (isWanted . ctEvidence . siNote) subst)
+        Impossible eq -> failWithProvenace $ fromNatEquality eq
+
+substItemToCt :: ExtraDefs -> SubstItem -> TcPluginM Ct
+substItemToCt defs si
+  | isGiven (ctEvidence ct) = mkNonCanonical <$> newGiven loc predicate evTm
+  | otherwise               = mkNonCanonical <$> newWantedWithProvenance
+                                                   (ctEvidence ct) predicate
+  where
+    predicate = mkEqPred ty1 ty2
+    ty1  = mkTyVarTy (siVar si)
+    ty2  = reifyExtraOp defs (siOP si)
+    ct   = siNote si
+    loc  = ctLoc ct
+    evTm = evByFiat "ghc-typelits-extra" ty1 ty2
+
+type NatEquality = (Ct,ExtraOp,ExtraOp)
+
+data SimplifyResult
+  = Simplified ExtraSubst [(EvTerm,Ct)]
+  | Impossible NatEquality
+
+instance Outputable SimplifyResult where
+  ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs
+  ppr (Impossible eq)  = text "Impossible" <+> ppr eq
+
+simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult
+simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] [] eqs
+  where
+    simples :: ExtraSubst -> [Maybe (EvTerm, Ct)] -> [NatEquality]
+            -> [NatEquality] -> TcPluginM SimplifyResult
+    simples subst evs _xs [] = return (Simplified subst (catMaybes evs))
+    simples subst evs xs (eq@(ct,u,v):eqs') = do
+      ur <- unifyExtra ct (substsExtra subst u) (substsExtra subst v)
+      tcPluginTrace "unifyExtra result" (ppr ur)
+      case ur of
+        Win         -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) []
+                               (xs ++ eqs')
+        Lose        -> return  (Impossible eq)
+        Draw []     -> simples subst evs (eq:xs) eqs'
+        Draw subst' -> simples (substsSubst subst' subst ++ subst') evs [eq]
+                               (xs ++ eqs')
+
+-- Extract the Nat equality constraints
+toNatEquality :: ExtraDefs -> Ct -> Maybe NatEquality
+toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
+    EqPred NomEq t1 t2
+      | isNatKind (typeKind t1) || isNatKind (typeKind t1)
+      -> (ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2
+    _ -> Nothing
+  where
+    isNatKind :: Kind -> Bool
+    isNatKind = (== typeNatKind)
+
+fromNatEquality :: NatEquality -> Ct
+fromNatEquality (ct, _, _) = ct
+
+lookupExtraDefs :: TcPluginM ExtraDefs
+lookupExtraDefs = do
+    md <- lookupModule myModule myPackage
+    gcdTc <- look md "GCD"
+    clogTc <- look md "CLog"
+    return $ ExtraDefs gcdTc clogTc
+  where
+    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
+    myModule  = mkModuleName "GHC.TypeLits.Extra"
+    myPackage = fsLit "ghc-typelits-extra"
+
+-- Utils
+evMagic :: Ct -> Maybe EvTerm
+evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
+    EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)
+    _                  -> Nothing
diff --git a/src/GHC/TypeLits/Extra/Solver/Operations.hs b/src/GHC/TypeLits/Extra/Solver/Operations.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Extra/Solver/Operations.hs
@@ -0,0 +1,37 @@
+module GHC.TypeLits.Extra.Solver.Operations where
+
+-- GHC API
+import Outputable (Outputable (..), (<+>), integer, text)
+import Type       (TyVar)
+
+data ExtraOp
+  = I    Integer
+  | V    TyVar
+  | GCD  ExtraOp ExtraOp
+  | CLog ExtraOp ExtraOp
+  | Exp  ExtraOp ExtraOp
+  deriving Eq
+
+instance Outputable ExtraOp where
+  ppr (I i)      = integer i
+  ppr (V v)      = ppr v
+  ppr (GCD x y)  = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
+  ppr (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
+  ppr (Exp x y)  = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
+
+mergeGCD :: ExtraOp -> ExtraOp -> ExtraOp
+mergeGCD (I i) (I j) = I (gcd i j)
+mergeGCD x     y     = GCD x y
+
+mergeCLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeCLog i (Exp j k)
+  | i == j && (i /= (I 0)) = Just k
+mergeCLog (I i) (I j)
+  | i > 1 && j > 0 = Just (I (ceiling (logBase (fromInteger i :: Double)
+                                      (fromInteger j))))
+  | otherwise      = Nothing
+mergeCLog x y = Just (CLog x y)
+
+mergeExp :: ExtraOp -> ExtraOp -> ExtraOp
+mergeExp (I i) (I j) = I (i^j)
+mergeExp x     y     = Exp x y
diff --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeLits/Extra/Solver/Unify.hs
@@ -0,0 +1,119 @@
+module GHC.TypeLits.Extra.Solver.Unify where
+
+-- external
+import Data.Function (on)
+
+-- GHC API
+import Outputable (Outputable (..), (<+>), ($$), text)
+import TcPluginM  (TcPluginM, tcPluginTrace)
+import TcRnMonad  (Ct)
+import TcTypeNats (typeNatExpTyCon)
+import Type       (TyVar, tcView, mkNumLitTy, mkTyConApp, mkTyVarTy)
+import TyCon      (TyCon)
+import TypeRep    (Type (..), TyLit (..))
+import UniqSet    (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
+
+-- internal
+import GHC.TypeLits.Extra.Solver.Operations
+
+data ExtraDefs = ExtraDefs
+  { gcdTyCon  :: TyCon
+  , clogTyCon :: TyCon
+  }
+
+normaliseNat :: ExtraDefs -> Type -> Maybe ExtraOp
+normaliseNat defs ty | Just ty1 <- tcView ty = normaliseNat defs ty1
+normaliseNat _ (TyVarTy v)          = pure (V v)
+normaliseNat _ (LitTy (NumTyLit i)) = pure (I i)
+normaliseNat defs (TyConApp tc [x,y])
+  | tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x
+                                   <*> normaliseNat defs y
+  | tc == clogTyCon defs = do x' <- normaliseNat defs x
+                              y' <- normaliseNat defs y
+                              mergeCLog x' y'
+  | tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x
+                                     <*> normaliseNat defs y
+  | otherwise = Nothing
+normaliseNat _ _ = Nothing
+
+reifyExtraOp :: ExtraDefs -> ExtraOp -> Type
+reifyExtraOp _    (I i)     = mkNumLitTy i
+reifyExtraOp _    (V v)     = mkTyVarTy v
+reifyExtraOp defs (GCD x y) = mkTyConApp (gcdTyCon defs)
+                                         [reifyExtraOp defs x
+                                         ,reifyExtraOp defs y
+                                         ]
+reifyExtraOp defs (CLog x y) = mkTyConApp (clogTyCon defs)
+                                          [reifyExtraOp defs x
+                                          ,reifyExtraOp defs y
+                                          ]
+reifyExtraOp defs (Exp x y) = mkTyConApp typeNatExpTyCon
+                                         [reifyExtraOp defs x
+                                         ,reifyExtraOp defs y
+                                         ]
+
+
+type ExtraSubst = [SubstItem]
+
+data SubstItem
+  = SubstItem
+  { siVar  :: TyVar
+  , siOP   :: ExtraOp
+  , siNote :: Ct
+  }
+
+instance Outputable SubstItem where
+  ppr si = ppr (siVar si) <+> text " := " <+> ppr (siOP si)
+
+substsExtra :: ExtraSubst -> ExtraOp -> ExtraOp
+substsExtra []     u = u
+substsExtra (si:s) u = substsExtra s (substExtra (siVar si) (siOP si) u)
+
+substExtra :: TyVar -> ExtraOp -> ExtraOp -> ExtraOp
+substExtra _  _ i@(I _)    = i
+substExtra tv e v@(V tv')
+  | tv == tv'              = e
+  | otherwise              = v
+substExtra tv e (GCD x y)  = mergeGCD (substExtra tv e x) (substExtra tv e y)
+substExtra tv e (CLog x y) = case mergeCLog x' y' of
+    Just k  -> k
+    Nothing -> CLog x' y'
+  where
+    x' = substExtra tv e x
+    y' = substExtra tv e y
+substExtra tv e (Exp x y) = mergeExp (substExtra tv e x) (substExtra tv e y)
+
+substsSubst :: ExtraSubst -> ExtraSubst -> ExtraSubst
+substsSubst s = map (\si -> si {siOP = substsExtra s (siOP si)})
+
+-- | Result of comparing two 'SOP' terms, returning a potential substitution
+-- list under which the two terms are equal.
+data UnifyResult
+  = Win             -- ^ Two terms are equal
+  | Lose            -- ^ Two terms are /not/ equal
+  | Draw ExtraSubst -- ^ Two terms are only equal if the given substitution holds
+
+instance Outputable UnifyResult where
+  ppr Win          = text "Win"
+  ppr (Draw subst) = text "Draw" <+> ppr subst
+  ppr Lose         = text "Lose"
+
+unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
+unifyExtra ct u v = do
+  tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v)
+  return (unifyExtra' ct u v)
+
+unifyExtra' :: Ct -> ExtraOp -> ExtraOp -> UnifyResult
+unifyExtra' _ u v
+  | eqFV u v  = if u == v then Win else Lose
+  | otherwise = Draw []
+
+fvOP :: ExtraOp -> UniqSet TyVar
+fvOP (I _)      = emptyUniqSet
+fvOP (V v)      = unitUniqSet v
+fvOP (GCD x y)  = fvOP x `unionUniqSets` fvOP y
+fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y
+fvOP (Exp x y)  = fvOP x `unionUniqSets` fvOP y
+
+eqFV :: ExtraOp -> ExtraOp -> Bool
+eqFV = (==) `on` fvOP
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
new file mode 100644
--- /dev/null
+++ b/tests/ErrorTests.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE DataKinds, TypeOperators #-}
+
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
+
+module ErrorTests where
+
+import GHC.TypeLits
+import GHC.TypeLits.Extra
+import Data.Proxy
+
+testFail1 :: Proxy (GCD 6 8) -> Proxy 4
+testFail1 = id
+
+testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))
+testFail2 = id
+
+testFail3 :: Proxy (CLog 3 10) -> Proxy 2
+testFail3 = id
+
+testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))
+testFail4 = id
+
+testFail5 :: Proxy (CLog 0 4) -> Proxy 100
+testFail5 = id
+
+testFail6 :: Proxy (CLog 1 4) -> Proxy 100
+testFail6 = id
+
+testFail7 :: Proxy (CLog 4 0) -> Proxy 0
+testFail7 = id
+
+testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y
+testFail8 = id
+
+testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y
+testFail9 = id
+
+testFail1Errors =
+  ["Expected type: Proxy (GCD 6 8) -> Proxy 4"
+  ,"Actual type: Proxy 4 -> Proxy 4"
+  ]
+
+testFail2Errors =
+  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"
+  ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"
+  ]
+
+testFail3Errors =
+  ["Expected type: Proxy (CLog 3 10) -> Proxy 2"
+  ,"Actual type: Proxy 2 -> Proxy 2"
+  ]
+
+testFail4Errors =
+  ["Expected type: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"
+  ,"Actual type: Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"
+  ]
+
+testFail5Errors =
+  ["Expected type: Proxy (CLog 0 4) -> Proxy 100"
+  ,"Actual type: Proxy 100 -> Proxy 100"
+  ]
+
+testFail6Errors =
+  ["Expected type: Proxy (CLog 1 4) -> Proxy 100"
+  ,"Actual type: Proxy 100 -> Proxy 100"
+  ]
+
+testFail7Errors =
+  ["Expected type: Proxy (CLog 4 0) -> Proxy 0"
+  ,"Actual type: Proxy 0 -> Proxy 0"
+  ]
+
+testFail8Errors =
+  ["Expected type: Proxy (CLog 1 (1 ^ y)) -> Proxy y"
+  ,"Actual type: Proxy y -> Proxy y"
+  ]
+
+testFail9Errors =
+  ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y"
+  ,"Actual type: Proxy y -> Proxy y"
+  ]
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE DataKinds, TypeOperators, ScopedTypeVariables #-}
+
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
+
+import Data.List (isInfixOf)
+import Control.Exception
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import ErrorTests
+
+import GHC.TypeLits
+import GHC.TypeLits.Extra
+import Data.Proxy
+
+test1 :: Proxy (GCD 6 8) -> Proxy 2
+test1 = id
+
+test2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 10 8))
+test2 = id
+
+test3 :: Proxy (CLog 3 10) -> Proxy 3
+test3 = id
+
+test4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 7))
+test4 = id
+
+test5 :: Proxy (CLog x (x^y)) -> Proxy y
+test5 = id
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "ghc-typelits-natnormalise"
+  [ testGroup "Basic functionality"
+    [ testCase "GCD 6 8 ~ 2" $
+      show (test1 Proxy) @?=
+      "Proxy"
+    , testCase "forall x . GCD 6 8 + x ~ x + GCD 10 8" $
+      show (test2 Proxy) @?=
+      "Proxy"
+    , testCase "CLog 3 10 ~ 3" $
+      show (test3 Proxy) @?=
+      "Proxy"
+    , testCase "forall x . CLog 3 10 + x ~ x + CLog 2 7" $
+      show (test4 Proxy) @?=
+      "Proxy"
+    , testCase "forall x>1 . CLog x (x^y) ~ y" $
+      show (test4 Proxy) @?=
+      "Proxy"
+    ]
+  , testGroup "errors"
+    [ testCase "GCD 6 8 ~ 4" $ testFail1 `throws` testFail1Errors
+    , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors
+    , testCase "CLog 3 10 ~ 2" $ testFail3 `throws` testFail3Errors
+    , testCase "CLog 3 10 + x ~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors
+    , testCase "CLog 0 4 ~ 100" $ testFail5 `throws` testFail5Errors
+    , testCase "CLog 1 4 ~ 100" $ testFail5 `throws` testFail5Errors
+    , testCase "CLog 4 0 ~ 0" $ testFail7 `throws` testFail7Errors
+    , testCase "CLog 1 (1^y) ~ y" $ testFail8 `throws` testFail8Errors
+    , testCase "CLog 0 (0^y) ~ y" $ testFail9 `throws` testFail9Errors
+    ]
+  ]
+
+-- | Assert that evaluation of the first argument (to WHNF) will throw
+-- an exception whose string representation contains the given
+-- substrings.
+throws :: a -> [String] -> Assertion
+throws v xs =
+  (evaluate v >> assertFailure "No exception!")
+  `catch` \ (e :: SomeException) -> if all (`isInfixOf` show e) xs then return () else throw e