@@ -317,16 +317,24 @@ apply fn imps =
317317 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
318318 -- so do nothing
319319 ptm <- get_term
320− let dontunify = [] -- map fst (filter (not.snd) (zip args (map fst imps)))
320+ let dontunify = if null imps then [] -- do all we can
321+ else
322+ map fst (filter (not.snd) (zip args (map fst imps)))
321323 ES (p, a) s prev <- get
322− let (n, hs) = unified p
323− let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)
324− put (ES (p { unified = unify }, a) s prev)
324+ let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dontunify)) $
325+ unified p
326+ let unify = dropGiven dontunify hs
327+ put (ES (p { unified = (n, unify) }, a) s prev)
325328 end_unify
326− return (map (updateUnify hs) args)
329+ return (map (updateUnify unify) args)
327330 where updateUnify hs n = case lookup n hs of
328331 Just (P _ t _) -> t
329332 _ -> n
333+ dropGiven du [] = []
334+ dropGiven du ((n, P a t ty) : us) | n `elem` du && not (t `elem` du)
335+ = (t, P a n ty) : dropGiven du us
336+ dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us
337+ dropGiven du (u : us) = u : dropGiven du us
330338
331339apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
332340apply2 fn elabs =