@@ -106,7 +106,7 @@ computeDagP :: Ord n
106106 -> TT n
107107 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
108108computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) where
109− f (n, t) = ((n, t), M.keysSet (usedVars False t))
109+ f (n, t) = ((n, t), M.keysSet (usedVars t))
110110
111111 (numArgs, args, removedArgs, retTy) = go 0 [] [] t
112112
@@ -118,19 +118,19 @@ computeDagP removePred t = (reverse (map f args), reverse removedArgs , retTy) w
118118 go k args removedArgs retTy = (k, args, removedArgs, retTy)
119119
120120-- | Collect the names and types of all the free variables
121−usedVars :: Ord n
122− => Bool -- ^ only collect variables which must be determined due to injectivity
123− -> TT n -> Map n (TT n)
124−usedVars inj = f where
125− f (P Bound n t) = M.singleton n t `M.union` f t
126− f (Bind n binder t2) = (M.delete n (f t2) `M.union`) $ case binder of
127− Let t v -> f t `M.union` f v
128− Guess t v -> f t `M.union` f v
129− b -> f (binderTy b)
130− f (App t1 t2) = f t1 `M.union` (if not inj || isInjective t1 then f t2 else M.empty)
131− f (Proj t _) = f t
132− f (V j) = error "unexpected! run vToP first"
133− f _ = M.empty
121+-- The Boolean indicates those variables which are determined due to injectivity
122+-- I have not given nearly enough thought to know whether this is correct
123+usedVars :: Ord n => TT n -> Map n (TT n, Bool)
124+usedVars = f True where
125+ f b (P Bound n t) = M.singleton n (t, b) `M.union` f b t
126+ f b (Bind n binder t2) = (M.delete n (f b t2) `M.union`) $ case binder of
127+ Let t v -> f b t `M.union` f b v
128+ Guess t v -> f b t `M.union` f b v
129+ bind -> f b (binderTy bind)
130+ f b (App t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2
131+ f b (Proj t _) = f b t
132+ f _ (V j) = error "unexpected! run vToP first"
133+ f _ _ = M.empty
134134
135135-- | Remove a node from a directed acyclic graph
136136deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
@@ -318,18 +318,23 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
318318
319319 resolveUnis ((name, term) : xs)
320320 state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of
321− (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep
322− (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep
321+ (Just (_,ix), Nothing) -> first (addScore (mempty { leftApplied = 1, rightApplied = otherApplied})) <$> nextStep
322+ (Nothing, Just (_,ix)) -> first (addScore (mempty { rightApplied = 1, leftApplied = otherApplied})) <$> nextStep
323323 (Nothing, Nothing) -> nextStep
324324 _ -> error ("Idris internal error: TypeSearch.resolveUnis")
325325 where
326326 -- find variables which are determined uniquely by the type
327327 -- due to injectivity
328− varsInTy = M.keys $ usedVars True term
328+ matchedVarMap = usedVars term
329+ both f (x, y) = (f x, f y)
330+ (injUsedVars, notInjUsedVars) = both M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst holes) $ M.map snd matchedVarMap
331+ varsInTy = injUsedVars ++ notInjUsedVars
329332 toDelete = name : varsInTy
330333 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
331334
332− inScore f state = state { score = f (score state) }
335+ otherApplied = length notInjUsedVars
336+
337+ addScore additions state = state { score = score state `mappend` additions }
333338 state' = modifyTypes (subst name term) . deleteMany $
334339 state { holes = filter (not . (`elem` toDelete) . fst) holes }
335340 nextStep = resolveUnis xs state'