@@ -79,7 +79,7 @@ build ist info emode opts fn tm
7979 mapM_ (\n -> when (n `elem` hs) $
8080 do focus n
8181 g <- goal
82− try (resolveTC True False 7 g fn ist)
82+ try (resolveTC True False 10 g fn ist)
8383 (movelast n)) ivs
8484 ivs <- get_instances
8585 hs <- get_holes
@@ -88,7 +88,7 @@ build ist info emode opts fn tm
8888 do focus n
8989 g <- goal
9090 ptm <- get_term
91− resolveTC True True 7 g fn ist) ivs
91+ resolveTC True True 10 g fn ist) ivs
9292 tm <- get_term
9393 ctxt <- get_context
9494 probs <- get_probs
@@ -339,7 +339,7 @@ elab ist info emode opts fn tm
339339 UType _ -> elab' ina (Just fc) (PRef fc unitTy)
340340 _ -> elab' ina (Just fc) (PRef fc unitCon)
341341 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
342− = do g <- goal; resolveTC False False 5 g fn ist
342+ = do g <- goal; resolveTC False False 10 g fn ist
343343 elab' ina fc (PResolveTC fc')
344344 = do c <- getNameFrom (sMN 0 "class")
345345 instanceArg c
@@ -559,7 +559,7 @@ elab ist info emode opts fn tm
559559 g <- goal
560560 hs <- get_holes
561561 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
562− then try (resolveTC True False 7 g fn ist)
562+ then try (resolveTC True False 10 g fn ist)
563563 (movelast n)
564564 else movelast n)
565565 (ivs' \\ ivs)
@@ -719,7 +719,7 @@ elab ist info emode opts fn tm
719719 env <- get_env
720720 hs <- get_holes
721721 if all (\n -> not (n `elem` hs)) (freeNames g)
722− then try (resolveTC False False 7 g fn ist)
722+ then try (resolveTC False False 10 g fn ist)
723723 (movelast n)
724724 else movelast n)
725725 (ivs' \\ ivs)
@@ -1441,14 +1441,11 @@ resTC' tcs defaultOn topholes depth topg fn ist
14411441 try' (trivial' ist)
14421442 (do t <- goal
14431443 let (tc, ttypes) = unApply (getRetTy t)
1444− scopeOnly <- needsDefault t tc ttypes
1444+ addDefault t tc ttypes
14451445 let stk = elab_stack ist
1446− let insts_in = findInstances ist t
1447− let insts = if scopeOnly then filter chaser insts_in
1448− else insts_in
1446+ let insts = findInstances ist t
14491447 tm <- get_term
1450− let depth' = if scopeOnly then 2 else depth
1451− blunderbuss t depth' stk (stk ++ insts)) True
1448+ blunderbuss t depth stk (stk ++ insts)) True
14521449 where
14531450 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
14541451 = True
@@ -1488,14 +1485,13 @@ resTC' tcs defaultOn topholes depth topg fn ist
14881485
14891486 numclass = sNS (sUN "Num") ["Classes","Prelude"]
14901487
1491− needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
1488+ addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
14921489 = do focus a
14931490 fill (RConstant (AType (ATInt ITBig))) -- default Integer
14941491 solve
1495− return False
1496− needsDefault t f as
1497− | all boundVar as = return True -- fail $ "Can't resolve " ++ show t
1498− needsDefault t f a = return False -- trace (show t) $ return ()
1492+ addDefault t f as
1493+ | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t
1494+ addDefault t f a = return () -- trace (show t) $ return ()
14991495
15001496 boundVar (P Bound _ _) = True
15011497 boundVar _ = False