@@ -408,6 +408,8 @@ instanceArg n ctxt env (Bind x (Hole t) sc)
408408 ps { holes = (hs \\ [x]) ++ [x],
409409 instances = x:is })
410410 return (Bind x (Hole t) sc)
411+instanceArg n ctxt env _
412+ = fail "The current focus is not a hole."
411413
412414autoArg :: Name -> RunTactic
413415autoArg n ctxt env (Bind x (Hole t) sc)
@@ -418,6 +420,8 @@ autoArg n ctxt env (Bind x (Hole t) sc)
418420 autos = (x, (while_elaborating ps, refsIn t)) : autos ps }
419421 Just _ -> ps)
420422 return (Bind x (Hole t) sc)
423+autoArg n ctxt env _
424+ = fail "The current focus not a hole."
421425
422426setinj :: Name -> RunTactic
423427setinj n ctxt env (Bind x b sc)
@@ -439,6 +443,7 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
439443 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
440444
441445 getP (n, b) = P Bound n (binderTy b)
446+defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."
442447
443448-- as defer, but build the type and application explicitly
444449deferType :: Name -> Raw -> [Name] -> RunTactic
@@ -454,6 +459,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
454459 getP n = case lookup n env of
455460 Just b -> P Bound n (binderTy b)
456461 Nothing -> error ("deferType can't find " ++ show n)
462+deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."
457463
458464regret :: RunTactic
459465regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
@@ -462,12 +468,14 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
462468 return sc
463469regret ctxt env (Bind x (Hole t) _)
464470 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
471+regret _ _ _ = fail "The current focus is not a hole."
465472
466473unifyGoal :: Raw -> RunTactic
467474unifyGoal tm ctxt env h@(Bind x b sc) =
468475 do (tmv, _) <- lift $ check ctxt env tm
469476 ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
470477 return h
478+unifyGoal _ _ _ _ = fail "The focus is not a binder."
471479
472480exact :: Raw -> RunTactic
473481exact guess ctxt env (Bind x (Hole ty) sc) =