@@ -366,7 +366,7 @@ resolveTC depth fn ist
366 tm <- get_term
366 tm <- get_term
367-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
367-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
368-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
368-- (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
370 blunderbuss t depth' insts)
370 blunderbuss t depth' insts)
372 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
372 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
@@ -404,7 +404,10 @@ resolveTC depth fn ist
404 args <- apply (Var n) imps
404 args <- apply (Var n) imps
405-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
405-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
406 mapM_ (\ (_,n) -> do focus n
406 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)
408 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
411 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
409 -- if there's any arguments left, we've failed to resolve
412 -- if there's any arguments left, we've failed to resolve