@@ -1451,6 +1451,8 @@ solveAutos ist fn ambigok
14511451
14521452trivial' ist
14531453 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1454+trivialHoles' h ist
1455+ = trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
14541456proofSearch' ist rec ambigok depth prv top n hints
14551457 = do unifyProblems
14561458 proofSearch rec prv ambigok (not prv) depth
@@ -1473,7 +1475,13 @@ resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False
14731475resTC' tcs defaultOn topholes depth topg fn ist
14741476 = do compute
14751477 g <- goal
1476− let argsok = tcArgsOK g topholes
1478+ -- Resolution can proceed only if there is something concrete in the
1479+ -- determining argument positions. Keep track of the holes in the
1480+ -- non-determining position, because it's okay for 'trivial' to solve
1481+ -- those holes and no others.
1482+ let (argsok, okholePos) = case tcArgsOK g topholes of
1483+ Nothing -> (False, [])
1484+ Just hs -> (True, hs)
14771485 if not argsok -- && not mvok)
14781486 then lift $ tfail $ CantResolve True topg
14791487 else do
@@ -1481,30 +1489,47 @@ resTC' tcs defaultOn topholes depth topg fn ist
14811489 ulog <- getUnifyLog
14821490 hs <- get_holes
14831491 env <- get_env
1484− traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env) $
1485− try' (trivial' ist)
1486− (do t <- goal
1487− let (tc, ttypes) = unApply (getRetTy t)
1488− addDefault t tc ttypes
1492+ t <- goal
1493+ let (tc, ttypes) = unApply (getRetTy t)
1494+ let okholes = case tc of
1495+ P _ n _ -> zip (repeat n) okholePos
1496+ _ -> []
1497+
1498+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
1499+ try' (trivialHoles' okholes ist)
1500+ (do addDefault t tc ttypes
14891501 let stk = elab_stack ist
14901502 let insts = findInstances ist t
14911503 tm <- get_term
14921504 blunderbuss t depth stk (stk ++ insts)) True
14931505 where
1506+ -- returns Just hs if okay, where hs are holes which are okay in the
1507+ -- goal, or Nothing if not okay to proceed
14941508 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
1495− = True
1496− tcArgsOK ty hs -- if any arguments are metavariables, postpone
1509+ = Just []
1510+ tcArgsOK ty hs -- if any determining arguments are metavariables, postpone
14971511 = let (f, as) = unApply (getRetTy ty) in
14981512 case f of
14991513 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
15001514 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
1501− Nothing -> not $ any (isMeta hs) as
1502− _ -> not $ any (isMeta hs) as
1503−
1515+ Nothing -> if any (isMeta hs) as
1516+ then Nothing
1517+ else Just []
1518+ _ -> if any (isMeta hs) as
1519+ then Nothing
1520+ else Just []
1521+
1522+ -- return the list of argument positions which can safely be a hole
1523+ -- or Nothing if one of the determining arguments is a hole
15041524 tcDetArgsOK i ds hs (x : xs)
1505− | i `elem` ds = not (isMeta hs x) && tcDetArgsOK (i + 1) ds hs xs
1506− | otherwise = tcDetArgsOK (i + 1) ds hs xs
1507− tcDetArgsOK _ _ _ [] = True
1525+ | i `elem` ds = if isMeta hs x
1526+ then Nothing
1527+ else tcDetArgsOK (i + 1) ds hs xs
1528+ | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs
1529+ case x of
1530+ P _ n _ -> Just (i : rs)
1531+ _ -> Just rs
1532+ tcDetArgsOK _ _ _ [] = Just []
15081533
15091534 isMeta :: [Name] -> Term -> Bool
15101535 isMeta ns (P _ n _) = n `elem` ns