@@ -366,7 +366,7 @@ resolveTC depth fn ist
366366 tm <- get_term
367367-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
368368-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
369− let depth' = if scopeOnly then 5 else depth
369+ let depth' = if scopeOnly then 2 else depth
370370 blunderbuss t depth' insts)
371371 where
372372 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
@@ -404,7 +404,10 @@ resolveTC depth fn ist
404404 args <- apply (Var n) imps
405405-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
406406 mapM_ (\ (_,n) -> do focus n
407− resolveTC (depth - 1) fn ist)
407+ t' <- goal
408+ let (tc', ttype) = unApply t'
409+ let depth' = if t == t' then depth - 1 else depth
410+ resolveTC depth' fn ist)
408411 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
409412 -- if there's any arguments left, we've failed to resolve
410413 solve