@@ -57,7 +57,7 @@ build ist info emode opts fn tm
57 mapM_ (\n -> when (n `elem` hs) $
57 mapM_ (\n -> when (n `elem` hs) $
58 do focus n
58 do focus n
60− try (resolveTC 7 g fn ist)
60+ try (resolveTC True 7 g fn ist)
61 (movelast n)) ivs
61 (movelast n)) ivs
62 ivs <- get_instances
62 ivs <- get_instances
63 hs <- get_holes
63 hs <- get_holes
@@ -65,7 +65,7 @@ build ist info emode opts fn tm
65 mapM_ (\n -> when (n `elem` hs) $
65 mapM_ (\n -> when (n `elem` hs) $
66 do focus n
66 do focus n
68− resolveTC 7 g fn ist) ivs
68+ resolveTC True 7 g fn ist) ivs
69 tm <- get_term
69 tm <- get_term
70 ctxt <- get_context
70 ctxt <- get_context
71 probs <- get_probs
71 probs <- get_probs
@@ -243,7 +243,7 @@ elab ist info emode opts fn tm
243 (elab' ina (PRef fc unitTy))
243 (elab' ina (PRef fc unitTy))
244 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
244 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
245 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
245 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
247 elab' ina (PResolveTC fc)
247 elab' ina (PResolveTC fc)
248 = do c <- getNameFrom (sMN 0 "class")
248 = do c <- getNameFrom (sMN 0 "class")
249 instanceArg c
249 instanceArg c
@@ -405,18 +405,18 @@ elab ist info emode opts fn tm
405 focus valn
405 focus valn
406 elabE (True, a, True, qq) val
406 elabE (True, a, True, qq) val
407 ivs' <- get_instances
407 ivs' <- get_instances
409+ elabE (True, a, inty, qq) sc
408 when (not pattern) $
410 when (not pattern) $
409 mapM_ (\n -> do focus n
411 mapM_ (\n -> do focus n
410 g <- goal
412 g <- goal
411 hs <- get_holes
413 hs <- get_holes
412 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
414 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
413 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
415 -- 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)
415 (movelast n)
417 (movelast n)
416 else movelast n)
418 else movelast n)
417 (ivs' \\ ivs)
419 (ivs' \\ ivs)
419− elabE (True, a, inty, qq) sc
420 -- HACK: If the name leaks into its type, it may leak out of
420 -- HACK: If the name leaks into its type, it may leak out of
421 -- scope outside, so substitute in the outer scope.
421 -- scope outside, so substitute in the outer scope.
422 expandLet n (case lookup n env of
422 expandLet n (case lookup n env of
@@ -543,7 +543,7 @@ elab ist info emode opts fn tm
543 hs <- get_holes
543 hs <- get_holes
544 if all (\n -> not (n `elem` hs)) (freeNames g)
544 if all (\n -> not (n `elem` hs)) (freeNames g)
545 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
545 -- 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)
547 (movelast n)
547 (movelast n)
548 else movelast n)
548 else movelast n)
549 (ivs' \\ ivs)
549 (ivs' \\ ivs)
@@ -1004,12 +1004,12 @@ proofSearch' ist rec depth prv top n hints
1004 proofSearch rec prv depth
1004 proofSearch rec prv depth
1005 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
1005 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
1007−resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
1007+resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
1008resolveTC = resTC' []
1008resolveTC = resTC' []
1010−resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"
1010+resTC' tcs def 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
1011+resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
1012−resTC' tcs depth topg fn ist
1012+resTC' tcs defaultOn depth topg fn ist
1013 = do hnf_compute
1013 = do hnf_compute
1014 g <- goal
1014 g <- goal
1015 ptm <- get_term
1015 ptm <- get_term
@@ -1040,7 +1040,7 @@ resTC' tcs depth topg fn ist
1041 numclass = sNS (sUN "Num") ["Classes","Prelude"]
1041 numclass = sNS (sUN "Num") ["Classes","Prelude"]
1043− needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass
1043+ needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
1044 = do focus a
1044 = do focus a
1045 fill (RConstant (AType (ATInt ITBig))) -- default Integer
1045 fill (RConstant (AType (ATInt ITBig))) -- default Integer
@@ -1085,7 +1085,7 @@ resTC' tcs depth topg fn ist
1085 let got = fst (unApply t)
1085 let got = fst (unApply t)
1086 let depth' = if tc' `elem` tcs
1086 let depth' = if tc' `elem` tcs
1087 then depth - 1 else depth
1087 then depth - 1 else depth
1088− resTC' (got : tcs) depth' topg fn ist)
1088+ resTC' (got : tcs) defaultOn depth' topg fn ist)
1089 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
1089 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
1090 -- if there's any arguments left, we've failed to resolve
1090 -- if there's any arguments left, we've failed to resolve
1091 hs <- get_holes
1091 hs <- get_holes