diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for algebra-checkers
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Sandy Maguire (c) 2020
+
+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 Sandy Maguire 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,92 @@
+# algebra-checkers
+
+[![Build Status](https://travis-ci.org/isovector/algebra-checkers.svg?branch=master)](https://travis-ci.org/isovector/algebra-checkers)
+
+## Dedication
+
+> "Any fool can make a rule, and any fool will mind it."
+>
+> Henry David Thoreau
+
+
+## Overview
+
+`algebra-checkers` is a little library for testing algebraic laws. For example,
+imagine we're writing an ADT:
+
+```haskell
+data Foo a
+instance Semigroup (Foo a)
+instance Monoid (Foo a)
+
+data Key
+
+
+get :: Key -> Foo a -> a
+get = undefined
+
+set :: Key -> a -> Foo a -> Foo a
+set = undefined
+```
+
+Let's say we expect the lens laws to hold for `get` and `set`, as well for `set`
+to be a monoid homomorphism. We can express those facts to `algebra-checkers`
+and have it generate tests for us:
+
+```haskell
+lawTests :: [Property]
+lawTests = $(testModel [e| do
+
+law "set/set"
+    (set i x' (set i x s) == set i x' s)
+
+law "set/get"
+    (set i (get i s) s == s)
+
+law "get/set"
+    (get i (set i x s) == x)
+
+homo @Monoid
+    (\s -> set i x s)
+
+|])
+```
+
+Furthermore, `algebra-checkers` will generate tests to show that these laws are
+confluent. We can run these tests via `quickCheck lawTests`.
+
+If we use the `theoremsOf` function instead of `testModel`, `algebra-checkers`
+will dump out all the additional theorems it has proven about our algebra. This
+serves as a good sanity check:
+
+```
+Theorems:
+
+• set i x' (set i x s) = set i x' s (definition of "set/set")
+• set i (get i s) s = s (definition of "set/get")
+• get i (set i x s) = x (definition of "get/set")
+• set i x mempty = mempty (definition of "set:Monoid:mempty")
+• set i x (s1 <> s2) = set i x s1 <> set i x s2
+    (definition of "set:Monoid:<>")
+• set i1 (get i1 (set i1 x1 s1)) s1 = set i1 x1 s1
+    (implied by "set/get" and "set/set")
+• set i1 (get i1 (s12 <> s22)) s12 <> set i1 (get i1 (s12 <> s22)) s22
+        = s12 <> s22
+    (implied by "set/get" and "set:Monoid:<>")
+• set i1 x'2 (set i1 x1 s11 <> set i1 x1 s21)
+        = set i1 x'2 (s11 <> s21)
+    (implied by "set/set" and "set:Monoid:<>")
+• get i1 (set i1 x1 s11 <> set i1 x1 s21) = x1
+    (implied by "get/set" and "set:Monoid:<>")
+
+
+Contradictions:
+
+• get i1 mempty = x1
+    the variable x1 is undetermined
+    (implied by "get/set" and "set:Monoid:mempty")
+```
+
+Uh oh! Look at that! This contradiction is  clearly a bogus theorem, which lets
+us know that "get/set" and "set mempty" are nonconfluent with one another!
+
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/algebra-checkers.cabal b/algebra-checkers.cabal
new file mode 100644
--- /dev/null
+++ b/algebra-checkers.cabal
@@ -0,0 +1,58 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: b82e33c00a44f13bb2653ad3fb8f750bc17d16b2c3c2c62c4aa0efed07997433
+
+name:           algebra-checkers
+version:        0.1.0.0
+synopsis:       Model and test API surfaces algebraically
+description:    Please see the README on GitHub at <https://github.com/isovector/algebra-checkers#readme>
+category:       Model
+homepage:       https://github.com/isovector/algebra-checkers#readme
+bug-reports:    https://github.com/isovector/algebra-checkers/issues
+author:         Sandy Maguire
+maintainer:     sandy@sandymaguire.me
+copyright:      2020 Sandy Maguire
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/isovector/algebra-checkers
+
+library
+  exposed-modules:
+      AlgebraCheckers
+  other-modules:
+      AlgebraCheckers.Homos
+      AlgebraCheckers.Patterns
+      AlgebraCheckers.Ppr
+      AlgebraCheckers.Suggestions
+      AlgebraCheckers.Theorems
+      AlgebraCheckers.TH
+      AlgebraCheckers.Types
+      AlgebraCheckers.Unification
+  hs-source-dirs:
+      src
+  ghc-options: -Wall
+  build-depends:
+      QuickCheck >=2.10.1 && <3
+    , ansi-terminal >=0.10.3
+    , base >=4.7 && <5
+    , checkers >=0.5.5
+    , containers >=0.5.10.2
+    , groups >=0.4.1.0
+    , mtl >=2.2.2 && <3
+    , pretty >=1.1.3.3 && <2
+    , syb >=0.7
+    , template-haskell >=2.12.0.0 && <3
+    , th-instance-reification >=0.1.5
+    , transformers >=0.5.2.0
+  default-language: Haskell2010
diff --git a/src/AlgebraCheckers.hs b/src/AlgebraCheckers.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers.hs
@@ -0,0 +1,14 @@
+module AlgebraCheckers
+  ( -- * Model Checking
+    testModel
+  , theoremsOf
+
+    -- * Modeling Tools
+  , law
+  , homo
+  , notDodgy
+  ) where
+
+import AlgebraCheckers.Patterns
+import AlgebraCheckers.TH
+
diff --git a/src/AlgebraCheckers/Homos.hs b/src/AlgebraCheckers/Homos.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Homos.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
+
+module AlgebraCheckers.Homos where
+
+import           AlgebraCheckers.Types
+import           AlgebraCheckers.Unification
+import           Control.Arrow (second)
+import           Data.Group
+import           Data.List (foldl')
+import qualified Data.Map as M
+import           Data.Maybe
+import           Language.Haskell.TH hiding (ppr, Arity)
+
+#if __GLASGOW_HASKELL__ <= 802
+import           Data.Semigroup
+#endif
+
+
+appHead :: Exp -> Maybe Name
+appHead = fmap fst . splitApps
+
+splitApps :: Exp -> Maybe (Name, [Exp])
+splitApps (VarE n)         = Just (n, [])
+splitApps (ConE n)         = Just (n, [])
+splitApps (AppE f e)       = fmap (second (++ [e])) $ splitApps f
+splitApps (InfixE e1 f e2) =
+  fmap (second (\e -> e ++ maybeToList e1 ++ maybeToList e2)) $ splitApps f
+splitApps _                = Nothing
+
+aritySize :: Arity -> Int
+aritySize Binary     = 2
+aritySize (Prefix n) = n
+
+makeHomo :: Name -> [(Name, Arity)] -> Exp -> [Law LawSort]
+makeHomo ty ops (LamE [VarP name] body) =
+  let app_head = maybe "<expr>" nameBase $ appHead body
+      homo_name = nameBase ty
+      hs = fmap (UnboundVarE . mkName . (nameBase name ++) . show)
+                [1 .. maximum $ fmap (aritySize . snd) ops]
+      mk_lawname fn =
+        mconcat
+          [ app_head, ":", homo_name, ":", nameBase fn ]
+   in flip fmap ops $ \(fn_name, arity) ->
+        mkHomo name hs body (mk_lawname fn_name) (VarE fn_name) arity
+makeHomo _ _ _ = error "monoidal homomorphism needs a lambda"
+
+
+mkHomo :: Name -> [Exp] -> Exp -> String -> Exp -> Arity -> NamedLaw
+mkHomo name vars body law_name fn Binary =
+  case vars of
+    (v1:v2:_) ->
+      let replace x = rebindVars (M.singleton name x) body
+       in Law (LawName law_name)
+              (replace $ InfixE (Just v1) fn (Just v2))
+              (InfixE (Just $ replace v1)
+                      fn
+                      (Just $ replace v2))
+    _ -> error "not enough args to mkHomo"
+mkHomo name all_vars body law_name fn (Prefix n)=
+  let replace x = rebindVars (M.singleton name x) body
+      vars = take n all_vars
+   in Law (LawName law_name)
+          (replace $ foldl' AppE fn vars)
+          (foldl' AppE fn $ fmap replace vars)
+
+
+knownHomos :: Name -> [(Name, Arity)]
+knownHomos nm
+  | nm == ''Semigroup
+        = [ ('(<>),   Binary) ]
+  | nm == ''Monoid
+        = [ ('mempty, Prefix 0)
+          , ('(<>),   Binary)
+          ]
+  | nm == ''Group
+        = [ ('invert, Prefix 1) ]
+  | nm == ''Eq
+        = [ ('(==), Binary) ]
+  | nm == ''Ord
+        = [ ('compare, Prefix 2) ]
+  | otherwise = error $ "unsupported homo type " ++ show nm
+
diff --git a/src/AlgebraCheckers/Patterns.hs b/src/AlgebraCheckers/Patterns.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Patterns.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE ViewPatterns          #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module AlgebraCheckers.Patterns where
+
+import Language.Haskell.TH hiding (ppr, Arity)
+
+pattern NotDodgyParens :: Exp -> Exp -> Stmt
+pattern NotDodgyParens exp1 exp2 <- NoBindS
+  (      VarE ((==) 'notDodgy -> True)
+  `AppE` (InfixE (Just exp1)
+                 (VarE ((==) '(==) -> True))
+                 (Just exp2)
+         )
+  )
+
+pattern NotDodgyDollar :: Exp -> Exp -> Stmt
+pattern NotDodgyDollar exp1 exp2 <- NoBindS
+  (InfixE
+    (Just ( VarE ((==) 'notDodgy -> True)))
+    (VarE ((==) '($) -> True))
+    (Just (InfixE (Just exp1)
+                  (VarE ((==) '(==) -> True))
+                  (Just exp2)
+          )
+    )
+  )
+
+matchNotDodgy :: Stmt -> Maybe (Exp, Exp)
+matchNotDodgy (NotDodgyParens exp1 exp2) = Just (exp1, exp2)
+matchNotDodgy (NotDodgyDollar exp1 exp2) = Just (exp1, exp2)
+matchNotDodgy _ = Nothing
+
+pattern NotDodgyDef :: Exp -> Exp -> Stmt
+pattern NotDodgyDef exp1 exp2 <- (matchNotDodgy -> Just (exp1, exp2))
+
+
+pattern LawParens :: String -> Exp -> Exp -> Stmt
+pattern LawParens lawname exp1 exp2 <- NoBindS
+  (      VarE ((==) 'law -> True)
+  `AppE` LitE  (StringL lawname)
+  `AppE` (InfixE (Just exp1)
+                 (VarE ((==) '(==) -> True))
+                 (Just exp2)
+         )
+  )
+
+pattern LawDollar :: String -> Exp -> Exp -> Stmt
+pattern LawDollar lawname exp1 exp2 <- NoBindS
+  (InfixE
+    (Just (  VarE ((==) 'law -> True)
+      `AppE` LitE  (StringL lawname)))
+    (VarE ((==) '($) -> True))
+    (Just (InfixE (Just exp1)
+                  (VarE ((==) '(==) -> True))
+                  (Just exp2)
+          )
+    )
+  )
+
+matchLaw :: Stmt -> Maybe (String, Exp, Exp)
+matchLaw (LawParens name exp1 exp2) = Just (name, exp1, exp2)
+matchLaw (LawDollar name exp1 exp2) = Just (name, exp1, exp2)
+matchLaw _ = Nothing
+
+pattern LawDef :: String -> Exp -> Exp -> Stmt
+pattern LawDef name exp1 exp2 <- (matchLaw -> Just (name, exp1, exp2))
+
+
+pattern HomoParens :: Name -> Exp -> Stmt
+pattern HomoParens ty expr <- NoBindS
+  (      (VarE ((==) 'homo -> True) `AppTypeE` ConT ty)
+  `AppE` expr
+  )
+
+pattern HomoDollar :: Name -> Exp -> Stmt
+pattern HomoDollar ty expr <- NoBindS
+  (InfixE
+    (Just ((VarE ((==) 'homo -> True) `AppTypeE` ConT ty)))
+    (VarE ((==) '($) -> True))
+    (Just expr)
+  )
+
+matchHomo :: Stmt -> Maybe (Name, Exp)
+matchHomo (HomoParens ty expr) = Just (ty, expr)
+matchHomo (HomoDollar ty expr) = Just (ty, expr)
+matchHomo _ = Nothing
+
+
+pattern HomoDef :: Name -> Exp -> Stmt
+pattern HomoDef ty expr <- (matchHomo -> Just (ty, expr))
+
+
+------------------------------------------------------------------------------
+-- | Asserts that an algebraic law must hold. This function /must/ be called
+-- only in the context of either 'AlgebraCheckers.testModel' or
+-- 'AlgebraCheckers.theoremsOf'.
+--
+-- Any variables that appear in the 'Bool' parameter are considered to be
+-- metavariables, and will be varied in the resulting property test.
+--
+-- The 'Bool' parameter /must/ be an expression of the form @exp1 '==' exp2@
+--
+-- ==== __Examples__
+--
+-- @'law' "set/get" $ set x (get x s) '==' s@
+--
+-- @'law' "set/set" (set x' (set x s) '==' set x' s)@
+law
+    :: String  -- ^ Name
+    -> Bool    -- ^ Law. /This is not any ordinary 'Bool'!/ See the documentation
+               -- on 'law' for more information.
+    -> law
+law =
+  error "law may be called only inside of a call to testModel or theoremsOf"
+
+
+------------------------------------------------------------------------------
+-- | Convinces 'AlgebraCheckers.theoremsOf' that the following law is not dodgy,
+-- preventing it from appearing in the dodgy theorems list.
+--
+-- This function does not introduce a new law.
+--
+-- This function /must/ be called only in the context of either
+-- 'AlgebraCheckers.testModel' or 'AlgebraCheckers.theoremsOf'.
+notDodgy
+    :: Bool  -- ^ Law. /This is not any ordinary 'Bool'!/ See the documentation
+             -- on 'law' for more information.
+    -> law
+notDodgy =
+  error "notDodgy may be called only inside of a call to testModel or theoremsOf"
+
+
+------------------------------------------------------------------------------
+-- | Asserts that a function should be a homomorphism in the argument described
+-- by a lambda.
+--
+-- This function /must/ be called with a type application describing the desired
+-- homomorphism. Acceptable typeclasses are 'Data.Semigroup.Semigroup',
+-- 'Monoid', 'Data.Group.Group', 'Eq' and 'Ord'.
+--
+-- The argument to this function must be a lambda binding a single variable.
+--
+-- This function introduces a law for every method in the typeclass.
+--
+-- This function /must/ be called only in the context of either
+-- 'AlgebraCheckers.testModel' or 'AlgebraCheckers.theoremsOf'.
+--
+-- ==== __Examples__
+--
+-- @'homo' \@'Monoid' $ \\s -> set x s@
+homo
+    :: (homo a, homo b)
+    => (a -> b)  -- ^ The function expected to be a homomorphism.
+                 -- /This is not any ordinary function!/ See the documentation
+                 -- on 'homo' for more information.
+    -> law
+homo =
+  error "homo may be called only inside of a call to testModel or theoremsOf"
+
diff --git a/src/AlgebraCheckers/Ppr.hs b/src/AlgebraCheckers/Ppr.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Ppr.hs
@@ -0,0 +1,129 @@
+module AlgebraCheckers.Ppr
+  ( module AlgebraCheckers.Ppr
+  , Doc
+  , render
+  , sep
+  , vcat
+  , hsep
+  , text
+  ) where
+
+import           Control.Monad
+import qualified Language.Haskell.TH as Ppr (ppr)
+import           Language.Haskell.TH hiding (ppr, Arity)
+import           Language.Haskell.TH.PprLib (to_HPJ_Doc)
+import           Prelude hiding (exp)
+import           System.Console.ANSI
+import           AlgebraCheckers.Types
+import           AlgebraCheckers.Unification
+import qualified Text.PrettyPrint.HughesPJ as Ppr
+import           Text.PrettyPrint.HughesPJ hiding ((<>))
+
+
+ppr :: Ppr a => a -> Doc
+ppr = to_HPJ_Doc . Ppr.ppr
+
+showTheoremSource :: TheoremSource -> Doc
+showTheoremSource (LawDefn n) =
+  text "definition of" <+> colorize lawColor (text $ show n)
+showTheoremSource (Interaction a b) =
+  hsep
+    [ text "implied by"
+    , colorize lawColor $ text $ show $ min a b
+    , text "and"
+    , colorize lawColor $ text $ show $ max a b
+    ]
+
+colorize :: Color -> Doc -> Doc
+colorize c doc
+       = zeroWidthText (setSGRCode [SetColor Foreground Vivid c])
+  Ppr.<> doc
+  Ppr.<> zeroWidthText (setSGRCode [SetDefaultColor Foreground])
+
+deepColorize :: Color -> Doc -> Doc
+deepColorize c doc
+       = zeroWidthText (setSGRCode [SetColor Foreground Vivid c, SetConsoleIntensity BoldIntensity])
+  Ppr.<> doc
+  Ppr.<> zeroWidthText (setSGRCode [SetDefaultColor Foreground, SetConsoleIntensity NormalIntensity])
+
+backcolorize :: Color -> Doc -> Doc
+backcolorize c doc
+       = zeroWidthText (setSGRCode [SetColor Background Dull c])
+  Ppr.<> doc
+  Ppr.<> zeroWidthText (setSGRCode [SetDefaultColor Background])
+
+showSaneTheorem :: Theorem -> Doc
+showSaneTheorem (Law n a b) = hang (text "•") 2 $
+  sep
+  [ hang (colorize exprColor $ ppr $ deModuleName a) 6
+      . hang (text "=") 2
+      . colorize exprColor
+      . ppr
+      $ deModuleName b
+  , nest 2 $ parens $ showTheoremSource n
+  ]
+
+showContradictoryTheorem :: Theorem -> TheoremProblem -> Doc
+showContradictoryTheorem (Law n a b) (Contradiction reason) = hang (text "•") 2 $
+  sep
+  [ vcat
+      [ backcolorize Red $ hang (ppr $ deModuleName a) 6
+          . hang (text "=") 2
+          . ppr
+          $ deModuleName b
+      , nest 2 $ pprContradiction reason
+      ]
+  , nest 2 $ parens $ showTheoremSource n
+  ]
+showContradictoryTheorem (Law n a b) (Dodgy reason) = hang (text "•") 2 $
+  sep
+  [ vcat
+      [ hang (backcolorize Black $ ppr $ deModuleName a) 6
+          . hang (text "=") 2
+          . backcolorize Black
+          . ppr
+          $ deModuleName b
+      , nest 2 $ pprDodgy reason
+      ]
+  , nest 2 $ parens $ showTheoremSource n
+  ]
+
+plural :: String -> String -> [a] -> Doc
+plural one _ [_] = text one
+plural _ many _  = text many
+
+pprContradiction :: ContradictionReason -> Doc
+pprContradiction (UnboundMatchableVars vars) =
+  sep
+    [ text "the"
+    , plural "variable" "variables" vars
+    , sep $ punctuate (char ',') $ fmap ppr vars
+    , nest 4 $ sep
+        [ plural "is" "are" vars
+        , text "undetermined"
+        ]
+    ]
+pprContradiction (UnknownConstructors vars) =
+  sep
+    [ text "the"
+    , plural "constructor" "constructors" vars
+    , sep $ punctuate (char ',') $ fmap ppr vars
+    , nest 4 $ sep
+        [ plural "does" "do" vars
+        , text "not exist"
+        ]
+    ]
+pprContradiction UnequalValues =
+  text "unequal values"
+
+pprDodgy :: DodgyReason -> Doc
+pprDodgy SelfRecursive =
+  text "not necessarily productive"
+
+
+exprColor :: Color
+exprColor = Blue
+
+lawColor :: Color
+lawColor = Yellow
+
diff --git a/src/AlgebraCheckers/Suggestions.hs b/src/AlgebraCheckers/Suggestions.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Suggestions.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE TemplateHaskellQuotes #-}
+
+module AlgebraCheckers.Suggestions where
+
+import AlgebraCheckers.Patterns
+import AlgebraCheckers.Ppr
+import AlgebraCheckers.Unification
+import Control.Monad
+import Data.Char
+import Data.Data
+import Data.Generics.Schemes (listify)
+import Data.Group
+import Data.List
+import Data.Maybe
+import Data.Semigroup
+import Data.Traversable
+import Language.Haskell.TH hiding (ppr)
+import Language.Haskell.TH.Syntax
+import Prelude hiding (exp)
+import THInstanceReification
+
+
+data Suggestion
+  = HomoSuggestion Name Name Int Type Type Exp
+  deriving (Eq, Ord, Show)
+
+homoSuggestionEq :: Suggestion -> Suggestion -> Bool
+homoSuggestionEq (HomoSuggestion _ fn1 ix1 _ _ _)
+                 (HomoSuggestion _ fn2 ix2 _ _ _) = fn1 == fn2
+                                                 && ix1 == ix2
+
+
+pprSuggestion :: Suggestion -> Doc
+pprSuggestion (HomoSuggestion nm _ _ arg_ty res_ty (LamE [VarP var] exp)) =
+  ppr $ deModuleName $
+    VarE 'law `AppTypeE` ConT nm `AppE` (LamE [SigP (VarP var) arg_ty] $ SigE exp res_ty)
+pprSuggestion (HomoSuggestion nm _ _ _ _ exp) =
+  ppr $ deModuleName $
+    VarE 'law `AppTypeE` ConT nm `AppE` exp
+
+
+knownSuggestionHierarchies :: [[Name]]
+knownSuggestionHierarchies =
+  [ [ ''Group, ''Monoid, ''Semigroup ]
+  ]
+
+suggest :: Data a => Module -> a -> Q [Suggestion]
+suggest md a = do
+  let surface = getSurface md a
+  fmap (join . join) $
+    for surface $ \nm ->
+      for knownSuggestionHierarchies $ \hierarchy -> do
+        zs <- fmap join $ for hierarchy $ \tc_name -> do
+          VarI _ ty _ <- reify nm
+          possibleHomos tc_name nm ty
+        pure $ nubBy homoSuggestionEq zs
+
+
+suggest' :: Data a => a -> Q [Suggestion]
+suggest' a = do
+  md <- thisModule
+  suggest md a
+
+
+
+possibleHomos :: Name -> Name -> Type -> Q [Suggestion]
+possibleHomos tc_name fn ty = do
+  let (args, res) = unrollTyArr ty
+  hasInstance tc_name res >>= \case
+    False -> pure []
+    True  -> do
+      names <- for args $ newName . goodTyName
+      fmap catMaybes $ for (zip3 names args [0..]) $ \(name, arg, ix) ->
+        hasInstance tc_name arg >>= \case
+          False -> pure Nothing
+          True  -> do
+            exp <- lamE [varP name] $ appsE $ varE fn : fmap varE names
+            pure $ Just $ HomoSuggestion tc_name fn ix arg res exp
+
+
+goodTyName :: Type -> String
+goodTyName = fmap toLower . take 1 . dropWhile (not . isAlpha) . render . ppr . deModuleName
+
+getSurface :: Data a => Module -> a -> [Name]
+getSurface m = listify (sameModule m)
+
+
+sameModule :: Module -> Name -> Bool
+sameModule (Module (PkgName pkg) (ModName md)) n =
+  nameModule n == Just md && namePackage n == Just pkg
+
+
+unrollTyArr :: Type -> ([Type], Type)
+unrollTyArr ty =
+  let tys = unloopTyArrs ty
+   in (init tys, last tys)
+  where
+    unloopTyArrs :: Type -> [Type]
+    unloopTyArrs (ArrowT `AppT` a `AppT` b) =  a : unloopTyArrs b
+    unloopTyArrs t =  [t]
+
+hasInstance :: Name -> Type -> Q Bool
+hasInstance tc_name = isProperInstance tc_name . pure
+
diff --git a/src/AlgebraCheckers/TH.hs b/src/AlgebraCheckers/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/TH.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeApplications    #-}
+
+{-# OPTIONS_HADDOCK not-home #-}
+
+module AlgebraCheckers.TH where
+
+import AlgebraCheckers.Homos
+import AlgebraCheckers.Patterns
+import AlgebraCheckers.Ppr
+import AlgebraCheckers.Theorems
+import AlgebraCheckers.Types
+import AlgebraCheckers.Unification
+import Control.Monad
+import Data.Bool
+import Data.List (nub, partition)
+import Data.Traversable
+import Language.Haskell.TH hiding (ppr, Arity)
+import Language.Haskell.TH.Syntax (lift, Module)
+import Prelude hiding (exp)
+import Test.QuickCheck hiding (collect)
+import Test.QuickCheck.Checkers ((=-=))
+
+
+showTheorem :: Module -> Theorem -> Doc
+showTheorem md thm =
+  case sanityCheck' md thm of
+    Just contradiction ->
+      showContradictoryTheorem thm contradiction
+    Nothing -> showSaneTheorem thm
+
+propTestEq :: Theorem -> ExpQ
+propTestEq t@(Law _ exp1 exp2) = do
+  md <- thisModule
+  let vars = nub $ unboundVars exp1 ++ unboundVars exp2
+  names <- for vars $ newName . nameBase
+  [e|
+    counterexample $(lift $ render $ showTheorem md t) $
+      property $(lamE (fmap varP names) [e|
+       $(pure exp1) =-= $(pure exp2)
+      |])
+    |]
+
+
+------------------------------------------------------------------------------
+-- | Generate QuickCheck property tests for the given model.
+--
+-- ==== __Examples__
+--
+-- @
+--   lawTests :: ['Test.QuickCheck.Property']
+--   lawTests = $('theoremsOf' [e| do
+--
+--   'AlgebraCheckers.law' "commutativity" $ a '+' b '==' b '+' a
+--   'AlgebraCheckers.law' "identity" (a '+' 0 '==' a)
+--
+--   |])
+-- @
+testModel :: ExpQ -> ExpQ
+testModel = (testModelImpl =<<)
+
+testModelImpl :: Exp -> ExpQ
+testModelImpl e = do
+  m <- thisModule
+  listE . fmap propTestEq . theorize m $ parseLaws e
+
+parseLaws :: Exp -> [Law LawSort]
+parseLaws (DoE z) = concatMap collect z
+parseLaws _ = error "you must call parseLaws with a do block"
+
+------------------------------------------------------------------------------
+-- | Like 'testModel', but also interactively dumps all of the derived theorems
+-- of your model. This is very helpful for finding dodgy derivations and
+-- outright contradictions.
+theoremsOf :: ExpQ -> ExpQ
+theoremsOf = (theoremsOfImpl =<<)
+
+theoremsOfImpl :: Exp -> ExpQ
+theoremsOfImpl z = do
+  md <- thisModule
+  let (theorems, problems) = partition (sanityCheck md) $ theorize md $ parseLaws z
+      contradicts = filter (maybe False isContradiction . sanityCheck' md) problems
+      dodgy       = filter (maybe False isDodgy . sanityCheck' md) problems
+  runIO $ do
+    putStrLn ""
+    printStuff md "Theorems"       theorems
+    printStuff md "Dodgy Theorems" dodgy
+    printStuff md "Contradictions" contradicts
+  listE $ fmap propTestEq $ theorems ++ dodgy ++ contradicts
+
+printStuff :: Module -> String -> [Theorem] -> IO ()
+printStuff md sort laws =
+  when (not $ null laws) $ do
+    putStrLn . render
+             $ sep
+             $ text (sort ++ ":") : text "" : fmap (showTheorem md) laws
+    putStrLn ""
+    putStrLn ""
+
+collect :: Stmt -> [Law LawSort]
+collect (LawDef lawname exp1 exp2) = [Law (LawName lawname) exp1 exp2]
+collect (NotDodgyDef exp1 exp2)    = [Law LawNotDodgy exp1 exp2]
+collect (HomoDef ty expr)          = makeHomo ty (knownHomos ty) expr
+collect x = error $ show x
+  -- "collect must be called with the form [e| law \"name\" (foo a b c == bar a d e) |]"
+
diff --git a/src/AlgebraCheckers/Theorems.hs b/src/AlgebraCheckers/Theorems.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Theorems.hs
@@ -0,0 +1,107 @@
+{-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE TupleSections         #-}
+
+module AlgebraCheckers.Theorems where
+
+import Data.Either
+import Control.Monad
+import Data.Bool
+import Data.Char
+import Data.Function (on)
+import Data.Generics.Schemes (listify)
+import Data.List (nub, (\\))
+import Data.Maybe (isNothing, fromMaybe, mapMaybe)
+import Data.Semigroup
+import Language.Haskell.TH hiding (ppr, Arity)
+import Language.Haskell.TH.Syntax (Module)
+import Prelude hiding (exp)
+import AlgebraCheckers.Homos
+import AlgebraCheckers.Suggestions
+import AlgebraCheckers.Types
+import AlgebraCheckers.Unification
+
+
+sanityCheck :: Module -> Theorem -> Bool
+sanityCheck md = isNothing . sanityCheck' md
+
+sanityCheck' :: Module -> Theorem -> Maybe TheoremProblem
+sanityCheck' md (Law _ lhs rhs) =
+  either Just (const Nothing) $ foldr1 (>>)
+    [ lift_error (Contradiction . UnknownConstructors)
+        $ fmap (\(UnboundVarE n) -> n)
+        $ listify is_unbound_ctor (lhs, rhs)
+    , ensure_bound_matches lhs rhs
+    , ensure_bound_matches rhs lhs
+    , bool (Left $ Contradiction UnequalValues) (Right ()) $
+        on (&&) isFullyMatchable lhs rhs `implies` (==) lhs rhs
+    , bool (Left $ Contradiction UnequalValues) (Right ()) $ fromMaybe True $
+        liftM2 (==) (matchableAppHead lhs) (matchableAppHead rhs)
+    , bool (Right ()) (Left $ Dodgy SelfRecursive) $ nonlinearUse md lhs rhs
+    , bool (Right ()) (Left $ Dodgy SelfRecursive) $ nonlinearUse md rhs lhs
+    ]
+  where
+    is_unbound_ctor (UnboundVarE n) = isUpper . head $ nameBase n
+    is_unbound_ctor _ = False
+
+    ensure_bound_matches a b
+      = lift_error (Contradiction . UnboundMatchableVars)
+      $ filter (not . exists_in a)
+      $ matchableMetaVars b
+    lift_error _ [] = Right ()
+    lift_error ctor x = Left $ ctor x
+    exists_in exp var = not . null $ listify (== var) exp
+
+implies :: Bool -> Bool -> Bool
+implies p q = not p || q
+
+matchableMetaVars :: Exp -> [Name]
+matchableMetaVars (UnboundVarE n) = [n]
+matchableMetaVars e =
+  case matchableAppHead e of
+    Just _ -> go e
+    Nothing -> []
+  where
+    go (exp1 `AppE` exp2) =
+      go exp1 ++ matchableMetaVars exp2
+    go _ = []
+
+isFullyMatchable :: Exp -> Bool
+isFullyMatchable (ConE _)                 = True
+isFullyMatchable (TupE es)                = all isFullyMatchable es
+isFullyMatchable (ListE es)               = all isFullyMatchable es
+isFullyMatchable (LitE _)                 = True
+isFullyMatchable (UnboundVarE _)          = True
+isFullyMatchable (AppE (UnboundVarE _) _) = False
+isFullyMatchable (AppE exp1 exp2)         = isFullyMatchable exp1 && isFullyMatchable exp2
+isFullyMatchable _                        = False
+
+namedLawToEither :: NamedLaw -> Either (Law ()) (Law String)
+namedLawToEither (Law (LawName n) a b) = Right (Law n a b)
+namedLawToEither (Law LawNotDodgy a b) = Left (Law () a b)
+
+theorize :: Module -> [NamedLaw] -> [Theorem]
+theorize md named_laws =
+  let (not_dodgy, laws) = partitionEithers $ fmap namedLawToEither named_laws
+      law_defs = fmap (\t -> t { lawData = LawDefn $ lawData t }) laws
+      sane_laws = filter (sanityCheck md) law_defs
+      theorems = do
+         l1@Law{lawData = LawDefn l1name} <- sane_laws
+         l2@Law{lawData = LawDefn l2name} <- sane_laws
+         guard $ l1 /= l2
+         (lhs, rhs) <- criticalPairs l1 l2
+         pure $ Law (Interaction l1name l2name) lhs rhs
+   in (nub $ law_defs <> theorems) \\ fmap (\l -> l {lawData = LawDefn ""} ) not_dodgy
+
+matchableAppHead :: Exp -> Maybe Name
+matchableAppHead (ConE n)   = Just n
+matchableAppHead (AppE f _) = matchableAppHead f
+matchableAppHead _          = Nothing
+
+nonlinearUse :: Module -> Exp -> Exp -> Bool
+nonlinearUse md exp1 exp2 =
+  let exp2s = mapMaybe (\exp -> splitApps exp) $ fmap seExp $ subexps exp2
+   in any (\(apphead, exps) -> nonlinearFunc md apphead && any (equalUpToAlpha exp1) exps) exp2s
+
+nonlinearFunc :: Module -> Name -> Bool
+nonlinearFunc md name = not $ sameModule md name
+
diff --git a/src/AlgebraCheckers/Types.hs b/src/AlgebraCheckers/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Types.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFunctor      #-}
+
+module AlgebraCheckers.Types where
+
+import Data.Data
+import AlgebraCheckers.Unification
+import Language.Haskell.TH
+
+data Law a = Law
+  { lawData :: a
+  , lawLhsExp :: Exp
+  , lawRhsExp :: Exp
+  }
+  deriving (Ord, Show, Data, Typeable)
+
+instance Eq a => Eq (Law a) where
+  Law _ a a' == Law _ b b' =
+    and
+      [ equalUpToAlpha a b && equalUpToAlpha a' b'
+      ]
+
+data LawSort
+  = LawName String
+  | LawNotDodgy
+  deriving (Eq, Ord, Show)
+
+type NamedLaw = Law LawSort
+type Theorem  = Law TheoremSource
+
+data Arity = Binary | Prefix Int
+  deriving (Eq, Ord, Show)
+
+data TheoremProblem
+  = Dodgy DodgyReason
+  | Contradiction ContradictionReason
+  deriving (Eq, Ord, Show)
+
+isContradiction :: TheoremProblem -> Bool
+isContradiction Contradiction{} = True
+isContradiction _               = False
+
+isDodgy :: TheoremProblem -> Bool
+isDodgy Dodgy{} = True
+isDodgy _       = False
+
+data ContradictionReason
+  = UnboundMatchableVars [Name]
+  | UnequalValues
+  | UnknownConstructors [Name]
+  deriving (Eq, Ord, Show)
+
+data DodgyReason
+  = SelfRecursive
+  deriving (Eq, Ord, Show)
+
+data TheoremSource
+  = LawDefn String
+  | Interaction String String
+  deriving (Eq, Ord, Show)
+
diff --git a/src/AlgebraCheckers/Types.hs-boot b/src/AlgebraCheckers/Types.hs-boot
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Types.hs-boot
@@ -0,0 +1,11 @@
+module AlgebraCheckers.Types where
+
+import Language.Haskell.TH
+
+data Law a = Law
+  { lawData :: a
+  , lawLhsExp :: Exp
+  , lawRhsExp :: Exp
+  }
+
+
diff --git a/src/AlgebraCheckers/Unification.hs b/src/AlgebraCheckers/Unification.hs
new file mode 100644
--- /dev/null
+++ b/src/AlgebraCheckers/Unification.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns    #-}
+
+module AlgebraCheckers.Unification where
+
+import           Control.Applicative
+import           Control.Monad.State
+import           Control.Monad.Trans.Writer
+import           Data.Data
+import           Data.Function
+import           Data.Generics.Aliases
+import           Data.Generics.Schemes
+import qualified Data.Map as M
+import           Language.Haskell.TH
+import           Language.Haskell.TH.Syntax
+import           Prelude hiding (exp)
+import {-# SOURCE #-} AlgebraCheckers.Types
+
+
+data SubExp = SubExp
+  { seExp  :: Exp
+  , seSubId :: Int
+  } deriving (Eq, Ord, Show)
+
+
+deModuleName :: Data a => a -> a
+deModuleName = everywhere $ mkT $ \case
+  NameQ _ -> NameS
+  NameG _ _ _ -> NameS
+  n       -> n
+
+
+unboundVars :: Exp -> [Name]
+unboundVars = everything (++) $
+  mkQ [] $ \case
+    UnboundVarE n -> [n]
+    _ -> []
+
+
+------------------------------------------------------------------------------
+-- | Operates over UnboundVarEs
+bindVars :: Data a => M.Map Name Exp -> a -> a
+bindVars m = everywhere $ mkT $ \case
+  e@(UnboundVarE n) ->
+    case M.lookup n m of
+      Just e' -> e'
+      Nothing -> e
+  t -> t
+
+
+------------------------------------------------------------------------------
+-- | Operates over VarEs
+rebindVars :: Data a => M.Map Name Exp -> a -> a
+rebindVars m = everywhere $ mkT $ \case
+  e@(VarE n) ->
+    case M.lookup n m of
+      Just e' -> e'
+      Nothing -> e
+  t -> t
+
+
+renameVars :: Data a => (String -> String) -> a -> a
+renameVars f = everywhere $ mkT $ \case
+  UnboundVarE n -> UnboundVarE . mkName . f $ nameBase n
+  t -> t
+
+
+type Subst = M.Map Name Exp
+
+sub :: Data a => Subst -> a -> a
+sub = bindVars
+
+unifySub :: Subst -> Exp -> Exp -> Maybe Subst
+unifySub s a
+  = fmap ((M.map =<< sub) . flip mappend s)
+  . on unify (sub s) a
+
+
+
+type Critical = (Exp, Exp)
+
+criticalPairs :: Law a -> Law a -> [Critical]
+criticalPairs other me = do
+  let (otherlhs, otherrhs)
+        = renameVars (++ "1") (lawLhsExp other, lawRhsExp other)
+      (melhs, merhs)
+        = renameVars (++ "2") (lawLhsExp me, lawRhsExp me)
+
+  pat <- subexps melhs
+  Just subs <- pure $ unify (seExp pat) otherlhs
+  let res = bindVars subs (merhs, replaceSubexp pat (const otherrhs) melhs)
+  guard $ uncurry (/=) res
+  let (a,b) = res
+  pure (min a b, max a b)
+
+
+
+subexps :: Exp -> [SubExp]
+subexps e =
+  flip evalState 0 $ execWriterT $
+    everywhereM (mkM  $ \e' -> do
+      ix <- get
+      modify (+1)
+      case e' of
+        UnboundVarE _ -> pure ()
+        se -> tell [(SubExp se ix)]
+      pure e'
+                             ) e
+
+
+replaceSubexp :: SubExp -> (Exp -> Exp) -> Exp -> Exp
+replaceSubexp (SubExp _ ix) f old =
+  flip evalState 0 $
+    everywhereM (mkM $ \e' -> do
+      ix' <- get
+      modify (+1)
+      pure $ case ix == ix' of
+        True  -> f e'
+        False -> e'
+                ) old
+
+
+equalUpToAlpha :: Exp -> Exp -> Bool
+equalUpToAlpha a b =
+  maybe
+    False
+    (\subst -> all isUnbound subst
+            && uncurry (==) (bindVars subst (a, b)))
+    (unify a b)
+  where
+    isUnbound (UnboundVarE _) = True
+    isUnbound _ = False
+
+
+unify :: Exp -> Exp -> Maybe Subst
+unify (ParensE exp1) exp2 = unify exp1 exp2
+unify exp1 (ParensE exp2) = unify exp1 exp2
+unify (UnboundVarE name) exp = pure $ M.singleton name exp
+unify exp (UnboundVarE name) = pure $ M.singleton name exp
+unify (AppE f1 exp1) (AppE f2 exp2) = do
+  s1 <- unify f1 f2
+  s2 <- unifySub s1 exp1 exp2
+  pure s2
+unify (AppTypeE exp1 t1) (AppTypeE exp2 t2) = do
+  guard $ t1 == t2
+  unify exp1 exp2
+unify (InfixE (Just lhs1) exp1 (Just rhs1))
+      (InfixE (Just lhs2) exp2 (Just rhs2)) = do
+  s1 <- unify exp1 exp2
+  s2 <- unifySub s1 lhs1 lhs2
+  s3 <- unifySub s2 rhs1 rhs2
+  pure s3
+unify (InfixE Nothing exp1 (Just rhs1))
+      (InfixE Nothing exp2 (Just rhs2)) = do
+  s1 <- unify exp1 exp2
+  unifySub s1 rhs1 rhs2
+unify (InfixE (Just lhs1) exp1 Nothing)
+      (InfixE (Just lhs2) exp2 Nothing) = do
+  s1 <- unify lhs1 lhs2
+  unifySub s1 exp1 exp2
+unify (TupE exps1) (TupE exps2) = do
+  guard $ exps1 == exps2
+  foldM (uncurry . unifySub) mempty $ zip exps1 exps2
+unify (CondE cond1 then1 else1) (CondE cond2 then2 else2) = do
+  s1 <- unify cond1 cond2
+  s2 <- unifySub s1 then1 then2
+  unifySub s2 else1 else2
+unify (SigE exp1 t1) (SigE exp2 t2) = do
+  guard $ t1 == t2
+  unify exp1 exp2
+unify a b = do
+  guard $ a == b
+  pure mempty
+