@@ -245,12 +245,8 @@ elab ist info emode opts fn tm
245245 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
246246 = do g <- goal; resolveTC 5 g fn ist
247247 elab' ina (PResolveTC fc)
248− | True = do c <- getNameFrom (sMN 0 "class")
249− instanceArg c
250− | otherwise = do g <- goal
251− try (resolveTC 2 g fn ist)
252− (do c <- getNameFrom (sMN 0 "class")
253− instanceArg c)
248+ = do c <- getNameFrom (sMN 0 "class")
249+ instanceArg c
254250 elab' ina (PRefl fc t)
255251 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
256252 pimp (sMN 0 "x") t False])
@@ -485,7 +481,9 @@ elab ist info emode opts fn tm
485481 -- we can unify with them
486482 case lookupCtxt f (idris_classes ist) of
487483 [] -> return ()
488− _ -> mapM_ setInjective (map getTm args)
484+ _ -> do mapM_ setInjective (map getTm args)
485+ -- maybe more things are solvable now
486+ unifyProblems
489487 ctxt <- get_context
490488 let guarded = isConName f ctxt
491489-- trace ("args is " ++ show args) $ return ()
@@ -498,10 +496,11 @@ elab ist info emode opts fn tm
498496 -- Sort so that the implicit tactics and alternatives go last
499497 let (ns', eargs) = unzip $
500498 sortBy cmpArg (zip ns args)
499+ ulog <- getUnifyLog
501500 elabArgs ist (ina || not isinf, guarded, inty, qq)
502501 [] fc False f ns'
503502 (f == sUN "Force")
504− (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
503+ (map (\x -> getTm x) eargs) -- TODO: remove this False arg
505504 solve
506505 ivs' <- get_instances
507506 -- Attempt to resolve any type classes which have 'complete' types,
@@ -525,16 +524,23 @@ elab ist info emode opts fn tm
525524 -- FIXME: Better would be to allow alternative resolution to be
526525 -- retried after more information is in.
527526 cmpArg (_, x) (_, y)
527+ | constraint x && not (constraint y) = LT
528+ | constraint y && not (constraint x) = GT
529+ | otherwise
528530 = compare (conDepth 0 (getTm x) + priority x + alt x)
529531 (conDepth 0 (getTm y) + priority y + alt y)
530532 where alt t = case getTm t of
531533 PAlternative False _ -> 5
532− PAlternative True _ -> 1
534+ PAlternative True _ -> 2
533535 PTactics _ -> 150
534− PLam _ _ _ -> 2
535− PRewrite _ _ _ _ -> 3
536− _ -> 0
537−
536+ PLam _ _ _ -> 3
537+ PRewrite _ _ _ _ -> 4
538+ PResolveTC _ -> 0
539+ _ -> 1
540+
541+ constraint (PConstraint _ _ _ _) = True
542+ constraint _ = False
543+
538544 -- Score a point for every level where there is a non-constructor
539545 -- function (so higher score --> done later)
540546 -- Only relevant when on lhs
@@ -546,6 +552,7 @@ elab ist info emode opts fn tm
546552 conDepth d (PPatvar _ _) = 0
547553 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
548554 conDepth d Placeholder = 0
555+ conDepth d (PResolveTC _) = 0
549556 conDepth d t = max (100 - d) 1
550557
551558 checkIfInjective n = do
@@ -558,7 +565,14 @@ elab ist info emode opts fn tm
558565 case lookupCtxt c (idris_classes ist) of
559566 [] -> return ()
560567 _ -> -- type class, set as injective
561− mapM_ setinjArg args
568+ do mapM_ setinjArg args
569+ -- maybe we can solve more things now...
570+ ulog <- getUnifyLog
571+ probs <- get_probs
572+ traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $
573+ unifyProblems
574+ probs <- get_probs
575+ traceWhen ulog (qshow probs) $ return ()
562576 _ -> return ()
563577
564578 setinjArg (P _ n _) = setinj n
@@ -832,17 +846,13 @@ elab ist info emode opts fn tm
832846 -> Name -- ^ Name of the function being applied
833847 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)
834848 -> Bool -- ^ under a 'force'
835− -> [(Bool, PTerm)] -- ^ (Laziness, argument)
849+ -> [PTerm] -- ^ (Laziness, argument)
836850 -> ElabD ()
837851 elabArgs ist ina failed fc retry f [] force _ = return ()
838− elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)
852+ elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)
839853 = elabArgs ist ina failed fc r f ns force args
840− elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
841− | lazy && not pattern
842− = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))
843− [pimp (sUN "a") Placeholder True,
844− pexp t])
845− | otherwise = elabArg argName holeName t
854+ elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)
855+ = do elabArg argName holeName t
846856 where elabArg argName holeName t =
847857 do now_elaborating fc f argName
848858 wrapErr f argName $ do
@@ -854,7 +864,11 @@ elab ist info emode opts fn tm
854864 failed' <- -- trace (show (n, t, hs, tm)) $
855865 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
856866 case holeName `elem` hs of
857− True -> do focus holeName; elab ina t; return failed
867+ True -> do focus holeName;
868+ g <- goal
869+ ulog <- getUnifyLog
870+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
871+ elab ina t; return failed
858872 False -> return failed
859873 done_elaborating_arg f argName
860874 elabArgs ist ina failed fc r f ns force args