diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr
new file mode 100644
index 0000000..c365158
--- /dev/null
+++ b/src/Core/AutoSearch.idr
@@ -0,0 +1,118 @@
+module Core.AutoSearch
+
+import Core.Context
+import Core.Core
+import Core.Env
+import Core.Normalise
+import Core.TT
+import Core.Unify
+import Core.Value
+
+%default covering
+
+SearchEnv : List Name -> Type
+SearchEnv vars = List (NF vars, Closure vars)
+
+searchType : {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST UState} ->
+             FC -> RigCount ->
+             (defining : Name) -> (topTy : Term vars) ->
+             Env Term vars -> SearchEnv vars -> 
+             (target : NF vars) -> Core (NF vars)
+
+export
+search : {auto c : Ref Ctxt Defs} ->
+         {auto u : Ref UST UState} ->
+         FC -> RigCount ->
+         (defining : Name) -> (topTy : Term vars) -> Env Term vars -> 
+         Core (Term vars)
+
+record ArgInfo (vars : List Name) where
+  constructor MkArgInfo
+  holeID : Int
+  argRig : RigCount
+  appInf : AppInfo
+  metaApp : Term vars
+  argType : NF vars
+
+mkArgs : {auto c : Ref Ctxt Defs} ->
+         {auto u : Ref UST UState} ->
+         FC -> RigCount ->
+         Env Term vars -> NF vars -> 
+         Core (List (ArgInfo vars), NF vars)
+mkArgs fc rigc env (NBind nfc x (Pi c p ty) sc)
+    = do defs <- get Ctxt
+         empty <- clearDefs defs
+         nm <- genName "sa"
+         argTy <- quote empty env ty
+         let argRig = rigMult rigc c
+         (idx, arg) <- newMeta fc argRig env nm argTy
+         -- setInvertible fc argName
+         (rest, restTy) <- mkArgs fc rigc env 
+                              !(sc (toClosure defaultOpts env arg))
+         pure (MkArgInfo idx argRig (appInf Nothing p) arg ty :: rest, restTy)
+mkArgs fc rigc env ty = pure ([], ty)
+
+closureApply : FC -> Closure vars -> List (ArgInfo vars) -> 
+               Core (Term vars)
+closureApply fc (MkClosure _ [] _ tm) args 
+    = pure (applyInfo fc tm (map (\i => (appInf i, metaApp i)) args))
+closureApply _ _ _ = throw (InternalError "Wrong argument form in AutoSearch")
+
+searchIfHole : {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               FC -> 
+               (defining : Name) -> (topTy : Term vars) -> Env Term vars -> 
+               SearchEnv vars ->
+               (arg : ArgInfo vars) -> 
+               Core () 
+searchIfHole fc def top env locs arg 
+    = do let hole = holeID arg
+         let rig = argRig arg
+
+         defs <- get Ctxt
+         Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
+              | Nothing => throw (CantSolveGoal fc env top)
+         let Hole inv = definition gdef
+              | _ => pure () -- already solved
+         argdef <- searchType fc rig def top env locs (argType arg)
+         vs <- unify InTerm fc env !(nf defs env (metaApp arg)) argdef
+         let [] = constraints vs
+              | _ => throw (CantSolveGoal fc env top)
+         pure ()
+
+searchLocal : {auto c : Ref Ctxt Defs} ->
+              {auto u : Ref UST UState} ->
+              FC -> RigCount ->
+              (defining : Name) -> (topTy : Term vars) ->
+              Env Term vars -> SearchEnv vars -> SearchEnv vars -> 
+              (target : NF vars) -> Core (NF vars)
+searchLocal fc rigc def top env locs [] target
+    = throw (CantSolveGoal fc env top)
+searchLocal fc rigc def top env locs ((ty, c) :: rest) target
+    = tryUnify 
+         (do (args, appTy) <- mkArgs fc rigc env ty
+             -- TODO: Can only use the local if it's not an unsolved hole
+             ures <- unify InTerm fc env target appTy
+             let [] = constraints ures
+                 | _ => throw (CantSolveGoal fc env top)
+             candidate <- closureApply fc c args
+             traverse (searchIfHole fc def top env locs) args
+             defs <- get Ctxt
+             nf defs env candidate)
+         (searchLocal fc rigc def top env locs rest target)
+
+searchType fc rigc def top env locs (NBind nfc x (Pi c p ty) sc)
+    = pure (NBind nfc x (Lam c p ty)
+             (\arg => searchType fc rigc def top env ((ty, arg) :: locs) !(sc arg)))
+searchType fc rigc def top env locs target
+    = searchLocal fc rigc def top env locs locs target
+
+-- Declared at the top
+search fc rigc def top env
+    = do defs <- get Ctxt
+         tm <- searchType fc rigc def top env []
+                          !(nf defs env top)
+         empty <- clearDefs defs
+         quote empty env tm
+
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 48a1b81..9803b1a 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -498,6 +498,10 @@ export
 lookupTyExact : Name -> Context GlobalDef -> Core (Maybe ClosedTerm)
 lookupTyExact = lookupExactBy type 
 
+export
+lookupTyName : Name -> Context GlobalDef -> Core (List (Name, Int, ClosedTerm))
+lookupTyName = lookupNameBy type 
+
 -- Set the default namespace for new definitions
 export
 setNS : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index c369103..575fa27 100644
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@@ -52,7 +52,7 @@ data Error
     | IncompatibleFieldUpdate FC (List String)
     | InvalidImplicits FC (Env Term vars) (List (Maybe Name)) (Term vars)
     | TryWithImplicits FC (Env Term vars) (List (Name, Term vars))
-    | CantSolveGoal FC (Term [])
+    | CantSolveGoal FC (Env Term vars) (Term vars)
     | DeterminingArg FC Name (Env Term vars) (Term vars)
     | UnsolvedHoles (List (FC, Name))
     | CantInferArgType FC (Env Term vars) Name Name (Term vars)
@@ -171,7 +171,8 @@ Show Error where
      = show fc ++ ":Need to bind implicits " 
           ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
           ++ "\n(The front end should probably have done this for you. Please report!)"
-  show (CantSolveGoal fc g) = show fc ++ ":Can't solve goal " ++ assert_total (show g)
+  show (CantSolveGoal fc env g) 
+      = show fc ++ ":Can't solve goal " ++ assert_total (show g)
   show (DeterminingArg fc n env g)
       = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++ 
                 " since argument " ++ show n ++ " can't be inferred"
@@ -263,7 +264,7 @@ getErrorLoc (NotRecordType loc _) = Just loc
 getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
 getErrorLoc (InvalidImplicits loc _ y tm) = Just loc
 getErrorLoc (TryWithImplicits loc _ _) = Just loc
-getErrorLoc (CantSolveGoal loc tm) = Just loc
+getErrorLoc (CantSolveGoal loc _ tm) = Just loc
 getErrorLoc (DeterminingArg loc y env tm) = Just loc
 getErrorLoc (UnsolvedHoles ((loc, _) :: xs)) = Just loc
 getErrorLoc (UnsolvedHoles []) = Nothing
diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr
index af4693a..a37c8e7 100644
--- a/src/Core/UnifyState.idr
+++ b/src/Core/UnifyState.idr
@@ -276,14 +276,14 @@ export
 newMeta : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           FC -> RigCount ->
-          Env Term vars -> Name -> Term vars -> Core (Term vars)
+          Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
 newMeta {vars} fc rig env n ty
     = do let hty = abstractEnvType fc env ty
          let hole = newDef fc n rig hty Public (Hole False)
          log 10 $ "Adding new meta " ++ show n
          idx <- addDef n hole 
          addHoleName fc n idx
-         pure (Meta fc n idx envArgs)
+         pure (idx, Meta fc n idx envArgs)
   where
     envArgs : List (Term vars)
     envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index e8ce90f..3593187 100644
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@@ -263,7 +263,7 @@ mutual
            let argTyG = gnf defs env argTy
            -- Can't use 'metaVar' to record it for binding because it's
            -- in a different scope... so it'll stay global
-           retTy <- newMeta {vars = argn :: vars}
+           (_, retTy) <- newMeta {vars = argn :: vars}
                             fc Rig0 (Pi RigW Explicit argTy :: env) 
                             retn (TType fc)
            (argv, argt) <- check rig (nextLevel elabinfo)
diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr
index 5a33842..86e22c9 100644
--- a/src/TTImp/Elab/Check.idr
+++ b/src/TTImp/Elab/Check.idr
@@ -186,7 +186,8 @@ metaVar : {auto c : Ref Ctxt Defs} ->
           FC -> RigCount ->
           Env Term vars -> Name -> Term vars -> Core (Term vars)
 metaVar fc rig env n ty
-    = newMeta fc rig env n ty
+    = do (_, tm) <- newMeta fc rig env n ty
+         pure tm
 
 -- Elaboration info (passed to recursive calls)
 public export
diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr
index c679bcf..8499042 100644
--- a/src/Yaffle/REPL.idr
+++ b/src/Yaffle/REPL.idr
@@ -1,5 +1,6 @@
 module Yaffle.REPL
 
+import Core.AutoSearch
 import Core.Context
 import Core.Core
 import Core.Env
@@ -7,6 +8,7 @@ import Core.FC
 import Core.Normalise
 import Core.TT
 import Core.Unify
+import Core.Value
 
 import TTImp.Elab
 import TTImp.Elab.Check
@@ -40,13 +42,16 @@ process (Check ttimp)
          ty <- normaliseHoles defs [] tyh
          coreLift (printLn !(toFullNames ty))
          pure True
-process (ProofSearch n)
-    = do throw (InternalError "Not implemented")
---          tm <- search () False 1000 [] (UN "(interactive)") Nothing n
---          gam <- get Ctxt
---          coreLift (putStrLn (show (normalise gam [] tm)))
---          dumpConstraints 0 True
---          pure True
+process (ProofSearch n_in)
+    = do defs <- get Ctxt
+         [(n, i, ty)] <- lookupTyName n_in (gamma defs)
+              | [] => throw (UndefinedName toplevelFC n_in)
+              | ns => throw (AmbiguousName toplevelFC (map fst ns))
+         def <- search toplevelFC RigW n ty []
+         defs <- get Ctxt
+         defnf <- normaliseHoles defs [] def
+         coreLift (printLn !(toFullNames defnf))
+         pure True
 process (DebugInfo n)
     = do defs <- get Ctxt
          traverse showInfo !(lookupDefName n (gamma defs))
diff --git a/yaffle.ipkg b/yaffle.ipkg
index 3295a78..dbd734a 100644
--- a/yaffle.ipkg
+++ b/yaffle.ipkg
@@ -3,6 +3,7 @@ package yaffle
 modules = 
     Control.Delayed,
 
+    Core.AutoSearch,
     Core.Binary,
     Core.CaseBuilder,
     Core.CaseTree,