@@ -47,14 +47,16 @@ build ist info pattern fn tm
47 when (not pattern) $
47 when (not pattern) $
48 mapM_ (\n -> when (n `elem` hs) $
48 mapM_ (\n -> when (n `elem` hs) $
49 do focus n
49 do focus n
50− try (resolveTC 7 fn ist)
51+ try (resolveTC 7 g fn ist)
51 (movelast n)) ivs
52 (movelast n)) ivs
52 ivs <- get_instances
53 ivs <- get_instances
53 hs <- get_holes
54 hs <- get_holes
54 when (not pattern) $
55 when (not pattern) $
55 mapM_ (\n -> when (n `elem` hs) $
56 mapM_ (\n -> when (n `elem` hs) $
56 do focus n
57 do focus n
57− resolveTC 7 fn ist) ivs
59+ resolveTC 7 g fn ist) ivs
58 tm <- get_term
60 tm <- get_term
59 ctxt <- get_context
61 ctxt <- get_context
60 when (not pattern) $ do matchProblems; unifyProblems
62 when (not pattern) $ do matchProblems; unifyProblems
@@ -150,12 +152,12 @@ elab ist info pattern tcgen fn tm
150 (elab' ina (PRef fc unitTy))
152 (elab' ina (PRef fc unitTy))
151 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
153 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
152 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
154 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
153− = resolveTC 5 fn ist
155+ = do g <- goal; resolveTC 5 g fn ist
154 elab' ina (PResolveTC fc)
156 elab' ina (PResolveTC fc)
155 | True = do c <- unique_hole (MN 0 "class")
157 | True = do c <- unique_hole (MN 0 "class")
156 instanceArg c
158 instanceArg c
157 | otherwise = do g <- goal
159 | otherwise = do g <- goal
158− try (resolveTC 2 fn ist)
160+ try (resolveTC 2 g fn ist)
159 (do c <- unique_hole (MN 0 "class")
161 (do c <- unique_hole (MN 0 "class")
160 instanceArg c)
162 instanceArg c)
161 elab' ina (PRefl fc t)
163 elab' ina (PRefl fc t)
@@ -414,7 +416,7 @@ elab ist info pattern tcgen fn tm
414 hs <- get_holes
416 hs <- get_holes
415 if all (\n -> not (n `elem` hs)) (freeNames g)
417 if all (\n -> not (n `elem` hs)) (freeNames g)
416 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
418 -- 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)
418 (movelast n)
420 (movelast n)
419 else movelast n)
421 else movelast n)
420 (ivs' \\ ivs)
422 (ivs' \\ ivs)
@@ -649,10 +651,10 @@ proofSearch' ist top n hints
649 = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
651 = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
652−resolveTC :: Int -> Name -> IState -> ElabD ()
654+resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
653−resolveTC 0 fn ist = fail $ "Can't resolve type class"
655+resolveTC 0 topg fn ist = fail $ "Can't resolve type class"
654−resolveTC 1 fn ist = try' (trivial' ist) (resolveTC 0 fn ist) True
656+resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
655−resolveTC depth fn ist
657+resolveTC depth topg fn ist
656 = do hnf_compute
658 = do hnf_compute
657 g <- goal
659 g <- goal
658 ptm <- get_term
660 ptm <- get_term
@@ -701,7 +703,7 @@ resolveTC depth fn ist
702 blunderbuss t d [] = do -- c <- get_env
704 blunderbuss t d [] = do -- c <- get_env
703 -- ps <- get_probs
705 -- ps <- get_probs
704− lift $ tfail $ CantResolve t
706+ lift $ tfail $ CantResolve topg
705 blunderbuss t d (n:ns)
707 blunderbuss t d (n:ns)
706 | n /= fn && tcname n = try' (resolve n d)
708 | n /= fn && tcname n = try' (resolve n d)
707 (blunderbuss t d ns) True
709 (blunderbuss t d ns) True
@@ -729,7 +731,7 @@ resolveTC depth fn ist
729 t' <- goal
731 t' <- goal
730 let (tc', ttype) = unApply t'
732 let (tc', ttype) = unApply t'
731 let depth' = if t == t' then depth - 1 else depth
733 let depth' = if t == t' then depth - 1 else depth
732− resolveTC depth' fn ist)
734+ resolveTC depth' topg fn ist)
733 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
735 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
734 -- if there's any arguments left, we've failed to resolve
736 -- if there's any arguments left, we've failed to resolve
735 hs <- get_holes
737 hs <- get_holes