diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Adam Gundry
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Adam Gundry nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+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/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/src/Data/UnitsOfMeasure.hs b/src/Data/UnitsOfMeasure.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | See "Data.UnitsOfMeasure.Tutorial" for how to use this module.
+module Data.UnitsOfMeasure
+    ( -- * Type-level units of measure
+      Unit
+    , type Base
+    , type One
+    , type (*:)
+    , type (/:)
+    , type (^:)
+
+      -- * Values indexed by their units
+    , Quantity
+    , unQuantity
+    , zero
+    , mk
+
+      -- * Unit-safe 'Num' operations
+    , (+:)
+    , (*:)
+    , (-:)
+    , negate'
+    , abs'
+    , signum'
+    , fromInteger'
+
+      -- * Unit-safe 'Fractional' operations
+    , (/:)
+    , recip'
+    , fromRational'
+
+      -- * Unit-safe 'Floating' operations
+    , sqrt'
+
+      -- * TH constructor for quantities/units
+    , u
+
+      -- * Declaring units
+    , declareBaseUnit
+    , declareDerivedUnit
+    , declareConvertibleUnit
+
+      -- * Automatic unit conversions
+    , convert
+
+      -- * Pay no attention to that man behind the curtain
+    , MkUnit
+    , Pack
+    , Unpack
+    , KnownUnit
+    ) where
+
+import Data.UnitsOfMeasure.Convert
+import Data.UnitsOfMeasure.Internal
+import Data.UnitsOfMeasure.Show ()
+import Data.UnitsOfMeasure.Singleton
+import Data.UnitsOfMeasure.TH
diff --git a/src/Data/UnitsOfMeasure/Convert.hs b/src/Data/UnitsOfMeasure/Convert.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Convert.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
+
+-- | Experimental support for conversions between units with the same
+-- dimension, for example feet and metres.  This interface is not
+-- necessarily stable!
+--
+-- Rather than defining dimensions explicitly, we pick a "canonical"
+-- base unit for each dimension, and record the conversion ratio
+-- between each base unit and the canonical base unit for its
+-- dimension.  This means we can automatically calculate the
+-- conversion ratio between a unit and its canonical representation,
+-- and hence between any two units that share a dimension (i.e. have
+-- the same canonical representation).
+--
+-- For example, to declare @m@ as a canonical base unit, write:
+--
+-- > instance HasCanonicalBaseUnit "m"
+--
+-- To declare @ft@ as a derived unit, write:
+--
+-- > instance HasCanonicalBaseUnit "ft" where
+-- >   type CanonicalBaseUnit "ft" = "m"
+-- >   conversionBase _ = [u| 3.28 ft/m |]
+--
+-- The above declarations can be written using the 'u' declaration
+-- quasiquoter as @['u'| m, ft = 1 % 3.28 ft/m |]@, or generated
+-- automatically using 'declareConvertibleUnit'.
+--
+-- Now it is possible to 'convert' between quantities whose units
+-- involve feet or metres.  For example:
+--
+-- >>> convert [u| 10m |] :: Quantity Double [u| ft |]
+-- [u| 32.8 ft |]
+-- >>> convert [u| 3ft^2 |] :: Quantity Double [u| m^2 |]
+-- [u| 0.27885187388459254 m^2 |]
+--
+-- You are likely to get unpleasant compiler error messages if you
+-- attempt to convert without the units being fully determined by type
+-- inference, or if the units do not have the same dimension.
+module Data.UnitsOfMeasure.Convert
+    ( convert
+    , ratio
+    , HasCanonicalBaseUnit(..)
+      -- * Constraints
+    , Good
+    , HasCanonical
+    , Convertible
+    , ToCanonicalUnit
+    , MapCBU
+    ) where
+
+import Data.UnitsOfMeasure.Internal
+import Data.UnitsOfMeasure.Singleton
+
+import GHC.Exts ( Constraint )
+import GHC.TypeLits
+
+
+-- | Class to capture the dimensions to which base units belong.  For
+-- a canonical base unit, the class instance can be left empty.
+class (CanonicalBaseUnit (CanonicalBaseUnit b) ~ CanonicalBaseUnit b)
+    => HasCanonicalBaseUnit (b :: Symbol) where
+  -- | The canonical base unit for this base unit.  If @b@ is
+  -- canonical, then @'CanonicalBaseUnit' b = b@.  Otherwise,
+  -- @'CanonicalBaseUnit' b@ must itself be canonical.
+  type CanonicalBaseUnit b :: Symbol
+  type CanonicalBaseUnit b = b
+
+  -- | The conversion ratio between this base unit and its canonical
+  -- base unit.  If @b@ is canonical then this ratio is @1@.
+  conversionBase :: proxy b -> Quantity Rational (Base b /: Base (CanonicalBaseUnit b))
+  default conversionBase :: (b ~ CanonicalBaseUnit b) => proxy b -> Quantity Rational (Base b /: Base b)
+  conversionBase _ = 1
+
+-- | Convert a unit into its canonical representation, where units are
+-- represented syntactically.
+type family MapCBU (u :: UnitSyntax Symbol) :: UnitSyntax Symbol where
+  MapCBU (xs :/ ys) = ListMapCBU xs :/ ListMapCBU ys
+
+type family ListMapCBU (xs :: [Symbol]) :: [Symbol] where
+  ListMapCBU '[]             = '[]
+  ListMapCBU (x ': xs) = CanonicalBaseUnit x ': ListMapCBU xs
+
+-- | This constraint will be satisfied if all the base units in a
+-- syntactically represented unit have associated canonical
+-- representations.
+type family HasCanonical (u :: UnitSyntax Symbol) :: Constraint where
+  HasCanonical (xs :/ ys) = (AllHasCanonical xs, AllHasCanonical ys)
+
+type family AllHasCanonical (xs :: [Symbol]) :: Constraint where
+  AllHasCanonical '[] = ()
+  AllHasCanonical (x ': xs) = (HasCanonicalBaseUnit x, AllHasCanonical xs)
+
+
+conversionRatio :: forall proxy u . Good u
+               => proxy u -> Quantity Rational (u /: Pack (MapCBU (Unpack u)))
+conversionRatio _ = help (unitSing :: SUnit (Unpack u))
+
+help :: forall u . HasCanonical u => SUnit u -> Quantity Rational (Pack u /: Pack (MapCBU u))
+help (SUnit xs ys) = help' xs /: help' ys
+
+help' :: forall xs . AllHasCanonical xs => SList xs -> Quantity Rational (Prod xs /: Prod (ListMapCBU xs))
+help' SNil         = 1
+help' (SCons p xs) = conversionBase p *: help' xs
+
+
+-- | A unit is "good" if all its base units have been defined, and
+-- have associated canonical base units.
+type Good            u = (u ~ Pack (Unpack u), KnownUnit (Unpack u), HasCanonical (Unpack u))
+
+-- | Two units are convertible if they are both 'Good' and they have
+-- the same canonical units (and hence the same dimension).
+type Convertible   u v = (Good u, Good v, ToCanonicalUnit u ~ ToCanonicalUnit v)
+
+-- | Converts a unit to the corresponding canonical representation.
+type ToCanonicalUnit u = Pack (MapCBU (Unpack u))
+
+-- | Automatically convert a quantity with units @u@ so that its units
+-- are @v@, provided @u@ and @v@ have the same dimension.
+convert :: forall a u v . (Fractional a, Convertible u v) => Quantity a u -> Quantity a v
+convert = (ratio (undefined :: proxy' (proxy v)) (undefined :: proxy' (proxy u)) *:)
+
+-- | Calculate the conversion ratio between two units with the same
+-- dimension.  The slightly unusual proxy arguments allow this to be
+-- called using quasiquoters to specify the units, for example
+-- @'ratio' [u| ft |] [u| m |]@.
+ratio :: forall a u v (proxy :: Unit -> *) proxy' .
+         (Fractional a, Convertible u v)
+      => proxy' (proxy u) -> proxy' (proxy v) -> Quantity a (u /: v)
+ratio _ _ = fromRational' $ conversionRatio (undefined :: proxy u) /: conversionRatio (undefined :: proxy v)
diff --git a/src/Data/UnitsOfMeasure/Defs.hs b/src/Data/UnitsOfMeasure/Defs.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Defs.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
+
+-- | This module exports some example definitions of base and derived
+-- units, for demonstration purposes.  In the future, this is likely
+-- to change or be moved to a separate package.
+module Data.UnitsOfMeasure.Defs
+    ( MkUnit
+    ) where
+
+import Data.UnitsOfMeasure
+
+-- The SI base units
+-- http://www.bipm.org/en/measurement-units/
+[u| m, kg, s, A, K, mol, cd |]
+
+-- Some prefixed units
+[u| km = 1000m, g = 0.001 kg |]
+
+-- SI derived units
+-- http://physics.nist.gov/cuu/Units/units.html
+[u| Hz = s^-1
+  , N  = kg m / s^2
+  , Pa = N / m^2
+  , J  = N m
+  , W  = J / s
+  , C  = s A
+  , V  = W / A
+  , F  = C / V
+  , ohm = V / A
+ |]
+
+-- Non-SI units accepted for use with them
+-- http://www.bipm.org/en/publications/si-brochure/chapter4.html
+[u| min = 60 s, h = 3600 s, d, ha, l, t, au |]
+
+-- Some random other units
+[u| ft = 100 % 328 m, in = 0.0254 m, mi = 1609.344 m, mph = mi/h |]
diff --git a/src/Data/UnitsOfMeasure/Internal.hs b/src/Data/UnitsOfMeasure/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Internal.hs
@@ -0,0 +1,248 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module defines the core types used in the @uom-plugin@
+-- library.  Note that importing this module may allow you to violate
+-- invariants, so you should generally work with the safe interface in
+-- "Data.UnitsOfMeasure" instead.
+module Data.UnitsOfMeasure.Internal
+    ( -- * Type-level units of measure
+      Unit
+    , type One
+    , type Base
+    , type (*:)
+    , type (/:)
+    , type (^:)
+
+      -- * Values indexed by their units
+    , Quantity(..)
+    , unQuantity
+    , zero
+    , mk
+
+      -- * Unit-safe 'Num' operations
+    , (+:)
+    , (*:)
+    , (-:)
+    , negate'
+    , abs'
+    , signum'
+    , fromInteger'
+
+      -- * Unit-safe 'Fractional' operations
+    , (/:)
+    , recip'
+    , fromRational'
+
+      -- * Unit-safe 'Floating' operations
+    , sqrt'
+
+      -- * Syntactic representation of units
+    , UnitSyntax(..)
+    , Unpack
+    , Pack
+    , Prod
+
+      -- * Internal
+    , type (~~)
+    , MkUnit
+    ) where
+
+import GHC.Exts (Constraint)
+import GHC.TypeLits (Symbol, Nat, type (-))
+
+-- | (Kind) Units of measure
+data Unit
+
+-- | Dimensionless unit (identity element)
+type family One :: Unit
+#if __GLASGOW_HASKELL__ >= 711
+  where
+#endif
+
+-- | Base unit
+type family Base (b :: Symbol) :: Unit
+#if __GLASGOW_HASKELL__ >= 711
+  where
+#endif
+
+-- | Multiplication for units of measure
+type family (u :: Unit) *: (v :: Unit) :: Unit
+#if __GLASGOW_HASKELL__ >= 711
+  where
+#endif
+
+-- | Division for units of measure
+type family (u :: Unit) /: (v :: Unit) :: Unit
+#if __GLASGOW_HASKELL__ >= 711
+  where
+#endif
+
+-- | Exponentiation (to a positive power) for units of measure;
+-- negative exponents are not yet supported (they require an Integer kind)
+type family (u :: Unit) ^: (n :: Nat)  :: Unit where
+  u ^: 0 = One
+  u ^: 1 = u
+  u ^: n = u *: (u ^: (n-1))
+
+infixl 6 +:, -:
+infixl 7 *:, /:
+infixr 8 ^:
+
+-- | A @Quantity a u@ is represented identically to a value of
+-- underlying numeric type @a@, but with units @u@.
+newtype Quantity a (u :: Unit) = MkQuantity a
+  -- ^ Warning: the 'MkQuantity' constructor allows module invariants
+  -- to be violated, so use it with caution!
+type role Quantity representational nominal
+
+-- These classes work uniformly on the underlying representation,
+-- regardless of the units
+deriving instance Bounded a => Bounded (Quantity a u)
+deriving instance Eq      a => Eq      (Quantity a u)
+deriving instance Ord     a => Ord     (Quantity a u)
+
+-- These classes are not unit-polymorphic, so we have to restrict the
+-- unit index to be dimensionless
+deriving instance (Enum       a, u ~ One) => Enum       (Quantity a u)
+deriving instance (Floating   a, u ~ One) => Floating   (Quantity a u)
+deriving instance (Fractional a, u ~ One) => Fractional (Quantity a u)
+deriving instance (Integral   a, u ~ One) => Integral   (Quantity a u)
+deriving instance (Num        a, u ~ One) => Num        (Quantity a u)
+deriving instance (Real       a, u ~ One) => Real       (Quantity a u)
+deriving instance (RealFloat  a, u ~ One) => RealFloat  (Quantity a u)
+deriving instance (RealFrac   a, u ~ One) => RealFrac   (Quantity a u)
+
+
+-- | Extract the underlying value of a quantity
+unQuantity :: Quantity a u -> a
+unQuantity (MkQuantity x) = x
+
+-- | Zero is polymorphic in its units: this is required because the
+-- 'Num' instance constrains the quantity to be dimensionless, so
+-- @0 :: Quantity a u@ is not well typed.
+zero :: Num a => Quantity a u
+zero = MkQuantity 0
+
+-- | Construct a 'Quantity' from a dimensionless value.  Note that for
+-- numeric literals, the 'Num' and 'Fractional' instances allow them
+-- to be treated as quantities directly.
+mk :: a -> Quantity a One
+mk = MkQuantity
+
+
+-- | Addition ('+') of quantities requires the units to match.
+(+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
+MkQuantity x +: MkQuantity y = MkQuantity (x + y)
+
+-- | Multiplication ('*') of quantities multiplies the units.
+(*:) :: (Num a, w ~~ u *: v) => Quantity a u -> Quantity a v -> Quantity a w
+MkQuantity x *: MkQuantity y = MkQuantity (x * y)
+
+-- | Subtraction ('-') of quantities requires the units to match.
+(-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
+MkQuantity x -: MkQuantity y = MkQuantity (x - y)
+
+-- | Negation ('negate') of quantities is polymorphic in the units.
+negate' :: Num a => Quantity a u -> Quantity a u
+negate' (MkQuantity x) = MkQuantity (negate x)
+
+-- | Absolute value ('abs') of quantities is polymorphic in the units.
+abs' :: Num a => Quantity a u -> Quantity a u
+abs' (MkQuantity x) = MkQuantity (abs x)
+
+-- | The sign ('signum') of a quantity gives a dimensionless result.
+signum' :: Num a => Quantity a u -> Quantity a One
+signum' (MkQuantity x) = MkQuantity (signum x)
+
+-- | Convert an 'Integer' quantity into any 'Integral' type ('fromInteger').
+fromInteger' :: Integral a => Quantity Integer u -> Quantity a u
+fromInteger' (MkQuantity x) = MkQuantity (fromInteger x)
+
+
+-- | Division ('/') of quantities divides the units.
+(/:) :: (Fractional a, w ~~ u /: v) => Quantity a u -> Quantity a v -> Quantity a w
+MkQuantity x /: MkQuantity y = MkQuantity (x / y)
+
+-- | Reciprocal ('recip') of quantities reciprocates the units.
+recip' :: (Fractional a, w ~~ One /: u) => Quantity a u -> Quantity a w
+recip' (MkQuantity x) = MkQuantity (recip x)
+
+-- | Convert a 'Rational' quantity into any 'Fractional' type ('fromRational').
+fromRational' :: Fractional a => Quantity Rational u -> Quantity a u
+fromRational' (MkQuantity x) = MkQuantity (fromRational x)
+
+
+-- | Taking the square root ('sqrt') of a quantity requires its units
+-- to be a square.  Fractional units are not currently supported.
+sqrt' :: (Floating a, w ~~ u ^: 2) => Quantity a w -> Quantity a u
+sqrt' (MkQuantity x) = MkQuantity (sqrt x)
+
+
+-- | Syntactic representation of a unit as a pair of lists of base
+-- units, for example 'One' is represented as @[] ':/' []@ and
+-- @'Base' "m" '/:' 'Base' "s" ^: 2@ is represented as @["m"] ':/' ["s","s"]@.
+data UnitSyntax s = [s] :/ [s]
+
+-- | Pack up a syntactic representation of a unit as a unit.  For example:
+--
+-- @ 'Pack' ([] ':/' []) = 'One' @
+--
+-- @ 'Pack' (["m"] ':/' ["s","s"]) = 'Base' "m" '/:' 'Base' "s" ^: 2 @
+--
+-- This is a perfectly ordinary closed type family.  'Pack' is a left
+-- inverse of 'Unpack' up to the equational theory of units, but it is
+-- not a right inverse (because there are multiple list
+-- representations of the same unit).
+type family Pack (u :: UnitSyntax Symbol) :: Unit where
+  Pack (xs :/ ys) = Prod xs /: Prod ys
+
+-- | Take the product of a list of base units.
+type family Prod (xs :: [Symbol]) :: Unit where
+  Prod '[]       = One
+  Prod (x ': xs) = Base x *: Prod xs
+
+-- | Unpack a unit as a syntactic representation, where the order of
+-- units is deterministic.  For example:
+--
+-- @ 'Unpack' 'One' = [] ':/' [] @
+--
+-- @ 'Unpack' ('Base' "s" '*:' 'Base' "m") = ["m","s"] ':/' [] @
+--
+-- This does not break type soundness because
+-- 'Unpack' will reduce only when the unit is entirely constant, and
+-- it does not allow the structure of the unit to be observed.  The
+-- reduction behaviour is implemented by the plugin, because we cannot
+-- define it otherwise.
+type family Unpack (u :: Unit) :: UnitSyntax Symbol
+#if __GLASGOW_HASKELL__ >= 711
+  where
+#endif
+
+
+-- | This is a bit of a hack, honestly, but a good hack.  Constraints
+-- @u ~~ v@ are just like equalities @u ~ v@, except solving them will
+-- be delayed until the plugin.  This may lead to better inferred types.
+type family (u :: Unit) ~~ (v :: Unit) :: Constraint
+#if __GLASGOW_HASKELL__ >= 711
+  where
+#endif
+
+infix 4 ~~
+
+
+-- | This type family is used for translating unit names (as
+-- type-level strings) into units.  It will be 'Base' for base units
+-- or expand the definition for derived units.
+--
+-- The instances displayed by Haddock are available only if
+-- "Data.UnitsOfMeasure.Defs" is imported.
+type family MkUnit (s :: Symbol) :: Unit
diff --git a/src/Data/UnitsOfMeasure/Plugin.hs b/src/Data/UnitsOfMeasure/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Plugin.hs
@@ -0,0 +1,198 @@
+{-# LANGUAGE CPP #-}
+
+-- | This module defines a typechecker plugin that solves equations
+-- involving units of measure.  To use it, add
+--
+-- > {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
+--
+-- above the module header of your source files, or in the
+-- @ghc-options@ field of your @.cabal@ file.  You do not need to
+-- import this module.
+module Data.UnitsOfMeasure.Plugin
+  ( plugin
+  ) where
+
+import Plugins
+
+import TcEvidence
+import TcRnTypes
+import TcType
+import TcPluginM
+
+import Coercion
+import DataCon
+import Type
+import TyCon
+import TypeRep
+import TysWiredIn
+
+import FastString
+import Outputable
+
+import OccName ( occName, occNameFS, mkTcOcc )
+import Module
+
+import Data.Either
+import Data.List
+
+import Data.UnitsOfMeasure.Plugin.Convert
+import Data.UnitsOfMeasure.Plugin.NormalForm
+import Data.UnitsOfMeasure.Plugin.Unify
+import TcPluginExtras
+
+import GHC.TcPluginM.Extra ( evByFiat, tracePlugin, lookupModule, lookupName )
+
+-- | The plugin that GHC will load when this module is used with the
+-- @-fplugin@ option.
+plugin :: Plugin
+plugin = defaultPlugin { tcPlugin = const $ Just uomPlugin }
+
+uomPlugin :: TcPlugin
+uomPlugin = tracePlugin "uom-plugin" $ TcPlugin { tcPluginInit  = lookupUnitDefs
+                                               , tcPluginSolve = unitsOfMeasureSolver
+                                               , tcPluginStop  = const $ return ()
+                                               }
+
+
+unitsOfMeasureSolver :: UnitDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+unitsOfMeasureSolver uds givens _deriveds []      = do
+    zonked_cts <- mapM zonkCt givens
+    let (unit_givens , _) = partitionEithers $ zipWith foo givens $ map (toUnitEquality uds) zonked_cts
+    case unit_givens of
+      []    -> return $ TcPluginOk [] []
+      (_:_) -> do
+        sr <- simplifyUnits uds $ map snd unit_givens
+        tcPluginTrace "unitsOfMeasureSolver simplified givens only" $ ppr sr
+        return $ case sr of
+          -- Simplified tvs []    evs eqs -> TcPluginOk (map (solvedGiven . fst) unit_givens) []
+          Simplified _    -> TcPluginOk [] []
+          Impossible eq _ -> TcPluginContradiction [fromUnitEquality eq]
+  where
+    foo :: Ct -> Either UnitEquality Ct -> Either (Ct, UnitEquality) Ct
+    foo ct (Left x)    = Left (ct, x)
+    foo _  (Right ct') = Right ct'
+
+    -- solvedGiven ct = (ctEvTerm (ctEvidence ct), ct)
+
+
+unitsOfMeasureSolver uds givens _deriveds wanteds = do
+  xs <- lookForUnpacks uds givens wanteds
+  case null xs of
+   False -> return $ TcPluginOk [] xs
+   True  -> do
+    let (unit_wanteds, _) = partitionEithers $ map (toUnitEquality uds) wanteds
+    case unit_wanteds of
+      []    -> return $ TcPluginOk [] []
+      (_:_) -> do
+        (unit_givens , _) <- partitionEithers . map (toUnitEquality uds) <$> mapM zonkCt givens
+        sr <- simplifyUnits uds unit_givens
+        tcPluginTrace "unitsOfMeasureSolver simplified givens" $ ppr sr
+        case sr of
+          Impossible eq _ -> return $ TcPluginContradiction [fromUnitEquality eq]
+          Simplified ss   -> do sr' <- simplifyUnits uds $ map (substsUnitEquality (simplifySubst ss)) unit_wanteds
+                                tcPluginTrace "unitsOfMeasureSolver simplified wanteds" $ ppr sr'
+                                case sr' of
+                                  Impossible eq _ -> return $ TcPluginContradiction [fromUnitEquality $ substsUnitEquality (simplifyUnsubst ss) eq]
+                                  Simplified ss'  -> TcPluginOk [ (evMagic uds ct, ct) | eq <- simplifySolved ss', let ct = fromUnitEquality eq ]
+                                                         <$> mapM (substItemToCt uds) (filter (isWanted . ctEvidence . siCt) (substsSubst (simplifyUnsubst ss) (simplifySubst ss')))
+
+
+substItemToCt :: UnitDefs -> SubstItem -> TcPluginM Ct
+substItemToCt uds si
+      | isGiven (ctEvidence ct) = newGivenCt loc prd $ evByFiat "units" ty1 ty2
+      | otherwise               = newWantedCt loc prd
+      where
+        prd  = mkEqPred ty1 ty2
+        ty1  = mkTyVarTy (siVar si)
+        ty2  = reifyUnit uds (siUnit si)
+        ct   = siCt si
+        loc  = ctLoc ct
+
+
+lookForUnpacks :: UnitDefs -> [Ct] -> [Ct] -> TcPluginM [Ct]
+lookForUnpacks uds givens wanteds = mapM unpackCt unpacks
+  where
+    unpacks = concatMap collectCt $ givens ++ wanteds
+
+    collectCt ct = collectType ct $ ctEvPred $ ctEvidence ct
+
+    collectType _  (TyVarTy _)      = []
+    collectType ct (AppTy f s)      = collectType ct f ++ collectType ct s
+    collectType ct (TyConApp tc [a])
+      | tc == unpackTyCon uds       = case maybeConstant =<< normaliseUnit uds a of
+                                        Just xs -> [(ct,a,xs)]
+                                        _       -> []
+    collectType ct (TyConApp _ as)  = concatMap (collectType ct) as
+    collectType ct (FunTy t v)      = collectType ct t ++ collectType ct v
+    collectType ct (ForAllTy _ t)   = collectType ct t
+    collectType _  (LitTy _)        = []
+
+    unpackCt (ct,a,xs) = newGivenCt loc (mkEqPred ty1 ty2) (evByFiat "units" ty1 ty2)
+      where
+        ty1 = TyConApp (unpackTyCon uds) [a]
+        ty2 = mkTyConApp (unitSyntaxPromotedDataCon uds)
+               [ typeSymbolKind
+               , foldr promoter nil ys
+               , foldr promoter nil zs ]
+        loc = ctLoc ct
+
+        ys = concatMap (\ (s, i) -> if i > 0 then genericReplicate i s       else []) xs
+        zs = concatMap (\ (s, i) -> if i < 0 then genericReplicate (abs i) s else []) xs
+
+    nil = mkTyConApp (promoteDataCon nilDataCon) [typeSymbolKind]
+
+    promoter x t = mkTyConApp cons_tycon [typeSymbolKind, mkStrLitTy x, t]
+    cons_tycon = promoteDataCon consDataCon
+
+
+-- Extract the unit equality constraints
+toUnitEquality :: UnitDefs -> Ct -> Either UnitEquality Ct
+toUnitEquality uds ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
+    EqPred NomEq t1 t2
+      | isUnitKind uds (typeKind t1) || isUnitKind uds (typeKind t1)
+      , Just u1 <- normaliseUnit uds t1
+      , Just u2 <- normaliseUnit uds t2 -> Left (ct, u1, u2)
+    IrredPred t
+      | Just (tc, [t1,t2]) <- splitTyConApp_maybe t
+      , tc == equivTyCon uds
+      , Just u1 <- normaliseUnit uds t1
+      , Just u2 <- normaliseUnit uds t2 -> Left (ct, u1, u2)
+    _                                   -> Right ct
+
+fromUnitEquality :: UnitEquality -> Ct
+fromUnitEquality (ct, _, _) = ct
+
+
+lookupUnitDefs :: TcPluginM UnitDefs
+lookupUnitDefs = do
+    md <- lookupModule myModule myPackage
+    u <- look md "Unit"
+    b <- look md "Base"
+    o <- look md "One"
+    m <- look md "*:"
+    d <- look md "/:"
+    e <- look md "^:"
+    x <- look md "Unpack"
+    i <- look md "UnitSyntax"
+    c <- look md "~~"
+    return $ UnitDefs u b o m d e x i (getDataCon i ":/") c
+  where
+    getDataCon u s = case [ dc | dc <- tyConDataCons u, occNameFS (occName (dataConName dc)) == fsLit s ] of
+                       [d] -> promoteDataCon d
+                       _   -> error $ "lookupUnitDefs/getDataCon: missing " ++ s
+
+    look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
+    myModule  = mkModuleName "Data.UnitsOfMeasure.Internal"
+    myPackage = fsLit "uom-plugin"
+
+
+-- | Produce bogus evidence for a constraint, including actual
+-- equality constraints and our fake '(~~)' equality constraints.
+evMagic :: UnitDefs -> Ct -> EvTerm
+evMagic uds ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
+    EqPred NomEq t1 t2   -> evByFiat "units" t1 t2
+    IrredPred t
+      | Just (tc, [t1,t2]) <- splitTyConApp_maybe t
+      , tc == equivTyCon uds -> evByFiat "units" t1 t2 `EvCast`
+                                  TcCoercion (mkUnivCo (fsLit "units") Representational (mkTyConApp eqTyCon [typeKind t1, t1, t2]) t)
+    _                    -> error "evMagic"
diff --git a/src/Data/UnitsOfMeasure/Plugin/Convert.hs b/src/Data/UnitsOfMeasure/Plugin/Convert.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Plugin/Convert.hs
@@ -0,0 +1,79 @@
+module Data.UnitsOfMeasure.Plugin.Convert
+  ( UnitDefs(..)
+  , unitKind
+  , isUnitKind
+  , normaliseUnit
+  , reifyUnit
+  ) where
+
+import TyCon
+import Type
+import TypeRep
+import TcType
+
+import Data.List
+
+import Data.UnitsOfMeasure.Plugin.NormalForm
+
+-- | Contains references to the basic unit constructors declared in
+-- "Data.UnitsOfMeasure", as loaded inside GHC.
+data UnitDefs = UnitDefs
+    { unitKindCon   :: TyCon -- ^ The 'Unit' type constructor, to be promoted to a kind
+    , unitBaseTyCon :: TyCon -- ^ The 'Base' data constructor of 'Unit', promoted to a type constructor
+    , unitOneTyCon  :: TyCon -- ^ The 'One'  type family
+    , mulTyCon      :: TyCon -- ^ The '(*:)' type family
+    , divTyCon      :: TyCon -- ^ The '(/:)' type family
+    , expTyCon      :: TyCon -- ^ The '(^:)' type family
+    , unpackTyCon     :: TyCon -- ^ The 'Unpack' type family
+    , unitSyntaxTyCon :: TyCon -- ^ The 'UnitSyntax' type constructor, to be promoted to a kind
+    , unitSyntaxPromotedDataCon :: TyCon -- ^ The data constructor of 'UnitSyntax', promoted to a type constructor
+    , equivTyCon      :: TyCon -- ^ The '(~~)' type family
+    }
+
+-- | 'Unit' promoted to a kind
+unitKind :: UnitDefs -> Kind
+unitKind uds = TyConApp (promoteTyCon $ unitKindCon uds) []
+
+-- | Is this the 'Unit' kind?
+isUnitKind :: UnitDefs -> Kind -> Bool
+isUnitKind uds ty | Just (tc, _) <- tcSplitTyConApp_maybe ty = tc == unitKindCon uds
+                  | otherwise                                = False
+
+
+-- | Try to convert a type to a unit normal form; this does not check
+-- the type has kind 'Unit', and may fail even if it does.
+normaliseUnit :: UnitDefs -> Type -> Maybe NormUnit
+normaliseUnit uds ty | Just ty1 <- tcView ty = normaliseUnit uds ty1
+normaliseUnit _   (TyVarTy v)              = pure $ varUnit v
+normaliseUnit uds (TyConApp tc tys)
+  | tc == unitOneTyCon  uds                = pure one
+  | tc == unitBaseTyCon uds, [x]    <- tys = pure $ baseUnit x
+  | tc == mulTyCon      uds, [u, v] <- tys = (*:) <$> normaliseUnit uds u <*> normaliseUnit uds v
+  | tc == divTyCon      uds, [u, v] <- tys = (/:) <$> normaliseUnit uds u <*> normaliseUnit uds v
+  | tc == expTyCon      uds, [u, n] <- tys, Just i <- isNumLitTy n = (^:) <$> normaliseUnit uds u <*> pure i
+  | isFamilyTyCon tc                       = pure $ famUnit tc tys
+normaliseUnit _ _ = Nothing
+
+
+-- | Convert a unit normal form to a type expression of kind 'Unit'
+reifyUnit :: UnitDefs -> NormUnit -> Type
+reifyUnit uds u | null xs && null ys = oneTy
+                | null ys            = foldr1 times xs
+                | null xs            = oneTy `divide` foldr1 times ys
+                | otherwise          = foldr1 times xs `divide` foldr1 times ys
+  where
+    (pos, neg) = partition ((> 0) . snd) $ ascending u
+    xs = map fromAtom            pos
+    ys = map (fromAtom . fmap negate) neg
+
+    oneTy      = mkTyConApp (unitOneTyCon uds) []
+    times  x y = mkTyConApp (mulTyCon uds) [x, y]
+    divide x y = mkTyConApp (divTyCon uds) [x, y]
+
+    fromAtom (a, n) = pow n (reifyAtom a)
+    pow 1 ty = ty
+    pow n ty = mkTyConApp (expTyCon uds) [ty, mkNumLitTy n]
+
+    reifyAtom (BaseAtom s)    = mkTyConApp (unitBaseTyCon uds) [s]
+    reifyAtom (VarAtom  v)    = mkTyVarTy  v
+    reifyAtom (FamAtom f tys) = mkTyConApp f tys
diff --git a/src/Data/UnitsOfMeasure/Plugin/NormalForm.hs b/src/Data/UnitsOfMeasure/Plugin/NormalForm.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Plugin/NormalForm.hs
@@ -0,0 +1,191 @@
+module Data.UnitsOfMeasure.Plugin.NormalForm
+  ( Atom(..)
+  , BaseUnit
+  , NormUnit
+    -- * Constructors
+  , one
+  , varUnit
+  , baseUnit
+  , famUnit
+  , mkNormUnit
+
+    -- * Algebraic operations
+  , (*:)
+  , (/:)
+  , (^:)
+  , invert
+
+    -- * Predicates
+  , isOne
+  , isConstant
+  , maybeConstant
+  , isBase
+  , divisible
+  , occurs
+
+    -- * Destructors
+  , ascending
+  , leftover
+  , divideExponents
+  , substUnit
+  ) where
+
+import Type
+import TyCon
+import VarSet
+
+import FastString
+import Outputable
+import Util ( thenCmp )
+
+import qualified Data.Foldable as Foldable
+import qualified Data.Map as Map
+import Data.List ( sortBy )
+import Data.Maybe
+import Data.Ord
+
+
+-- | Base units are just represented as strings, for simplicity
+type BaseUnit = FastString
+
+-- | An atom in the normal form is either a base unit, a variable or a
+-- stuck type family application (but not one of the built-in type
+-- families that correspond to group operations).
+data Atom = BaseAtom Type | VarAtom TyVar | FamAtom TyCon [Type]
+
+instance Eq Atom where
+  a == b = compare a b == EQ
+
+-- TODO: using cmpTypes here probably isn't ideal, but does it matter?
+instance Ord Atom where
+  compare (BaseAtom x)    (BaseAtom y)      = cmpType x y
+  compare (BaseAtom _)    _                 = LT
+  compare (VarAtom  _)    (BaseAtom _)      = GT
+  compare (VarAtom  a)    (VarAtom  b)      = compare a b
+  compare (VarAtom  _)    (FamAtom _ _)     = LT
+  compare (FamAtom f tys) (FamAtom f' tys') = compare f f' `thenCmp` cmpTypes tys tys'
+  compare (FamAtom _ _)   _                 = GT
+
+instance Outputable Atom where
+  ppr (BaseAtom b) = ppr b
+  ppr (VarAtom  v) = ppr v
+  ppr (FamAtom tc tys) = ppr tc <> text " " <> ppr tys
+
+
+-- | A unit normal form is a signed multiset of atoms; we maintain the
+-- invariant that the map does not contain any zero values.
+newtype NormUnit = NormUnit { _NormUnit :: Map.Map Atom Integer }
+
+instance Outputable NormUnit where
+    ppr = ppr . Map.map show . _NormUnit
+
+
+-- | The group identity, representing the dimensionless unit
+one :: NormUnit
+one = NormUnit Map.empty
+
+-- | Construct a normalised unit from an atom
+atom :: Atom -> NormUnit
+atom a = NormUnit $ Map.singleton a 1
+
+-- | Construct a normalised unit from a single variable
+varUnit :: TyVar -> NormUnit
+varUnit = atom . VarAtom
+
+-- | Construct a normalised unit from a single base unit
+baseUnit :: Type -> NormUnit
+baseUnit = atom . BaseAtom
+
+-- | Construct a normalised unit from a stuck type family application:
+-- this must not be one of the built-in type families!
+famUnit :: TyCon -> [Type] -> NormUnit
+famUnit tc = atom . FamAtom tc
+
+-- | Construct a normalised unit from a list of atom-exponent pairs
+mkNormUnit :: [(Atom, Integer)] -> NormUnit
+mkNormUnit = mkNormUnitMap . Map.fromList
+
+-- | Construct a normalised unit from an atom-exponent map, applying
+-- the signed multiset invariant
+mkNormUnitMap :: Map.Map Atom Integer -> NormUnit
+mkNormUnitMap =  NormUnit . Map.filter (/= 0)
+
+
+-- | Multiplication of normalised units
+(*:) :: NormUnit -> NormUnit -> NormUnit
+u *: v = mkNormUnitMap $ Map.unionWith (+) (_NormUnit u) (_NormUnit v)
+
+-- | Division of normalised units
+(/:) :: NormUnit -> NormUnit -> NormUnit
+u /: v = u *: invert v
+
+-- | Expontentiation of normalised units
+(^:) :: NormUnit -> Integer -> NormUnit
+_ ^: 0 = one
+u ^: n = NormUnit $ Map.map (* n) $ _NormUnit u
+
+infixl 7 *:, /:
+infixr 8 ^:
+
+-- | Invert a normalised unit
+invert :: NormUnit -> NormUnit
+invert = NormUnit . Map.map negate . _NormUnit
+
+
+-- | Test whether a unit is dimensionless
+isOne :: NormUnit -> Bool
+isOne = Map.null . _NormUnit
+
+-- | Test whether a unit is constant (contains only base literals)
+isConstant :: NormUnit -> Bool
+isConstant = all isBaseLiteral . Map.keys . _NormUnit
+
+-- | Extract the base units if a unit is constant
+maybeConstant :: NormUnit -> Maybe [(BaseUnit, Integer)]
+maybeConstant = mapM getBase . Map.toList . _NormUnit
+  where
+    getBase (BaseAtom ty, i) = (\ b -> (b, i)) <$> isStrLitTy ty
+    getBase _                = Nothing
+
+-- | Test whether an atom is a base unit (but not necessarily a
+-- *literal*, e.g. it could be @Base b@ for some variable @b@)
+isBase :: Atom -> Bool
+isBase (BaseAtom _) = True
+isBase _            = False
+
+-- | Test whether an atom is a literal base unit
+isBaseLiteral :: Atom -> Bool
+isBaseLiteral (BaseAtom ty) = isJust $ isStrLitTy ty
+isBaseLiteral _             = False
+
+-- | Test whether all exponents in a unit are divisble by an integer
+divisible :: Integer -> NormUnit -> Bool
+divisible i = Foldable.all (\ j -> j `rem` i == 0) . _NormUnit
+
+-- | Test whether a type variable occurs in a unit (possibly under a
+-- type family application)
+occurs :: TyVar -> NormUnit -> Bool
+occurs a = any occursAtom . Map.keys . _NormUnit
+  where
+    occursAtom (BaseAtom ty)   = elemVarSet a $ tyVarsOfType ty
+    occursAtom (VarAtom b)     = a == b
+    occursAtom (FamAtom _ tys) = elemVarSet a $ tyVarsOfTypes tys
+
+
+-- | View a unit as a list of atoms in order of ascending absolute exponent
+ascending :: NormUnit -> [(Atom, Integer)]
+ascending = sortBy (comparing (abs . snd)) . Map.toList . _NormUnit
+
+-- | Drop a variable from a unit
+leftover :: TyVar -> NormUnit -> NormUnit
+leftover a = NormUnit . Map.delete (VarAtom a) . _NormUnit
+
+-- | Divide all the exponents in a unit by an integer
+divideExponents :: Integer -> NormUnit -> NormUnit
+divideExponents i = mkNormUnitMap . Map.map (`quot` i) . _NormUnit
+
+-- | Substitute the first unit for the variable in the second unit
+substUnit :: TyVar -> NormUnit -> NormUnit -> NormUnit
+substUnit a v u = case Map.lookup (VarAtom a) $ _NormUnit u of
+                    Nothing -> u
+                    Just i  -> (v ^: i) *: leftover a u
diff --git a/src/Data/UnitsOfMeasure/Plugin/Unify.hs b/src/Data/UnitsOfMeasure/Plugin/Unify.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Plugin/Unify.hs
@@ -0,0 +1,182 @@
+module Data.UnitsOfMeasure.Plugin.Unify
+  ( SubstItem(..)
+  , substsSubst
+  , substsUnitEquality
+  , UnitEquality
+  , SimplifyState(..)
+  , SimplifyResult(..)
+  , simplifyUnits
+  ) where
+
+import FastString
+import Name
+import Outputable
+import TcRnMonad ( Ct, isGiven, ctEvidence )
+import TcType
+import Type
+import Var
+
+import Data.UnitsOfMeasure.Plugin.Convert
+import Data.UnitsOfMeasure.Plugin.NormalForm
+import TcPluginExtras
+import TcPluginM
+
+
+-- | A substitution is essentially a list of (variable, unit) pairs,
+-- but we keep the original 'Ct' that lead to the substitution being
+-- made, for use when turning the substitution back into constraints.
+type TySubst = [SubstItem]
+
+data SubstItem = SubstItem { siVar     :: TyVar
+                           , siUnit    :: NormUnit
+                           , siCt     ::  Ct
+                           }
+
+instance Outputable SubstItem where
+  ppr si = ppr (siVar si) <+> text " := " <+> ppr (siUnit si) <+> text "  {" <+> ppr (siCt si) <+> text "}"
+
+-- | Apply a substitution to a single normalised unit
+substsUnit :: TySubst -> NormUnit -> NormUnit
+substsUnit []     u = u
+substsUnit (si:s) u = substsUnit s (substUnit (siVar si) (siUnit si) u)
+
+-- | Compose two substitutions
+substsSubst :: TySubst -> TySubst -> TySubst
+substsSubst s = map $ \ si -> si { siUnit = substsUnit s (siUnit si) }
+
+substsUnitEquality :: TySubst -> UnitEquality -> UnitEquality
+substsUnitEquality s (ct, u, v) = (ct, substsUnit s u, substsUnit s v)
+
+extendSubst :: SubstItem -> TySubst -> TySubst
+extendSubst si s = si : substsSubst [si] s
+
+
+-- | Possible results of unifying a single pair of units.  In the
+-- non-failing cases, we return a substitution and a list of fresh
+-- variables that were created.
+data UnifyResult = Win [TyVar] TySubst TySubst
+                 | Draw [TyVar] TySubst TySubst
+                 | Lose
+
+instance Outputable UnifyResult where
+  ppr (Win  tvs subst unsubst) = text "Win"  <+> ppr tvs <+> ppr subst <+> ppr unsubst
+  ppr (Draw tvs subst unsubst) = text "Draw" <+> ppr tvs <+> ppr subst <+> ppr unsubst
+  ppr Lose                     = text "Lose"
+
+
+-- | Attempt to unify two normalised units to produce a unifying
+-- substitution.  The 'Ct' is the equality between the non-normalised
+-- (and perhaps less substituted) unit type expressions.
+unifyUnits :: UnitDefs -> UnitEquality -> TcPluginM UnifyResult
+unifyUnits uds (ct, u0, v0) = do tcPluginTrace "unifyUnits" (ppr u0 $$ ppr v0)
+                                 unifyOne uds ct [] [] [] (u0 /: v0)
+
+unifyOne :: UnitDefs -> Ct -> [TyVar] -> TySubst -> TySubst -> NormUnit -> TcPluginM UnifyResult
+unifyOne uds ct tvs subst unsubst u
+      | isOne u           = return $ Win tvs subst unsubst
+      | isConstant u      = return   Lose
+      | otherwise         = tcPluginTrace "unifyOne" (ppr u) >> go [] (ascending u)
+
+      where
+        go :: [(Atom, Integer)] -> [(Atom, Integer)] -> TcPluginM UnifyResult
+        go _  []                       = return $ Draw tvs subst unsubst
+        go ls (at@(VarAtom a, i) : xs) = do
+            tch <- if given_mode then return True else isTouchableTcPluginM a
+            let r = divideExponents (-i) $ leftover a u
+            case () of
+                () | tch && divisible i u -> return $ if occurs a r then Draw tvs subst unsubst
+                                                                    else Win tvs (extendSubst (SubstItem a r ct) subst) unsubst
+                   | tch && any (not . isBase . fst) xs -> do beta <- newUnitVar
+                                                              let subst'   = extendSubst (SubstItem a    (varUnit beta *: r) ct) subst
+                                                                  unsubst' = extendSubst (SubstItem beta (varUnit a    /: r) ct) unsubst
+                                                              unifyOne uds ct (beta:tvs) subst' unsubst' $ substUnit a (varUnit beta *: r) u
+                   | otherwise            -> go (at:ls) xs
+
+        go ls (at@(FamAtom f tys, i) : xs) = do
+          mb <- matchFam f tys
+          case normaliseUnit uds . snd =<< mb of
+            Just v  -> unifyOne uds ct tvs subst unsubst $ mkNormUnit (ls ++ xs) *: v ^: i
+            Nothing -> go (at:ls) xs
+        go ls (at@(BaseAtom  _, _) : xs) = go (at:ls) xs
+
+
+        given_mode = isGiven (ctEvidence ct)
+
+        newUnitVar | given_mode = newSkolemTyVar $ unitKind uds
+                   | otherwise  = newFlexiTyVar  $ unitKind uds
+
+        newSkolemTyVar kind = do
+            x <- newUnique
+            let name = mkSysTvName x (fsLit "beta")
+            return $ mkTcTyVar name kind vanillaSkolemTv
+
+
+type UnitEquality = (Ct, NormUnit, NormUnit)
+
+data SimplifyState
+  = SimplifyState { simplifyFreshVars :: [TyVar]
+                  , simplifySubst     :: TySubst
+                  , simplifyUnsubst   :: TySubst
+                  , simplifySolved    :: [UnitEquality]
+                  , simplifyStuck     :: [UnitEquality]
+                  }
+
+instance Outputable SimplifyState where
+  ppr ss = text "fresh   = " <+> ppr (simplifyFreshVars ss)
+        $$ text "subst   = " <+> ppr (simplifySubst     ss)
+        $$ text "unsubst = " <+> ppr (simplifyUnsubst   ss)
+        $$ text "solved  = " <+> ppr (simplifySolved    ss)
+        $$ text "stuck   = " <+> ppr (simplifyStuck     ss)
+
+initialState :: SimplifyState
+initialState = SimplifyState [] [] [] [] []
+
+data SimplifyResult
+  = Simplified SimplifyState
+  | Impossible { simplifyImpossible :: UnitEquality
+               , simplifyRemaining  :: [UnitEquality]
+               }
+
+instance Outputable SimplifyResult where
+  ppr (Simplified ss)     = text "Simplified" $$ ppr ss
+  ppr (Impossible eq eqs) = text "Impossible" <+> ppr eq <+> ppr eqs
+
+simplifyUnits :: UnitDefs -> [UnitEquality] -> TcPluginM SimplifyResult
+simplifyUnits uds eqs0 = tcPluginTrace "simplifyUnits" (ppr eqs0) >> simples initialState eqs0
+  where
+    simples :: SimplifyState -> [UnitEquality] -> TcPluginM SimplifyResult
+    simples ss [] = return $ Simplified ss
+    simples ss (eq:eqs) = do
+        ur <- unifyUnits uds (substsUnitEquality (simplifySubst ss) eq)
+        tcPluginTrace "unifyUnits result" (ppr ur)
+        case ur of
+          Win  tvs subst unsubst -> let (ss', xs) = win eq tvs subst unsubst ss
+                                    in simples ss' (xs ++ eqs)
+          Draw _   []    _       -> simples (addStuck eq ss) eqs
+          Draw tvs subst unsubst -> let (ss', xs) = draw eq tvs subst unsubst ss
+                                    in simples ss' (xs ++ eqs)
+          Lose                   -> return Impossible { simplifyImpossible = eq
+                                                      , simplifyRemaining  = simplifyStuck ss ++ eqs }
+
+win :: UnitEquality -> [TyVar] -> TySubst -> TySubst -> SimplifyState -> (SimplifyState, [UnitEquality])
+win eq tvs subst unsubst ss =
+  ( SimplifyState { simplifyFreshVars = simplifyFreshVars ss ++ tvs
+                  , simplifySubst     = substsSubst subst (simplifySubst ss) ++ subst
+                  , simplifyUnsubst   = substsSubst unsubst (simplifyUnsubst ss) ++ unsubst
+                  , simplifySolved    = eq : simplifySolved ss
+                  , simplifyStuck     = []
+                  }
+  , simplifyStuck ss )
+
+draw :: UnitEquality -> [TyVar] -> TySubst -> TySubst -> SimplifyState -> (SimplifyState, [UnitEquality])
+draw eq tvs subst unsubst ss =
+  ( SimplifyState { simplifyFreshVars = simplifyFreshVars ss ++ tvs
+                  , simplifySubst     = substsSubst subst (simplifySubst ss) ++ subst
+                  , simplifyUnsubst   = substsSubst unsubst (simplifyUnsubst ss) ++ unsubst
+                  , simplifySolved    = simplifySolved ss
+                  , simplifyStuck     = [eq]
+                  }
+  , simplifyStuck ss )
+
+addStuck :: UnitEquality -> SimplifyState -> SimplifyState
+addStuck eq ss = ss { simplifyStuck = eq : simplifyStuck ss }
diff --git a/src/Data/UnitsOfMeasure/Show.hs b/src/Data/UnitsOfMeasure/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Show.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- | Experimental support for showing units of measure in a pretty
+-- syntax.  This requires the units to be fully determined.
+--
+-- Apart from the definitions below, this module also exports a 'Show'
+-- instance for @'Quantity' a u@, which is re-exported by
+-- "Data.UnitsOfMeasure".
+module Data.UnitsOfMeasure.Show
+    ( showQuantity
+    , showUnit
+    ) where
+
+import Data.UnitsOfMeasure.Internal
+import Data.UnitsOfMeasure.Singleton
+
+import Data.List (intercalate, group)
+
+instance (Show a, KnownUnit (Unpack u)) => Show (Quantity a u) where
+  show x = "[u| " ++ showQuantity x ++ " |]"
+
+-- | Render a quantity nicely, followed by its units:
+--
+-- >>> showQuantity (1 /: [u| 0.1 s / m kg |])
+-- "10.0 kg m / s"
+showQuantity :: forall a u. (Show a, KnownUnit (Unpack u)) => Quantity a u -> String
+showQuantity (MkQuantity x) = show x ++ if s == "1" then "" else ' ':s
+  where s = showUnit (undefined :: proxy u)
+
+-- | Render a unit nicely:
+--
+-- >>> showUnit (undefined :: proxy [u| 1 / s |])
+-- "s^-1"
+showUnit :: forall proxy u . KnownUnit (Unpack u) => proxy u -> String
+showUnit _ = showUnitBits (unitVal (undefined :: proxy' (Unpack u)))
+
+showUnitBits :: UnitSyntax String -> String
+showUnitBits ([] :/ []) = "1"
+showUnitBits (xs :/ []) = showPos xs
+showUnitBits ([] :/ ys) = showNeg ys
+showUnitBits (xs :/ ys) = showPos xs ++ " / " ++ showPos ys
+
+showPos :: [String] -> String
+showPos = intercalate " " . map (\ xs -> showAtom (head xs, length xs)) . group
+
+showNeg :: [String] -> String
+showNeg = intercalate " " . map (\ xs -> showAtom (head xs, negate $ length xs)) . group
+
+showAtom :: (String, Int) -> String
+showAtom (s, 1) = s
+showAtom (s, i) = s ++ "^" ++ show i
diff --git a/src/Data/UnitsOfMeasure/Singleton.hs b/src/Data/UnitsOfMeasure/Singleton.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Singleton.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module defines singleton types for integers and concrete
+-- units.
+module Data.UnitsOfMeasure.Singleton
+    ( -- * Singletons for units
+      SUnit(..)
+    , forgetSUnit
+    , KnownUnit(..)
+    , unitVal
+
+      -- * Singletons for lists
+    , SList(..)
+    , KnownList(..)
+    ) where
+
+import GHC.TypeLits
+
+import Data.UnitsOfMeasure.Internal
+
+
+-- | Singleton type for concrete units of measure represented as lists
+-- of base units
+data SUnit (u :: UnitSyntax Symbol) where
+  SUnit :: SList xs -> SList ys -> SUnit (xs :/ ys)
+
+-- | Singleton type for lists of base units
+data SList (xs :: [Symbol]) where
+  SNil :: SList '[]
+  SCons :: KnownSymbol x => proxy x -> SList xs -> SList (x ': xs)
+
+-- | Extract the runtime syntactic representation from a singleton unit
+forgetSUnit :: SUnit u -> UnitSyntax String
+forgetSUnit (SUnit xs ys) = forgetSList xs :/ forgetSList ys
+
+forgetSList :: SList xs -> [String]
+forgetSList SNil = []
+forgetSList (SCons px xs) = symbolVal px : forgetSList xs
+
+
+-- | A constraint @'KnownUnit' u@ means that @u@ must be a concrete
+-- unit that is statically known but passed at runtime
+class KnownUnit (u :: UnitSyntax Symbol) where
+  unitSing :: SUnit u
+
+instance (KnownList xs, KnownList ys) => KnownUnit (xs :/ ys) where
+  unitSing = SUnit listSing listSing
+
+
+-- | A constraint @'KnownList' xs@ means that @xs@ must be a list of
+-- base units that is statically known but passed at runtime
+class KnownList (xs :: [Symbol]) where
+  listSing :: SList xs
+
+instance KnownList '[] where
+  listSing = SNil
+
+instance (KnownSymbol x, KnownList xs) => KnownList (x ': xs) where
+  listSing = SCons (undefined :: proxy x) listSing
+
+
+-- | Extract the runtime syntactic representation of a 'KnownUnit'
+unitVal :: forall proxy u . KnownUnit u => proxy u -> UnitSyntax String
+unitVal _ = forgetSUnit (unitSing :: SUnit u)
diff --git a/src/Data/UnitsOfMeasure/TH.hs b/src/Data/UnitsOfMeasure/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/TH.hs
@@ -0,0 +1,206 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
+
+-- | Template Haskell utilities for working with units of measure in a
+-- nice syntax.
+module Data.UnitsOfMeasure.TH
+    ( u
+    , declareBaseUnit
+    , declareDerivedUnit
+    , declareConvertibleUnit
+    ) where
+
+import Data.Char
+import Numeric
+import Text.Parse.Units
+
+import Language.Haskell.TH
+import Language.Haskell.TH.Quote
+
+import Data.UnitsOfMeasure.Internal
+import Data.UnitsOfMeasure.Convert
+
+-- | The 'u' quasiquoter may be used to create units or quantities;
+-- its meaning depends on the context:
+--
+-- * in a declaration context, it creates new base and derived units
+--   from a comma-separated list of names with optional definitions,
+--   for example @['u'|kg, m, s, N = kg * m/s^2|]@;
+--
+-- * in a type context, it parses a single unit and converts it into
+--   the corresponding type, so @['u'|m/s|]@ becomes the type
+--   @'Base' "m" /: 'Base' "s"@ of kind 'Unit';
+--
+-- * in an expression context, it can be used to create a 'Quantity'
+--   corresponding to a numeric literal, for example @['u'|42 m|]@ is
+--   an expression of type @'Quantity' 'Integer' ('Base' "m")@,
+--   @['u'|-2.2 m|]@ is an expression of type @'Quantity' 'Double' ('Base' "m")@,
+--   and @['u'|m|]@ alone is a function of type @a -> 'Quantity' a ('Base' "m")@;
+--
+-- * in a pattern context, it can be used to match on a particular
+--   value of a quantity with an 'Integer' or 'Rational'
+--   representation type, for example @f ['u'| 42 m |] = 'True'@ is a
+--   (partial) function of type @'Quantity' 'Integer' [u|m|] -> Bool@.
+--
+u :: QuasiQuoter
+u = QuasiQuoter
+      { quoteExp  = uExp
+      , quotePat  = uPat
+      , quoteType = uType
+      , quoteDec  = uDec
+      }
+
+-- | Parse a unit expression optionally preceded by a literal, and
+-- create a constructor for 'Quantity' with the given units (applied
+-- to the literal if one is present).
+uExp :: String -> Q Exp
+uExp s
+  | Just (ei, s') <- readNumber s = mkLiteral ei =<< parseUnitQ s'
+  | otherwise                     = mkConversion =<< parseUnitQ s
+  where
+    mkLiteral (Left  0) Unity = [| zero |]
+    mkLiteral (Right 0) Unity = [| MkQuantity 0.0 |]
+    mkLiteral ei        expr  = [| (MkQuantity :: a -> Quantity a $(reifyUnit expr))
+                                                                  $(litE (either integerL rationalL ei)) |]
+    mkConversion expr = [|  MkQuantity :: a -> Quantity a $(reifyUnit expr) |]
+
+-- | Parse an integer or rational literal followed by a unit
+-- expression, and create a pattern match on @'Quantity' 'Integer' u@
+-- or @'Quantity' 'Rational' u@.  Unfortunately we cannot easily
+-- support arbitrary representation types.
+uPat :: String -> Q Pat
+uPat s
+  | Just (Left  i, s') <- readNumber s  = mkPat (integerL  i) [t|Integer |] s'
+  | Just (Right r, s') <- readNumber s  = mkPat (rationalL r) [t|Rational|] s'
+  | otherwise                           = error "unable to parse literal"
+  where
+    mkPat l t s' = [p| MkQuantity $(litP l) |] `sigP` [t| Quantity $t $(uType s') |]
+
+-- | Parse a unit expression and convert it into the corresponding type.
+uType :: String -> Q Type
+uType s = reifyUnit =<< parseUnitQ s
+
+parseUnitQ :: String -> Q (UnitExp () String)
+parseUnitQ s = case parseUnit universalSymbolTable s of
+                 Right expr -> return expr
+                 Left  err  -> fail ("unable to parse unit expression \"" ++ s ++ "\": " ++ err)
+
+-- | Convert a unit expression into the corresponding type.
+reifyUnit :: UnitExp () String -> Q Type
+reifyUnit Unity        = [t| One |]
+reifyUnit (Unit _ s)   = [t| MkUnit $(litT (strTyLit s))            |]
+reifyUnit (u `Mult` v) = [t| $(reifyUnit u) *: $(reifyUnit v)       |]
+reifyUnit (u `Div`  v) = [t| $(reifyUnit u) /: $(reifyUnit v)       |]
+reifyUnit (u `Pow`  n) | n >= 0    = [t| $(reifyUnit u) ^: $(litT (numTyLit n)) |]
+                       | otherwise = [t| One /: $(reifyUnit u) ^: $(litT (numTyLit (- n))) |]
+
+
+-- | Parse the string as a mixture of base units and derived units,
+-- and create corresponding 'MkUnit' type instance declarations.
+uDec :: String -> Q [Dec]
+uDec s = case parseUnitDecs s of
+           Just xs -> concat <$> mapM (uncurry declareUnit) xs
+           Nothing -> reportError ("unable to parse unit declarations: " ++ s) >> return []
+
+data UnitDecl = BaseUnit
+              | DefinedUnit    (UnitExp () String)
+              | ConversionUnit Rational String
+
+-- | Parse a comma-separated list of unit declarations, for example:
+--
+-- > kg, m, s, N = kg * m/s^2
+parseUnitDecs :: String -> Maybe [(String, UnitDecl)]
+parseUnitDecs = go
+  where
+    go [] = Just []
+    go (c:xs) | isSpace c || c == ',' = go xs
+    go xs = case span isAlpha xs of
+              ([], _) -> Nothing
+              (u, ys) -> go' u ys
+
+    go' u [] = Just [(u, BaseUnit)]
+    go' u (c:xs) | isSpace c = go' u xs
+    go' u (',':xs) = ((u, BaseUnit) :) <$> go xs
+    go' u ('=':xs) = let (d, ys) = break (== ',') xs
+                     in case readNumber d of
+                          Just (ei, s) -> case parseUnit universalSymbolTable s of
+                                        Right (Unit _ e :: UnitExp () String) -> ((u, ConversionUnit (either fromInteger id ei) e) :) <$> go ys
+                                        _                -> Nothing
+                          _        -> case parseUnit universalSymbolTable d of
+                                        Right e -> ((u, DefinedUnit e) :) <$> go ys
+                                        Left  _ -> Nothing
+    go' _ _        = Nothing
+
+-- | Given a unit name and an optional definition, create an
+-- appropriate instance of the 'MkUnit' type family.
+declareUnit :: String -> UnitDecl -> Q [Dec]
+declareUnit s ud = case ud of
+  BaseUnit           -> [d| type instance MkUnit $(litT (strTyLit s)) = Base $(litT (strTyLit s))
+                            instance HasCanonicalBaseUnit $(litT (strTyLit s))
+                          |]
+  DefinedUnit u      -> [d| type instance MkUnit $(litT (strTyLit s)) = $(reifyUnit u) |]
+  ConversionUnit r t -> [d| type instance MkUnit $(litT (strTyLit s)) = Base $(litT (strTyLit s))
+                            instance HasCanonicalBaseUnit $(litT (strTyLit s)) where
+                              type CanonicalBaseUnit $(litT (strTyLit s)) = $(litT (strTyLit t))
+                              conversionBase _ = MkQuantity $(litE (rationalL (recip r)))
+                          |]
+
+-- | Declare a canonical base unit of the given name, which must not
+-- contain any spaces, e.g.
+--
+-- > declareBaseUnit "m"
+--
+-- produces
+--
+-- > type instance MkUnit "m" = Base "m"
+-- > instance HasCanonicalBaseUnit "m"
+--
+-- This can also be written @['u'| m |]@.
+declareBaseUnit :: String -> Q [Dec]
+declareBaseUnit s = declareUnit s BaseUnit
+
+
+-- | Declare a derived unit with the given name and definition, e.g.
+--
+-- > declareDerivedUnit "N" "kg m / s^2"
+--
+-- produces
+--
+-- > type instance MkUnit "N" = Base "kg" *: Base "m" /: Base "s" ^: 2
+--
+-- This can also be written @['u'| N = kg m / s^2 |]@.
+declareDerivedUnit :: String -> String -> Q [Dec]
+declareDerivedUnit s d = case parseUnit universalSymbolTable d of
+                           Right e -> declareUnit s (DefinedUnit e)
+                           Left _  -> reportError ("unable to parse derived unit: " ++ d) >> return []
+
+-- | Declare a base unit of the given name, which is convertible to
+-- the canonical base unit, e.g.
+--
+-- > declareConvertibleUnit "kilobyte" 1024 "byte"
+--
+-- produces
+--
+-- > type instance MkUnit "kilobyte" = Base "kilobyte"
+-- > instance HasCanonicalBaseUnit "kilobyte" where
+-- >   type CanonicalBaseUnit "kilobyte" = "byte"
+-- >   conversionBase _ = [u| 1 % 1024 kilobyte/byte |]
+--
+-- This can also be written @['u'| kilobyte = 1024 byte |]@.
+-- See "Data.UnitsOfMeasure.Convert" for more information about conversions.
+declareConvertibleUnit :: String -> Rational -> String -> Q [Dec]
+declareConvertibleUnit derived r base = declareUnit derived (ConversionUnit r base)
+
+
+-- | Read either an integer or a rational from a string, if possible,
+-- and return the remainder of the string.
+readNumber :: String -> Maybe (Either Integer Rational, String)
+readNumber s
+  | [(r, s')] <- reads s                = Just (Right r, s')
+  | [(i, s')] <- reads s                = Just (Left i , s')
+  | [(r, s')] <- readSigned readFloat s = Just (Right r, s')
+  | otherwise                           = Nothing
diff --git a/src/Data/UnitsOfMeasure/Tutorial.hs b/src/Data/UnitsOfMeasure/Tutorial.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/UnitsOfMeasure/Tutorial.hs
@@ -0,0 +1,171 @@
+-- | This module gives a brief introduction to the @uom-plugin@
+-- library.
+
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+module Data.UnitsOfMeasure.Tutorial
+  ( -- $tutorial
+  ) where
+
+import Data.UnitsOfMeasure
+
+-- $tutorial
+--
+-- === Prerequisites
+--
+-- To use the @uom-plugin@ library, simply import "Data.UnitsOfMeasure"
+-- and pass the option @-fplugin Data.UnitsOfMeasure.Plugin@ to GHC, for
+-- example by adding the following above the module header of your source
+-- files:
+--
+-- > {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
+--
+-- This will enable the typechecker plugin, which automatically solves
+-- equality constraints between units of measure.  You will also need
+-- some language extensions:
+--
+-- > {-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators #-}
+--
+-- In order to declare new units, you will need:
+--
+-- > {-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+--
+--
+-- === Interactive use
+--
+-- If experimenting with @uom-plugin@ in GHCi you will need to
+-- activate the plugin with the command
+--
+-- >>> :seti -fplugin Data.UnitsOfMeasure.Plugin
+--
+-- otherwise you will get mysterious unsolved constraint errors.  You
+-- will probably also need the extensions:
+--
+-- >>> :seti -XDataKinds -XQuasiQuotes -XTypeOperators
+--
+--
+-- === The 'Unit' kind
+--
+-- Units of measure, such as kilograms or metres per second, are
+-- represented by the abstract kind 'Unit'.  They can be built out of
+-- 'One', 'Base', ('Data.UnitsOfMeasure.Internal.*:'),
+-- ('Data.UnitsOfMeasure.Internal./:') and
+-- ('Data.UnitsOfMeasure.Internal.^:').  Base units are represented as
+-- type-level strings (with kind 'Symbol').  For example,
+--
+-- >>> :kind One
+-- One :: Unit
+--
+-- >>> :kind Base "m" /: Base "s"
+-- Base "m" /: Base "s" :: Unit
+--
+-- The TH quasiquoter 'u' is provided to give a nice syntax for units
+-- (see @Text.Parse.Units@ from the @units-parser@ package for details
+-- of the syntax).  When used in a type, the quasiquoter produces an
+-- expression of kind 'Unit', for example
+--
+-- >>> :kind! [u| m^2 |]
+-- [u| m^2 |] :: Unit
+-- = Base "m" ^: 2
+--
+-- >>> :kind! [u| kg m/s |]
+-- [u|kg m/s|] :: Unit
+-- = (Base "kg" *: Base "m") /: Base "s"
+--
+--
+-- === Declaring base and derived units
+--
+-- Base and derived units need to be declared before use, otherwise
+-- you will get unsolved constraints like @'KnownUnit' ('Unpack' ('MkUnit' "m"))@.
+-- When the TH quasiquoter 'u' is used as in a declaration context, it
+-- creates new base or derived units.  Alternatively,
+-- 'declareBaseUnit' and 'declareDerivedUnit' can be used as top-level
+-- TH declaration splices.  For example:
+--
+-- > declareBaseUnit "m"
+-- > declareDerivedUnit "N" "kg m / s^2"
+-- > [u| kg, s |]
+--
+-- Note that these lines must appear in a module, not GHCi.  For
+-- experimenting interactively, "Data.UnitsOfMeasure.Defs" provides
+-- definitions of common units, but is subject to change.
+--
+--
+-- === Creating quantities
+--
+-- A 'Quantity' is a numeric value annotated with its units.
+-- Quantities can be created using the 'u' quasiquoter in an
+-- expression, for example @[u| 5 m |]@ or @[u| 2.2 m/s^2 |]@.  The
+-- syntax consists of an integer or decimal number, followed by a
+-- unit.
+--
+-- The type of a quantity includes the underlying representation type and
+-- the unit, for example:
+--
+-- > [u| 5 m |] :: Quantity Int (Base "m")
+--
+-- or using the 'u' quasiquoter in the type as well:
+--
+-- > [u| 1.1 m/s |] :: Quantity Double [u| m/s |]
+--
+-- Numeric literals may be used to produce dimensionless quantities
+-- (i.e. those with unit 'One'):
+--
+-- > 2 :: Quantity Int One
+--
+-- The underlying numeric value of a quantity may be extracted with
+-- 'unQuantity':
+--
+-- >>> unQuantity [u| 15 kg |]
+-- 15
+--
+--
+-- === Operations on quantities
+--
+-- The usual arithmetic operators from 'Num' and related typeclasses
+-- are restricted to operating on dimensionless quantities.  Thus
+-- using them directly on quantities with units will result in errors:
+--
+-- >>> 2 * [u| 5 m |]
+--   Couldn't match type ‘Base "m"’ with ‘One’...
+--
+-- >>> [u| 2 m/s |] + [u| 5 m/s |]
+--   Couldn't match type ‘Base "m" /: Base "s"’ with ‘One’...
+--
+-- Instead, "Data.UnitsOfMeasure" provides more general arithmetic
+-- operators including ('+:'), ('-:'), ('*:') and ('/:').  These may
+-- be used to perform unit-safe arithmetic:
+--
+-- >>> 2 *: [u| 5 m |]
+-- [u| 10 m |]
+--
+-- >>> [u| 2 m / s |] +: [u| 5 m / s |]
+-- [u| 7 m / s |]
+--
+-- However, unit errors will be detected by the type system:
+--
+-- >>>  [u| 3 m |] -: [u| 1 s |]
+--   Couldn't match type ‘Base "s"’ with ‘Base "m"’...
+--
+--
+-- === Unit polymorphism
+--
+-- It is easy to work with arbitrary units (type variables of kind
+-- 'Unit') rather than particular choices of unit.  The typechecker
+-- plugin ensures that type inference is well-behaved and
+-- automatically solves equations between units (e.g. making unit
+-- multiplication commutative):
+--
+-- >>> let cube x = x *: x *: x
+-- >>> :t cube
+-- cube :: Num a => Quantity a v -> Quantity a (v ^: 3)
+--
+-- >>> let f x y = (x *: y) +: (y *: x)
+-- >>> :t f
+-- f :: Num a => Quantity a v -> Quantity a u -> Quantity a (u *: v)
+--
+--
+-- == Further reading
+--
+--  * <http://adam.gundry.co.uk/pub/typechecker-plugins/ Paper about uom-plugin>
+--
+--  * <https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker Plugins on the GHC wiki>
diff --git a/src/TcPluginExtras.hs b/src/TcPluginExtras.hs
new file mode 100644
--- /dev/null
+++ b/src/TcPluginExtras.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module TcPluginExtras
+  ( -- * Wrappers
+    newUnique
+  , newWantedCt
+  , newGivenCt
+  ) where
+
+import TcPluginM  ( TcPluginM )
+import TcEvidence ( EvTerm )
+import TcRnTypes  ( mkNonCanonical )
+import TcRnMonad  ( Ct, CtLoc )
+import Type       ( PredType )
+
+import GHC.TcPluginM.Extra
+
+#if __GLASGOW_HASKELL__ < 711
+import Unique     ( Unique )
+import qualified TcRnMonad
+import TcPluginM ( unsafeTcPluginTcM )
+#else
+import TcPluginM ( newUnique )
+#endif
+
+
+#if __GLASGOW_HASKELL__ < 711
+newUnique :: TcPluginM Unique
+newUnique = unsafeTcPluginTcM TcRnMonad.newUnique
+#endif
+
+newWantedCt :: CtLoc -> PredType -> TcPluginM Ct
+newWantedCt loc = fmap mkNonCanonical . newWanted loc
+
+newGivenCt :: CtLoc -> PredType -> EvTerm -> TcPluginM Ct
+newGivenCt loc prd ev = fmap mkNonCanonical $ newGiven loc prd ev
diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs
new file mode 100644
--- /dev/null
+++ b/tests/ErrorTests.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
+module ErrorTests where
+
+import Data.UnitsOfMeasure
+import Data.UnitsOfMeasure.Defs
+
+mismatch1 :: Quantity Double [u| s/m |]
+mismatch1 = [u| 3 m/s |]
+
+mismatch1_errors = [ [ "Couldn't match type ‘Base \"s\" /: Base \"m\"’"
+                     , "with ‘Base \"m\" /: Base \"s\"’" ]
+                   , [ "Couldn't match type ‘Base \"m\" /: Base \"s\"’"
+                     , "with ‘Base \"s\" /: Base \"m\"’" ]
+                   ]
+
+
+mismatch2 = [u| 2 m |] +: ([u| 2 s |] :: Quantity Int [u| s |])
+
+mismatch2_errors = [ [ "Couldn't match type ‘Base \"s\"’ with ‘Base \"m\"’" ]
+                   , [ "Couldn't match type ‘Base \"m\"’ with ‘Base \"s\"’" ]
+                   ]
+
+
+given1 :: ((One *: a) ~ (a *: One)) => Quantity Double a -> Quantity Double [u|kg|]
+given1 = id
+
+given1_errors = [ [ "Could not deduce (a ~ Base \"kg\")"
+                  , "from the context ((One *: a) ~ (a *: One))" ]
+                , [ "Could not deduce: a ~ Base \"kg\""
+                  , "from the context: (One *: a) ~ (a *: One)" ]
+                ]
+
+
+given2 :: ((One *: a) ~ (b *: One)) => Quantity Double a -> Quantity Double [u|kg|]
+given2 = id
+
+given2_errors = [ [ "Could not deduce (a ~ Base \"kg\")"
+                  , "from the context ((One *: a) ~ (b *: One))" ]
+                , [ "Could not deduce: a ~ Base \"kg\""
+                  , "from the context: (One *: a) ~ (b *: One)" ]
+                ]
+
+
+given3 :: ((a ^: 2) ~ (b ^: 3)) => Quantity Integer b -> Quantity Integer a
+given3 _ = [u| 3 s |]
+
+given3_errors = [ [ "Could not deduce (a ~ Base \"s\")"
+                  , "from the context ((a ^: 2) ~ (b ^: 3))" ]
+                , [ "Could not deduce: a ~ Base \"s\""
+                  , "from the context: (a ^: 2) ~ (b ^: 3)" ]
+                ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests.hs
@@ -0,0 +1,184 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
+
+import Data.UnitsOfMeasure
+import Data.UnitsOfMeasure.Convert
+import Data.UnitsOfMeasure.Defs ()
+import Data.UnitsOfMeasure.Show
+
+import Control.Exception
+import Data.List
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import ErrorTests
+
+
+-- Declarations
+declareBaseUnit "byte"
+declareDerivedUnit "bps" "byte / s"
+declareConvertibleUnit "kilobyte" 1024 "byte"
+
+
+-- Some basic examples
+
+myMass :: Quantity Double (Base "kg")
+myMass = [u| 65 kg |]
+
+gravityOnEarth :: Quantity Double [u| m/s^2 |]
+gravityOnEarth = [u| 9.808 m/(s*s) |]
+
+forceOnGround :: Quantity Double [u| N |]
+forceOnGround = gravityOnEarth *: myMass
+
+inMetresPerSecond :: a -> Quantity a [u| m/s |]
+inMetresPerSecond = [u| m/s |]
+
+attract (m1 :: Quantity a [u| kg |]) (m2 :: Quantity a [u| kg |]) (r :: Quantity a [u| m |])
+    = _G *: m1 *: m2 /: (r *: r) :: Quantity a [u| N |]
+  where
+    _G = [u| 6.67384e-11 N*m^2/kg^2 |]
+
+sum' xs = foldr (+:) zero xs
+mean xs = sum' xs /: mk (genericLength xs)
+
+foo x y = x *: y +: y *: x
+
+foo' :: Num a => Quantity a u -> Quantity a v -> Quantity a (u *: v)
+foo' = foo
+
+
+-- Check that the abelian group laws hold
+
+associativity :: Quantity a (u *: (v *: w)) -> Quantity a ((u *: v) *: w)
+associativity = id
+
+commutativity :: Quantity a (u *: v) -> Quantity a (v *: u)
+commutativity = id
+
+unit :: Quantity a (u *: One) -> Quantity a u
+unit = id
+
+inverse :: Quantity a (u *: (One /: u)) -> Quantity a One
+inverse = id
+
+inverse2 :: proxy b -> Quantity a (Base b /: Base b) -> Quantity a One
+inverse2 _ = id
+
+
+-- Gingerly now...
+
+-- w^-2 ~ kg^-2  =>  w ~ kg
+f :: (One /: (w ^: 2)) ~ (One /: [u| kg^2 |])  => Quantity a w -> Quantity a [u| kg |]
+f = id
+
+-- u ~ v * w, v^2 ~ v  =>  u ~ w
+g :: (u ~ (v *: w), (v ^: 2) ~ v) => Quantity a u -> Quantity a w
+g = id
+
+-- a*a ~ 1  =>  a ~ 1
+givens :: ((a *: a) ~ One) => Quantity Double a -> Quantity Double One
+givens = id
+
+-- a^2 ~ b^3, b^6 ~ 1 => a ~ 1
+givens2 :: ((a ^: 2) ~ (b ^: 3), (b ^: 6) ~ One) => Quantity Double a -> Quantity Double One
+givens2 = id
+
+-- a^2 ~ b^3, b^37 ~ 1 => b ~ 1
+givens3 :: ((a ^: 2) ~ (b ^: 3), (b ^: 37) ~ One) => Quantity Double b -> Quantity Double One
+givens3 = id
+
+-- in baf, c is uniquely determined to be a^3 (or b^2)
+baz :: (a ~ (c ^: 3), b ~ (c ^: 2)) => Quantity Double a -> Quantity Double b -> Quantity Double c -> Int
+baz _ _ _ = 3
+baf :: ((a ^: 2) ~ (b ^: 3)) => Quantity Double a -> Quantity Double b -> Int
+baf qa qb = baz qa qb undefined
+
+
+-- Miscellaneous bits and bobs
+
+-- Inferring this type used to lead to unit equations with occur-check
+-- failures, because it involves things like Pack (Unpack u) ~ u
+z q = convert q
+
+-- Pattern splices are supported, albeit with restricted types
+patternSplice [u| 2 m |] [u| 0.0 kg / s |] = True
+patternSplice [u| 1 m |] [u| 0.1 kg / s |] = True
+patternSplice _          _                 = False
+
+-- Andrew's awkward generalisation example is accepted only with a
+-- type signature, even with NoMonoLocalBinds
+tricky :: forall a u . Num a => Quantity a u -> (Quantity a (u *: Base "m"), Quantity a (u *: Base "kg"))
+tricky x = let f :: Quantity a v -> Quantity a (u *: v)
+               f = (x *:)
+           in (f [u| 3 m |], f [u| 5 kg |])
+
+
+-- Test that basic constraints involving exponentiation work
+pow :: Quantity a (u *: (v ^: i)) -> Quantity a ((v ^: i) *: u)
+pow = id
+
+
+-- Runtime testsuite
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "uom-plugin"
+  [ testGroup "Showing constants"
+    [ testCase "show 3m"                 $ show [u| 3 m |]                @?= "[u| 3 m |]"
+    , testCase "show 3m/s"               $ show [u| 3 m/s |]              @?= "[u| 3 m / s |]"
+    , testCase "show 3.2 s^2"            $ show [u| 3.2 s^2 |]            @?= "[u| 3.2 s^2 |]"
+    , testCase "show 3.0 kg m^2 / m s^2" $ show [u| 3.0 kg m^2 / m s^2 |] @?= "[u| 3.0 kg m / s^2 |]"
+    , testCase "show 1"                  $ show (mk 1)                    @?= "[u| 1 |]"
+    , testCase "show 1 s^-1"             $ show [u| 1 s^-1 |]             @?= "[u| 1 s^-1 |]"
+    , testCase "show 2 1 / kg s"         $ show [u| 2 1 / kg s |]         @?= "[u| 2 kg^-1 s^-1 |]"
+    , testCase "show (1 % 2) kg"         $ show [u| 1 % 2 kg |]           @?= "[u| 0.5 kg |]"
+    ]
+  , testGroup "Basic operations"
+    [ testCase "2 + 2"                   $ [u| 2 s |] +: [u| 2 s |]        @?= [u| 4 s |]
+    , testCase "in m/s"                  $ inMetresPerSecond 5             @?= [u| 5 m/s |]
+    , testCase "mean"                    $ mean [ [u| 2 N |], [u| 4 N |] ] @?= [u| 3 N |]
+    , testCase "tricky generalisation"   $ tricky [u| 2 s |]               @?= ([u| 6 m s |], [u| 10 kg s |])
+    , testCase "polymorphic zero"        $ [u| 0 |] @?= [u| 0 m |]
+    , testCase "polymorphic frac zero"   $ [u| 0.0 |] @?= [u| 0.0 N / m |]
+    ]
+  , testGroup "showQuantity"
+    [ testCase "myMass"         $ showQuantity myMass         @?= "65.0 kg"
+    , testCase "gravityOnEarth" $ showQuantity gravityOnEarth @?= "9.808 m / s^2"
+    , testCase "forceOnGround"  $ showQuantity forceOnGround  @?= "637.52 kg m / s^2"
+    ]
+  , testGroup "convert"
+    [ testCase "10m in ft"     $ convert [u| 10m |]   @?= [u| 32.8 ft |]
+    , testCase "5 km^2 in m^2" $ convert [u| 5km^2 |] @?= [u| 5000000 m m |]
+    , testCase "ratio"         $ show (ratio [u| ft |] [u| m |]) @?= "[u| 3.28 ft / m |]"
+    ]
+  , testGroup "errors"
+    [ testCase "s/m ~ m/s"            $ mismatch1 `throws` mismatch1_errors
+    , testCase "m + s"                $ mismatch2 `throws` mismatch2_errors
+    , testCase "a ~ a  =>  a ~ kg"    $ given1 undefined `throws` given1_errors
+    , testCase "a ~ b  =>  a ~ kg"    $ given2 undefined `throws` given2_errors
+    , testCase "a^2 ~ b^3  =>  a ~ s" $ given3 undefined `throws` given3_errors
+    ]
+  ]
+
+
+-- | Assert that evaluation of the first argument (to WHNF) will throw
+-- an exception whose string representation contains one of the given
+-- lists of substrings.
+throws :: a -> [[String]] -> Assertion
+throws v xs =
+    (evaluate v >> assertFailure "No exception!")
+  `catch` \ (e :: SomeException) -> if any (all (`isInfixOf` show e)) xs then return () else throw e
diff --git a/uom-plugin.cabal b/uom-plugin.cabal
new file mode 100644
--- /dev/null
+++ b/uom-plugin.cabal
@@ -0,0 +1,61 @@
+name:                uom-plugin
+version:             0.1.0.0
+synopsis:            Units of measure as a GHC typechecker plugin
+category:            Type System
+description:         A prototype typechecker plugin for GHC with support for units of measure
+license:             BSD3
+license-file:        LICENSE
+author:              Adam Gundry <adam@well-typed.com>
+maintainer:          Adam Gundry <adam@well-typed.com>
+homepage:            https://github.com/adamgundry/uom-plugin
+bug-reports:         https://github.com/adamgundry/uom-plugin/issues
+stability:           experimental
+copyright:           Copyright (c) 2014-2015, Adam Gundry
+build-type:          Simple
+cabal-version:       >=1.10
+description:
+
+    The @uom-plugin@ library adds support for units of measure to GHC
+    using the new experimental facility for typechecker plugins, which
+    is available in GHC 7.10 and later.  See
+    "Data.UnitsOfMeasure.Tutorial" for an introduction to the library.
+
+source-repository head
+  type:     git
+  location: https://github.com/adamgundry/uom-plugin.git
+
+library
+  exposed-modules:     Data.UnitsOfMeasure,
+                       Data.UnitsOfMeasure.Convert,
+                       Data.UnitsOfMeasure.Defs,
+                       Data.UnitsOfMeasure.Internal,
+                       Data.UnitsOfMeasure.Plugin,
+                       Data.UnitsOfMeasure.Show,
+                       Data.UnitsOfMeasure.Singleton,
+                       Data.UnitsOfMeasure.Tutorial
+  other-modules:       Data.UnitsOfMeasure.Plugin.Convert,
+                       Data.UnitsOfMeasure.Plugin.NormalForm,
+                       Data.UnitsOfMeasure.Plugin.Unify,
+                       Data.UnitsOfMeasure.TH,
+                       TcPluginExtras
+  other-extensions:    TemplateHaskell
+  build-depends:       base >=4.7 && <5,
+                       ghc >= 7.9 && <7.12,
+                       ghc-tcplugins-extra >=0.1 && <0.2,
+                       template-haskell >=2.9 && <2.12,
+                       containers >=0.5 && <0.6,
+                       units-parser >=0.1 && <0.2
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall -fno-warn-unticked-promoted-constructors
+
+test-suite test-uom-plugin
+  type:                exitcode-stdio-1.0
+  main-is:             Tests.hs
+  other-modules:       ErrorTests
+  other-extensions:    TemplateHaskell
+  build-depends:       base, uom-plugin,
+                       tasty >=0.10 && <0.11, tasty-hunit >=0.9 && <0.10
+  hs-source-dirs:      tests
+  default-language:    Haskell2010
+  ghc-options:         -O0