@@ -153,10 +153,9 @@ elab ist info pattern opts fn tm
153153 [] -> return ()
154154
155155 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
156− elabE ina t = {- do g <- goal
157− tm <- get_term
158− trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
159− $ -}
156+ elabE ina t =
157+-- do g <- goal
158+-- trace ("Elaborating " ++ show t ++ " : " ++ show g) $
160159 do ct <- insertCoerce ina t
161160 t' <- insertLazy ct
162161 g <- goal
@@ -841,9 +840,11 @@ proofSearch' ist top n hints
841840
842841
843842resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
844−resolveTC 0 topg fn ist = fail $ "Can't resolve type class"
845−resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
846−resolveTC depth topg fn ist
843+resolveTC = resTC' []
844+
845+resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"
846+resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
847+resTC' tcs depth topg fn ist
847848 = do hnf_compute
848849 g <- goal
849850 ptm <- get_term
@@ -915,8 +916,10 @@ resolveTC depth topg fn ist
915916 mapM_ (\ (_,n) -> do focus n
916917 t' <- goal
917918 let (tc', ttype) = unApply t'
918− let depth' = if t == t' then depth - 1 else depth
919− resolveTC depth' topg fn ist)
919+ let got = fst (unApply t)
920+ let depth' = if tc' `elem` tcs
921+ then depth - 1 else depth
922+ resTC' (got : tcs) depth' topg fn ist)
920923 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
921924 -- if there's any arguments left, we've failed to resolve
922925 hs <- get_holes