@@ -1376,7 +1376,7 @@ pruneByType _ t _ as = as
13761376
13771377findInstances :: IState -> Term -> [Name]
13781378findInstances ist t
1379− | (P _ n _, _) <- unApply t
1379+ | (P _ n _, _) <- unApply (getRetTy t)
13801380 = case lookupCtxt n (idris_classes ist) of
13811381 [CI _ _ _ _ _ ins _] -> filter accessible ins
13821382 _ -> []
@@ -1427,17 +1427,17 @@ resTC' tcs defaultOn topholes depth topg fn ist
14271427 = do compute
14281428 g <- goal
14291429 let argsok = tcArgsOK g topholes
1430−-- trace (show (g,hs,argsok,topholes)) $
14311430 if not argsok -- && not mvok)
14321431 then lift $ tfail $ CantResolve True topg
14331432 else do
14341433 ptm <- get_term
14351434 ulog <- getUnifyLog
14361435 hs <- get_holes
1437− traceWhen ulog ("Resolving class " ++ show g) $
1436+ env <- get_env
1437+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env) $
14381438 try' (trivial' ist)
14391439 (do t <- goal
1440− let (tc, ttypes) = unApply t
1440+ let (tc, ttypes) = unApply (getRetTy t)
14411441 scopeOnly <- needsDefault t tc ttypes
14421442 let stk = elab_stack ist
14431443 let insts_in = findInstances ist t
@@ -1447,10 +1447,10 @@ resTC' tcs defaultOn topholes depth topg fn ist
14471447 let depth' = if scopeOnly then 2 else depth
14481448 blunderbuss t depth' stk (stk ++ insts)) True
14491449 where
1450− tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn
1450+ tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
14511451 = True
14521452 tcArgsOK ty hs -- if any arguments are metavariables, postpone
1453− = let (f, as) = unApply ty in
1453+ = let (f, as) = unApply (getRetTy ty) in
14541454 case f of
14551455 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
14561456 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
@@ -1467,7 +1467,7 @@ resTC' tcs defaultOn topholes depth topg fn ist
14671467 isMeta _ _ = False
14681468
14691469 notHole hs (P _ n _, c)
1470− | (P _ cn _, _) <- unApply c,
1470+ | (P _ cn _, _) <- unApply (getRetTy c),
14711471 n `elem` hs && isConName cn (tt_ctxt ist) = False
14721472 | Constant _ <- c = not (n `elem` hs)
14731473 notHole _ _ = True
@@ -1508,11 +1508,22 @@ resTC' tcs defaultOn topholes depth topg fn ist
15081508 _ -> blunderbuss t d stk ns)
15091509 | otherwise = blunderbuss t d stk ns
15101510
1511+ introImps = do g <- goal
1512+ case g of
1513+ (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing
1514+ num <- introImps
1515+ return (num + 1)
1516+ _ -> return 0
1517+
1518+ solven 0 = return ()
1519+ solven n = do solve; solven (n - 1)
1520+
15111521 resolve n depth
15121522 | depth == 0 = fail $ "Can't resolve type class"
15131523 | otherwise
1514− = do t <- goal
1515− let (tc, ttypes) = unApply t
1524+ = do lams <- introImps
1525+ t <- goal
1526+ let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
15161527-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
15171528-- else do
15181529 -- if there's a hole in the goal, don't even try
@@ -1524,14 +1535,15 @@ resTC' tcs defaultOn topholes depth topg fn ist
15241535 tm <- get_term
15251536 args <- map snd <$> try' (apply (Var n) imps)
15261537 (match_apply (Var n) imps) True
1538+ solven lams -- close any implicit lambdas we introduced
15271539 ps' <- get_probs
15281540 when (length ps < length ps' || unrecoverable ps') $
15291541 fail "Can't apply type class"
15301542-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
15311543 mapM_ (\ (_,n) -> do focus n
15321544 t' <- goal
1533− let (tc', ttype) = unApply t'
1534− let got = fst (unApply t)
1545+ let (tc', ttype) = unApply (getRetTy t')
1546+ let got = fst (unApply (getRetTy t))
15351547 let depth' = if tc' `elem` tcs
15361548 then depth - 1 else depth
15371549 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)