diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Revision history for inspection-testing
 
+## 0.1.1 -- 2017-11-09
+
+* More complete output when `(===)` fails
+* Variant `(==-)` that ignores types when comparing terms
+
 ## 0.1 -- 2017-11-09
 
 * Repackaged as inspection-testing
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -13,7 +13,7 @@
 more to it than:
 
 ```haskell
-{-# LANGAUGE TemplateHaskell #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}
 module Simple where
 
@@ -59,8 +59,8 @@
 examples/Simple.hs: error: inspection testing unsuccessful
 ```
 
-What can I check for
---------------------
+What can I check for?
+---------------------
 
 Currently, inspection-testing supports
 
@@ -75,6 +75,16 @@
  * peforming some of these checks only within recursive loops
 
 Let me know if you need any of these, or have further ideas.
+
+Help, I am drowining in Core!
+-----------------------------
+
+inspection-testing prints the Core more or less like GHC would, and the same
+flags can be used to control the level of detail. In particular, you might want
+to pass to GHC a selection of the following flags:
+
+    -dsuppress-idinfo -dsuppress-coercions -dsuppress-type-applications
+    -dsuppress-module-prefixes -dsuppress-type-signatures -dsuppress-uniques
 
 Can I comment or help?
 ----------------------
diff --git a/Test/Inspection.hs b/Test/Inspection.hs
--- a/Test/Inspection.hs
+++ b/Test/Inspection.hs
@@ -6,7 +6,7 @@
 -- Portability : GHC specifc
 --
 -- This module supports the accompanying GHC plugin "Test.Inspection.Plugin" and adds
--- to GHC the ability to do inspeciton testing.
+-- to GHC the ability to do inspection testing.
 
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -18,7 +18,9 @@
     -- * Registering obligations
     inspect,
     -- * Defining obligations
-    Obligation(..), mkObligation, Property(..), (===), (=/=), hasNoType, ) where
+    Obligation(..), mkObligation, Property(..),
+    (===), (==-), (=/=), hasNoType,
+) where
 
 import Control.Monad
 import Language.Haskell.TH
@@ -90,7 +92,9 @@
     -- More precisely: @f@ is equal to @g@ if either the definition of @f@ is
     -- @f = g@, or the definition of @g@ is @g = f@, or if the definitions are
     -- @f = e@ and @g = e@.
-    = EqualTo Name
+    --
+    -- If the boolean flag is true, then ignore types during the comparison.
+    = EqualTo Name Bool
 
     -- | Does this type not occur anywhere in the definition of the function
     -- (neither locally bound nor passed as arguments)
@@ -104,7 +108,7 @@
 allLocalNames obl = target obl : goProp (property obl)
   where
     goProp :: Property -> [Name]
-    goProp (EqualTo n) = [n]
+    goProp (EqualTo n _) = [n]
     goProp _ = []
 
 -- | Creates an inspection obligation for the given function name
@@ -120,17 +124,25 @@
 
 -- | Convenience function to declare two functions to be equal
 (===) :: Name -> Name -> Obligation
-(===) = mkEquality False
-infix 1 ===
+(===) = mkEquality False False
+infix 9 ===
 
+-- | Convenience function to declare two functions to be equal, but ignoring
+-- type lambdas, type arguments and type casts
+(==-) :: Name -> Name -> Obligation
+(==-) = mkEquality False True
+infix 9 ==-
+
 -- | Convenience function to declare two functions to be equal, but expect the test to fail
 -- (This is useful for documentation purposes, or as a TODO list.)
 (=/=) :: Name -> Name -> Obligation
-(=/=) = mkEquality True
-infix 1 =/=
+(=/=) = mkEquality True False
+infix 9 =/=
 
-mkEquality :: Bool -> Name -> Name -> Obligation
-mkEquality expectFail n1 n2 = (mkObligation n1 (EqualTo n2)) { expectFail = expectFail }
+mkEquality :: Bool -> Bool -> Name -> Name -> Obligation
+mkEquality expectFail ignore_types n1 n2 =
+    (mkObligation n1 (EqualTo n2 ignore_types))
+        { expectFail = expectFail }
 
 -- | Convenience function to declare that a function’s implementation does not
 -- mention a type
diff --git a/Test/Inspection/Core.hs b/Test/Inspection/Core.hs
--- a/Test/Inspection/Core.hs
+++ b/Test/Inspection/Core.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE CPP #-}
 module Test.Inspection.Core
   ( slice
+  , pprSlice
+  , pprSliceDifference
   , eqSlice
   , freeOfType
   , doesNotAllocate
@@ -17,14 +19,20 @@
 import Name
 import VarEnv
 import Literal (nullAddrLit)
+import Outputable
+import PprCore
+import Coercion
+import Util
 
 import qualified Data.Set as S
 import Data.Maybe
 import State
 import Control.Monad
 
+type Slice = [(Var, CoreExpr)]
+
 -- | Selects those bindings that define the given variable
-slice :: [(Var, CoreExpr)] -> Var -> [(Var,CoreExpr)]
+slice :: [(Var, CoreExpr)] -> Var -> Slice
 slice binds v = [(v,e) | (v,e) <- binds, v `S.member` used ]
   where
     used = execState (goV v) S.empty
@@ -53,18 +61,96 @@
 
     goA (_, _, e) = go e
 
+-- | Pretty-print a slice
+pprSlice :: Slice -> SDoc
+pprSlice slice = withLessDetail $ pprCoreBindings [ NonRec v e  | (v,e) <- slice ]
+
+-- | Pretty-print two slices, after removing variables occurring in both
+pprSliceDifference :: Slice -> Slice -> SDoc
+pprSliceDifference slice1 slice2 =
+    nest 4 (hang (text "LHS" <> colon) 4 (pprSlice slice1')) $$
+    nest 4 (hang (text "RHS" <> colon) 4 (pprSlice slice2'))
+  where
+    both = S.intersection (S.fromList (map fst slice1)) (S.fromList (map fst slice2))
+    slice1' = filter (\(v,_) -> v `S.notMember` both) slice1
+    slice2' = filter (\(v,_) -> v `S.notMember` both) slice2
+
+withLessDetail :: SDoc -> SDoc
+#if MIN_VERSION_GLASGOW_HASKELL(8,2,0,0)
+withLessDetail sdoc = sdocWithDynFlags $ \dflags ->
+     withPprStyle (defaultUserStyle dflags) sdoc
+#else
+withLessDetail sdoc = withPprStyle defaultUserStyle sdoc
+#endif
+
 -- | This is a heuristic, which only works if both slices
 -- have auxillary variables in the right order.
 -- (This is mostly to work-around the buggy CSE in GHC-8.0)
 -- It also breaks if there is shadowing.
-eqSlice :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> Bool
-eqSlice slice1 slice2 =
-    eqExpr emptyInScopeSet (Let (Rec slice1) (Lit nullAddrLit))
-                           (Let (Rec slice2) (Lit nullAddrLit))
+eqSlice :: Bool {- ^ ignore types -} -> Slice -> Slice -> Bool
+-- Compares for equality, modulo alpha
+eqSlice it slice1 slice2
+  = go (mkRnEnv2 emptyInScopeSet)
+       (Let (Rec slice1) (Lit nullAddrLit))
+       (Let (Rec slice2) (Lit nullAddrLit))
+         -- this is a slight hack, for now
+  where
+    go env (Var v1) (Var v2)
+      | rnOccL env v1 == rnOccR env v2
+      = True
+    go _   (Lit lit1)    (Lit lit2)        = lit1 == lit2
+    go env (Type t1)     (Type t2)         = eqTypeX env t1 t2
+    go env (Coercion co1) (Coercion co2)   = eqCoercionX env co1 co2
 
+    go env (Cast e1 _) e2 | it             = go env e1 e2
+    go env e1 (Cast e2 _) | it             = go env e1 e2
+    go env (Cast e1 co1) (Cast e2 co2)     = eqCoercionX env co1 co2 && go env e1 e2
+
+    go env (App e1 a) e2 | it, isTypeArg a = go env e1 e2
+    go env e1 (App e2 a) | it, isTypeArg a = go env e1 e2
+    go env (App f1 a1)   (App f2 a2)       = go env f1 f2 && go env a1 a2
+    go env (Tick n1 e1)  (Tick n2 e2)      = go_tick env n1 n2 && go env e1 e2
+
+    go env (Lam b e1) e2 | it, isTyCoVar b = go env e1 e2
+    go env e1 (Lam b e2) | it, isTyCoVar b = go env e1 e2
+    go env (Lam b1 e1)  (Lam b2 e2)
+      =  (it || eqTypeX env (varType b1) (varType b2))  -- False for Id/TyVar combination
+      && go (rnBndr2 env b1 b2) e1 e2
+
+    go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2)
+      =  go env r1 r2  -- No need to check binder types, since RHSs match
+      && go (rnBndr2 env v1 v2) e1 e2
+
+    go env (Let (Rec ps1) e1) (Let (Rec ps2) e2)
+      = equalLength ps1 ps2
+      && all2 (go env') rs1 rs2 && go env' e1 e2
+      where
+        (bs1,rs1) = unzip ps1
+        (bs2,rs2) = unzip ps2
+        env' = rnBndrs2 env bs1 bs2
+
+    go env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2)
+      | null a1   -- See Note [Empty case alternatives] in TrieMap
+      = null a2 && go env e1 e2 && (it || eqTypeX env t1 t2)
+      | otherwise
+      =  go env e1 e2 && all2 (go_alt (rnBndr2 env b1 b2)) a1 a2
+
+    go _ _ _ = False
+
+    -----------
+    go_alt env (c1, bs1, e1) (c2, bs2, e2)
+      = c1 == c2 && go (rnBndrs2 env bs1 bs2) e1 e2
+
+    go_tick :: RnEnv2 -> Tickish Id -> Tickish Id -> Bool
+    go_tick env (Breakpoint lid lids) (Breakpoint rid rids)
+          = lid == rid  &&  map (rnOccL env) lids == map (rnOccR env) rids
+    go_tick _ l r = l == r
+
+
+
 -- | Returns @True@ if the given core expression mentions no type constructor
 -- anywhere that has the given name.
-freeOfType :: [(Var, CoreExpr)] -> Name -> Maybe (Var, CoreExpr)
+freeOfType :: Slice -> Name -> Maybe (Var, CoreExpr)
 freeOfType slice tcN = listToMaybe [ (v,e) | (v,e) <- slice, not (go e) ]
   where
     goV v = goT (varType v)
@@ -103,7 +189,7 @@
 -- allocate. It should probably at least look through local function calls.
 --
 -- The variable is important to know the arity of the function.
-doesNotAllocate :: [(Var, CoreExpr)] -> Maybe (Var, CoreExpr)
+doesNotAllocate :: Slice -> Maybe (Var, CoreExpr)
 doesNotAllocate slice = listToMaybe [ (v,e) | (v,e) <- slice, not (go (idArity v) e) ]
   where
     go _ (Var v)
diff --git a/Test/Inspection/Plugin.hs b/Test/Inspection/Plugin.hs
--- a/Test/Inspection/Plugin.hs
+++ b/Test/Inspection/Plugin.hs
@@ -61,7 +61,8 @@
     (if expectFail then " (failure expected)" else "")
 
 prettyProperty :: Module -> TH.Name -> Property -> String
-prettyProperty mod target (EqualTo n2)        = showTHName mod target ++ " === " ++ showTHName mod n2
+prettyProperty mod target (EqualTo n2 False)  = showTHName mod target ++ " === " ++ showTHName mod n2
+prettyProperty mod target (EqualTo n2 True)   = showTHName mod target ++ " ==- " ++ showTHName mod n2
 prettyProperty mod target (NoType t)          = showTHName mod target ++ " `hasNoType` " ++ showTHName mod t
 prettyProperty mod target NoAllocation        = showTHName mod target ++ " does not allocate"
 
@@ -104,7 +105,7 @@
     ]
 
 checkProperty :: ModGuts -> TH.Name -> Property -> CoreM Result
-checkProperty guts thn1 (EqualTo thn2) = do
+checkProperty guts thn1 (EqualTo thn2 ignore_types) = do
     Just n1 <- thNameToGhcName thn1
     Just n2 <- thNameToGhcName thn2
 
@@ -118,18 +119,16 @@
        -> return Nothing
        | Just (_, Var other) <- p2, getName other == n1
        -> return Nothing
-       -- OK if they have the same expression
        | Just (v1, _) <- p1
        , Just (v2, _) <- p2
-       , eqSlice (slice binds v1) (slice binds v2)
-       -> return Nothing
-       -- Not ok if the expression differ
-       | Just (_, e1) <- p1
-       , Just (_, e2) <- p2
-       -> pure . Just $ do
-            putMsg $
-                nest 4 (hang (text "LHS" <> colon) 4 (ppr e1)) $$
-                nest 4 (hang (text "RHS" <> colon) 4 (ppr e2))
+       , let slice1 = slice binds v1
+       , let slice2 = slice binds v2
+       -> if eqSlice ignore_types slice1 slice2
+          -- OK if they have the same expression
+          then return Nothing
+          -- Not ok if the expression differ
+          else pure . Just $ putMsg $
+            pprSliceDifference slice1 slice2
        -- Not ok if both names are bound externally
        | Nothing <- p1
        , Nothing <- p2
diff --git a/inspection-testing.cabal b/inspection-testing.cabal
--- a/inspection-testing.cabal
+++ b/inspection-testing.cabal
@@ -1,6 +1,6 @@
 name:                inspection-testing
-version:             0.1
-synopsis:            GHC plugin to do inspection esting
+version:             0.1.1
+synopsis:            GHC plugin to do inspection testing
 description:         Some carefully crafted libraries make promises to their
                      users beyond functionality and performance.
                      .