@@ -57,7 +57,7 @@ build ist info emode opts fn tm
5757 mapM_ (\n -> when (n `elem` hs) $
5858 do focus n
5959 g <- goal
60− try (resolveTC 7 g fn ist)
60+ try (resolveTC True 7 g fn ist)
6161 (movelast n)) ivs
6262 ivs <- get_instances
6363 hs <- get_holes
@@ -65,7 +65,7 @@ build ist info emode opts fn tm
6565 mapM_ (\n -> when (n `elem` hs) $
6666 do focus n
6767 g <- goal
68− resolveTC 7 g fn ist) ivs
68+ resolveTC True 7 g fn ist) ivs
6969 tm <- get_term
7070 ctxt <- get_context
7171 probs <- get_probs
@@ -243,7 +243,7 @@ elab ist info emode opts fn tm
243243 (elab' ina (PRef fc unitTy))
244244 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
245245 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
246− = do g <- goal; resolveTC 5 g fn ist
246+ = do g <- goal; resolveTC False 5 g fn ist
247247 elab' ina (PResolveTC fc)
248248 = do c <- getNameFrom (sMN 0 "class")
249249 instanceArg c
@@ -405,18 +405,18 @@ elab ist info emode opts fn tm
405405 focus valn
406406 elabE (True, a, True, qq) val
407407 ivs' <- get_instances
408+ env <- get_env
409+ elabE (True, a, inty, qq) sc
408410 when (not pattern) $
409411 mapM_ (\n -> do focus n
410412 g <- goal
411413 hs <- get_holes
412414 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
413415 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
414− then try (resolveTC 7 g fn ist)
416+ then try (resolveTC True 7 g fn ist)
415417 (movelast n)
416418 else movelast n)
417419 (ivs' \\ ivs)
418− env <- get_env
419− elabE (True, a, inty, qq) sc
420420 -- HACK: If the name leaks into its type, it may leak out of
421421 -- scope outside, so substitute in the outer scope.
422422 expandLet n (case lookup n env of
@@ -543,7 +543,7 @@ elab ist info emode opts fn tm
543543 hs <- get_holes
544544 if all (\n -> not (n `elem` hs)) (freeNames g)
545545 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
546− then try (resolveTC 7 g fn ist)
546+ then try (resolveTC False 7 g fn ist)
547547 (movelast n)
548548 else movelast n)
549549 (ivs' \\ ivs)
@@ -1004,12 +1004,12 @@ proofSearch' ist rec depth prv top n hints
10041004 proofSearch rec prv depth
10051005 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
10061006
1007−resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
1007+resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
10081008resolveTC = resTC' []
10091009
1010−resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"
1011−resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
1012−resTC' tcs depth topg fn ist
1010+resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
1011+resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
1012+resTC' tcs defaultOn depth topg fn ist
10131013 = do hnf_compute
10141014 g <- goal
10151015 ptm <- get_term
@@ -1040,7 +1040,7 @@ resTC' tcs depth topg fn ist
10401040
10411041 numclass = sNS (sUN "Num") ["Classes","Prelude"]
10421042
1043− needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass
1043+ needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
10441044 = do focus a
10451045 fill (RConstant (AType (ATInt ITBig))) -- default Integer
10461046 solve
@@ -1085,7 +1085,7 @@ resTC' tcs depth topg fn ist
10851085 let got = fst (unApply t)
10861086 let depth' = if tc' `elem` tcs
10871087 then depth - 1 else depth
1088− resTC' (got : tcs) depth' topg fn ist)
1088+ resTC' (got : tcs) defaultOn depth' topg fn ist)
10891089 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
10901090 -- if there's any arguments left, we've failed to resolve
10911091 hs <- get_holes