diff --git a/.travis.yml b/.travis.yml
index 478d01d35..4454704b0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,7 +21,7 @@ install:
 
 script:
 - stack --no-terminal build --fast --test --no-run-tests --ghc-options "-Werror -fmax-pmcheck-iterations=5000000"
-- env AMC_LIBRARY_PATH=$PWD/lib/ stack --no-terminal test --fast --ghc-options "-Werror -fmax-pmcheck-iterations=5000000" --test-arguments "--xml junit.xml --display t --hedgehog-tests 10000 --timeout 60"
+- env AMC_LIBRARY_PATH=$PWD/lib/ stack --no-terminal test --fast --ghc-options "-Werror -fmax-pmcheck-iterations=5000000" --test-arguments "--xml junit.xml --display t --hedgehog-tests 1000 --timeout 80"
 - stack --no-terminal exec --package=hlint -- hlint --git
 
 notifications:
diff --git a/amuletml.cabal b/amuletml.cabal
index 147726e21..1b1fa057d 100644
--- a/amuletml.cabal
+++ b/amuletml.cabal
@@ -153,6 +153,7 @@ test-suite tests
                      , Test.Syntax.Verify
 
                      , Test.Types.Check
+                     , Test.Types.Holes
                      , Test.Types.Unify
                      , Test.Types.Util
 
diff --git a/tests/driver/Main.hs b/tests/driver/Main.hs
index b2e9b6ff0..e7b2c9fbe 100644
--- a/tests/driver/Main.hs
+++ b/tests/driver/Main.hs
@@ -7,7 +7,8 @@ import Test.Tasty.Reporter
 import Test.Tasty.Rerun
 import Test.Tasty
 
--- import qualified Test.Types.Unify as Solver
+import qualified Test.Types.Unify as Solver
+import qualified Test.Types.Holes as Holes
 import qualified Test.Core.Lint as Lint
 import qualified Test.Parser.Lexer as Lexer
 import qualified Test.Parser.Parser as Parser
@@ -20,10 +21,12 @@ import qualified Test.Frontend.Amc as Amc
 
 tests :: IO TestTree
 tests = testGroup "Tests" <$> sequence
-  -- [ pure Solver.tests Has a tendency to timeout. TODO: Get better CI
-  -- machines
+  -- These two will timeout if you run 10000 of them.
+  -- TODO: Get better CI machines
+  [ pure Solver.tests
+  , pure Holes.tests
 
-  [ Amc.tests
+  , Amc.tests
   , Lint.tests
   , Lexer.tests
   , Parser.tests
diff --git a/tests/driver/Test/Syntax/Gen.hs b/tests/driver/Test/Syntax/Gen.hs
index 37e75c8bf..7f6d842ed 100644
--- a/tests/driver/Test/Syntax/Gen.hs
+++ b/tests/driver/Test/Syntax/Gen.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-}
-module Test.Syntax.Gen ( genType, genLit ) where
+module Test.Syntax.Gen ( genType, genSimpleType, genFormula, genLit ) where
 
 import Syntax.Builtin
 import Syntax.Var
@@ -28,6 +28,12 @@ referToVar = do
   scope <- asks namesInScope
   Gen.element scope
 
+-- | Generate a type using most of Amulet's type system features. Types
+-- generated by 'genType' are most likely nonsense.
+genType :: MonadGen m => m (Type Typed)
+genType = runReaderT gen_type emptyScope
+
+
 gen_type :: (MonadGen m, MonadReader InScopeSet m) => m (Type Typed)
 gen_type = do
   scope <- asks namesInScope
@@ -36,10 +42,7 @@ gen_type = do
           [ Gen.element [ tyUnit, tyBool, tyInt, tyString ]
           , Gen.element [ TyPromotedCon nILName, TyPromotedCon cONSName ]
           ]
-        ++
-          case scope of
-            [] -> []
-            _ -> [TyVar <$> referToVar]
+        ++ [ TyVar <$> referToVar | not (null scope) ]
 
   Gen.recursive Gen.choice
     base_case
@@ -72,8 +75,44 @@ gen_type = do
           (,) (alpha !! n) <$> genType
     ]
 
-genType :: MonadGen m => m (Type Typed)
-genType = runReaderT gen_type emptyScope
+-- | Generate an inhabited type of kind Type
+genSimpleType :: MonadGen m => m (Type Typed)
+genSimpleType =
+  Gen.recursive Gen.choice
+    [ Gen.element [ tyUnit, tyBool, tyInt, tyString ]
+    ]
+    [ TyArr <$> genSimpleType <*> genSimpleType
+    , TyTuple <$> genSimpleType <*> genSimpleType
+
+    , TyApp tyLazy <$> genSimpleType
+    , TyApp tyList <$> genSimpleType
+    ]
+
+-- | Generate a type that looks somewhat like a formula in first-order
+-- logic, using implication and conjunction. This always starts with a
+-- (random) number of foralls introducting logical variables /and/
+-- assumptions of those variables. This is to insure that the types are
+-- inhabited by a proof more often than they are not.
+genFormula :: MonadGen m => m (Type Typed)
+genFormula = do
+  vars <- Gen.int (Range.linear 1 5)
+  runReaderT (intros vars gen_formula) emptyScope
+
+gen_formula :: (MonadGen m, MonadReader InScopeSet m) => m (Type Typed)
+gen_formula =
+  Gen.recursive Gen.choice
+    [ TyVar <$> referToVar ]
+    [ TyArr <$> gen_formula <*> gen_formula
+    , TyTuple <$> gen_formula <*> gen_formula
+    ]
+
+intro :: MonadReader InScopeSet m => m (Type Typed) -> m (Type Typed)
+intro k = withVar $ \v ->
+  TyPi (Invisible v Nothing Spec) . TyArr (TyVar v) <$> k
+
+intros :: MonadReader InScopeSet m => Int -> m (Type Typed) -> m (Type Typed)
+intros 0 k = k
+intros n k = intro (intros (n - 1) k)
 
 genLit :: MonadGen m => m Lit
 genLit =
@@ -95,5 +134,3 @@ emptyScope :: InScopeSet
 emptyScope = InScopeSet alpha mempty where
   alpha = zipWith toName [1..] ([1..] >>= flip replicateM ['a'..'z'])
   toName id n = TgName (T.pack n) id
-
--- pah orphans
diff --git a/tests/driver/Test/Types/Holes.hs b/tests/driver/Test/Types/Holes.hs
new file mode 100644
index 000000000..8c8a528b0
--- /dev/null
+++ b/tests/driver/Test/Types/Holes.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Test.Types.Holes where
+
+import Control.Monad.Namey
+import Control.Monad.Infer (firstName)
+import Control.Arrow hiding ((<+>))
+import Control.Lens hiding (Lazy)
+
+import Test.Syntax.Gen
+import Test.Types.Util
+import Test.Util
+
+import Syntax.Transform
+import Syntax.Builtin
+import Syntax.Desugar
+import Syntax.Pretty
+import Syntax
+
+import Types.Holes
+
+import Data.Foldable
+import Data.Span
+
+import Text.Pretty.Semantic
+
+import Unsafe.Coerce
+
+import Hedgehog
+
+prop_amuseMakesTermsOfType :: Property
+prop_amuseMakesTermsOfType = property $ testAmuse genSimpleType
+
+prop_amuseProvesFormulas :: Property
+prop_amuseProvesFormulas = property $ testAmuse genFormula
+
+testAmuse :: Gen (Type Typed) -> PropertyT IO ()
+testAmuse gen = do
+  aty <- forAllWith (displayS . displayType) gen
+  let (terms, nm) =
+        runNamey (findHoleCandidate mempty internal builtinEnv aty) firstName
+
+  for_ terms $ \term -> do
+    let term' = forgetTypes term
+        ([LetStmt _ _ [Binding _  term'' _ _]], _) =
+          runNamey (desugarProgram
+                      [LetStmt NonRecursive Private [Binding firstName term' False internal]])
+                   nm
+
+    case checkExpr term'' aty of
+      Left e -> do
+        footnote . displayS $
+          keyword "Proof term:" <+> pretty term''
+        footnote . displayS . pretty . toList $ e
+        failure
+      Right () -> success
+
+tests :: TestTree
+tests = hedgehog $ $$(discover)
+
+forgetTypes :: Expr Typed -> Expr Resolved
+forgetTypes (VarRef v (an, _)) = VarRef v an
+forgetTypes (Let re bs bd (a, _)) = Let re (forgetBinds <$> bs) (forgetTypes bd) a where
+  forgetBinds (Binding v e b (a, _)) = Binding v (forgetTypes e) b a
+  forgetBinds (Matching p e (a, _)) = Matching (forgetPat p) (forgetTypes e) a
+  forgetBinds (TypedMatching p e (a, _) _) = Matching (forgetPat p) (forgetTypes e) a
+forgetTypes (If c t e (a, _)) = If (forgetTypes c) (forgetTypes t) (forgetTypes e) a
+forgetTypes (App f x (a, _)) = App (forgetTypes f) (forgetTypes x) a
+forgetTypes (Fun p bd (a, _)) = Fun (forgetP p) (forgetTypes bd) a where
+  forgetP (PatParam p) = PatParam $ forgetPat p
+  forgetP (EvParam p) = EvParam $ forgetPat p
+forgetTypes (Begin es (a, _)) = Begin (forgetTypes <$> es) a
+forgetTypes (Literal l (a, _)) = Literal l a
+forgetTypes (Match e as (a, _)) = Match (forgetTypes e) (forgetArm <$> as) a where
+  forgetArm (Arm p g e) = Arm (forgetPat p) (forgetTypes <$> g) (forgetTypes e)
+forgetTypes (Function as (a, _)) = Function (forgetArm <$> as) a where
+  forgetArm (Arm p g e) = Arm (forgetPat p) (forgetTypes <$> g) (forgetTypes e)
+forgetTypes (BinOp l o r (a, _)) = BinOp (forgetTypes l) (forgetTypes o) (forgetTypes r) a
+forgetTypes (Hole v (a, _)) = Hole v a
+forgetTypes (Ascription e t (a, _)) = Ascription (forgetTypes e) (forgetKind t) a
+forgetTypes (Record fs (a, _)) = Record (forgetField <$> fs) a
+forgetTypes (RecordExt e fs (a, _)) = RecordExt (forgetTypes e) (forgetField <$> fs) a
+forgetTypes (Access r t (a, _)) = Access (forgetTypes r) t a
+
+forgetTypes LeftSection{} = undefined
+forgetTypes RightSection{} = undefined
+forgetTypes BothSection{} = undefined
+forgetTypes AccessSection{} = undefined
+forgetTypes Parens{} = undefined
+
+forgetTypes (Tuple es (a, _)) = Tuple (forgetTypes <$> es) a
+forgetTypes TupleSection{} = undefined
+forgetTypes OpenIn{} = undefined
+
+forgetTypes (Lazy e (a, _)) = Lazy (forgetTypes e) a
+forgetTypes (Vta e t (a, _)) = Vta (forgetTypes e) (forgetKind t) a
+forgetTypes (ListExp es (a, _)) = ListExp (forgetTypes <$> es) a
+
+forgetTypes ListComp{} = undefined
+forgetTypes DoExpr{} = undefined
+forgetTypes Idiom{} = undefined
+
+forgetTypes (ExprWrapper _ e _) = forgetTypes e
+
+forgetField :: Field Typed -> Field Resolved
+forgetField (Field t e (a, _)) = Field t (forgetTypes e) a
+
+forgetPat :: Pattern Typed -> Pattern Resolved
+forgetPat (Wildcard (a, _)) = Wildcard a
+forgetPat (Capture v (a, _)) = Capture v a
+forgetPat (Destructure v p (a, _)) = Destructure v (forgetPat <$> p) a
+forgetPat (PAs p v (a, _)) = PAs (forgetPat p) v a
+forgetPat (PType p t (a, _)) = PType (forgetPat p) (forgetKind t) a
+forgetPat (PRecord rs (a, _)) = PRecord (map (second forgetPat) rs) a
+forgetPat (PTuple p (a, _)) = PTuple (forgetPat <$> p) a
+forgetPat (PList p (a, _)) = PTuple (forgetPat <$> p) a
+forgetPat (PLiteral l (a, _)) = PLiteral l a
+forgetPat PGadtCon{} = undefined
+
+forgetKind :: Type Typed -> Type Resolved
+forgetKind = unsafeCoerce . transformType go where
+  go (TySkol v) = TyVar (v ^. skolVar)
+  go x = x