@@ -250,21 +250,44 @@ goal h tm = g [] tm where
250250
251251tactic :: Hole -> RunTactic -> StateT TState TC ()
252252tactic h f = do ps <- get
253− tm' <- atH (context ps) [] (pterm ps)
253+ (tm', _) <- atH (context ps) [] (pterm ps)
254254 ps <- get -- might have changed while processing
255255 put (ps { pterm = tm' })
256256 where
257− atH c env binder@(Bind n b sc)
258− | hole b && same h n = f c env binder
257+ updated o = do o' <- o
258+ return (o', True)
259+
260+ ulift2 c env op a b
261+ = do (b', u) <- atH c env b
262+ if u then return (op a b', True)
263+ else do (a', u) <- atH c env a
264+ return (op a' b', u)
265+
266+ -- Search the things most likely to contain the binding first!
267+
268+ atH :: Context -> Env -> Term -> StateT TState TC (Term, Bool)
269+ atH c env binder@(Bind n b@(Guess t v) sc)
270+ | same h n = updated (f c env binder)
259271 | otherwise
260− = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
261− atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
262− atH c env t = return t
272+ = do -- binder first
273+ (b', u) <- ulift2 c env Guess t v
274+ if u then return (Bind n b' sc, True)
275+ else do (sc', u) <- atH c ((n, b) : env) sc
276+ return (Bind n b' sc', u)
277+ atH c env binder@(Bind n b sc)
278+ | hole b && same h n = updated (f c env binder)
279+ | otherwise -- scope first
280+ = do (sc', u) <- atH c ((n, b) : env) sc
281+ if u then return (Bind n b sc', True)
282+ else do (b', u) <- atHb c env b
283+ return (Bind n b' sc', u)
284+ atH c env (App f a) = ulift2 c env App f a
285+ atH c env t = return (t, False)
263286
264− atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
265− atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
266− atHb c env t = do ty' <- atH c env (binderTy t)
267− return $ t { binderTy = ty' }
287+ atHb c env (Let t v) = ulift2 c env Let t v
288+ atHb c env (Guess t v) = ulift2 c env Guess t v
289+ atHb c env t = do (ty', u) <- atH c env (binderTy t)
290+ return (t { binderTy = ty' }, u)
268291
269292computeLet :: Context -> Name -> Term -> Term
270293computeLet ctxt n tm = cl [] tm where
@@ -453,8 +476,8 @@ solve ctxt env (Bind x (Guess ty val) sc)
453476 -- dontunify = dontunify ps \\ [x],
454477 -- unified = (uh, uns ++ [(x, val)]),
455478 instances = instances ps \\ [x] })
456− return $ {- Bind x (Let ty val) sc -}
457− instantiate val (pToV x sc)
479+ let tm' = instantiate val (pToV x sc) in
480+ return tm'
458481 | otherwise = lift $ tfail $ IncompleteTerm val
459482solve _ _ h@(Bind x t sc)
460483 = do ps <- get