@@ -47,14 +47,16 @@ build ist info pattern fn tm
4747 when (not pattern) $
4848 mapM_ (\n -> when (n `elem` hs) $
4949 do focus n
50− try (resolveTC 7 fn ist)
50+ g <- goal
51+ try (resolveTC 7 g fn ist)
5152 (movelast n)) ivs
5253 ivs <- get_instances
5354 hs <- get_holes
5455 when (not pattern) $
5556 mapM_ (\n -> when (n `elem` hs) $
5657 do focus n
57− resolveTC 7 fn ist) ivs
58+ g <- goal
59+ resolveTC 7 g fn ist) ivs
5860 tm <- get_term
5961 ctxt <- get_context
6062 when (not pattern) $ do matchProblems; unifyProblems
@@ -150,12 +152,12 @@ elab ist info pattern tcgen fn tm
150152 (elab' ina (PRef fc unitTy))
151153 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
152154 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
153− = resolveTC 5 fn ist
155+ = do g <- goal; resolveTC 5 g fn ist
154156 elab' ina (PResolveTC fc)
155157 | True = do c <- unique_hole (MN 0 "class")
156158 instanceArg c
157159 | otherwise = do g <- goal
158− try (resolveTC 2 fn ist)
160+ try (resolveTC 2 g fn ist)
159161 (do c <- unique_hole (MN 0 "class")
160162 instanceArg c)
161163 elab' ina (PRefl fc t)
@@ -414,7 +416,7 @@ elab ist info pattern tcgen fn tm
414416 hs <- get_holes
415417 if all (\n -> not (n `elem` hs)) (freeNames g)
416418 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
417− then try (resolveTC 7 fn ist)
419+ then try (resolveTC 7 g fn ist)
418420 (movelast n)
419421 else movelast n)
420422 (ivs' \\ ivs)
@@ -649,10 +651,10 @@ proofSearch' ist top n hints
649651 = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
650652
651653
652−resolveTC :: Int -> Name -> IState -> ElabD ()
653−resolveTC 0 fn ist = fail $ "Can't resolve type class"
654−resolveTC 1 fn ist = try' (trivial' ist) (resolveTC 0 fn ist) True
655−resolveTC depth fn ist
654+resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
655+resolveTC 0 topg fn ist = fail $ "Can't resolve type class"
656+resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
657+resolveTC depth topg fn ist
656658 = do hnf_compute
657659 g <- goal
658660 ptm <- get_term
@@ -701,7 +703,7 @@ resolveTC depth fn ist
701703
702704 blunderbuss t d [] = do -- c <- get_env
703705 -- ps <- get_probs
704− lift $ tfail $ CantResolve t
706+ lift $ tfail $ CantResolve topg
705707 blunderbuss t d (n:ns)
706708 | n /= fn && tcname n = try' (resolve n d)
707709 (blunderbuss t d ns) True
@@ -729,7 +731,7 @@ resolveTC depth fn ist
729731 t' <- goal
730732 let (tc', ttype) = unApply t'
731733 let depth' = if t == t' then depth - 1 else depth
732− resolveTC depth' fn ist)
734+ resolveTC depth' topg fn ist)
733735 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
734736 -- if there's any arguments left, we've failed to resolve
735737 hs <- get_holes