@@ -294,7 +294,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
294294 -- that the result of this function is used at all
295295 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree
296296 where
297−
298297 addTagDep = case alts of
299298 [_] -> id -- single branch, tag not used
300299 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)
@@ -329,11 +328,15 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
329328 | otherwise = \j -> Nothing
330329
331330 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
332− getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
331+ getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps
333332
334333 -- named variables introduce dependencies as described in `vs'
335334 getDepsTerm vs bs cd (P _ n _)
336− -- local variables
335+ -- de bruijns (lambda-bound, let-bound vars)
336+ | Just deps <- lookup n bs
337+ = deps cd
338+
339+ -- ctor-bound/arg-bound variables
337340 | Just var <- M.lookup n vs
338341 = M.singleton cd (viDeps var)
339342
@@ -348,18 +351,18 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
348351 specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"
349352
350353 -- dependencies of de bruijn variables are described in `bs'
351− getDepsTerm vs bs cd (V i) = (bs !! i) cd
354+ getDepsTerm vs bs cd (V i) = snd (bs !! i) cd
352355
353356 getDepsTerm vs bs cd (Bind n bdr t)
354357 -- here we just push IM.empty on the de bruijn stack
355358 -- the args will be marked as used at the usage site
356− | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t
357− | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t
359+ | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t
360+ | Pi ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t
358361
359362 -- let-bound variables can get partially evaluated
360363 -- it is sufficient just to plug the Cond in when the bound names are used
361− | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t
362− | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t
364+ | Let ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t
365+ | NLet ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t
363366 where
364367 var t cd = getDepsTerm vs bs cd t
365368
@@ -386,6 +389,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
386389 -- a bound variable might draw in additional dependencies,
387390 -- think: f x = x 0 <-- here, `x' _is_ used
388391 P _ n _
392+ -- debruijn-bound name
393+ | Just deps <- lookup n bs
394+ -> deps cd `union` unconditionalDeps args
395+
389396 -- local name that refers to a method
390397 | Just var <- M.lookup n vs
391398 , Just meth <- viMethod var
@@ -402,7 +409,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
402409 -> conditionalDeps n args
403410
404411 -- TODO: could we somehow infer how bound variables use their arguments?
405− V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)
412+ V i -> snd (bs !! i) cd `union` unconditionalDeps args
406413
407414 -- we interpret applied lambdas as lets in order to reuse code here
408415 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
@@ -418,6 +425,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
418425
419426 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args
420427 where
428+ union = M.unionWith $ M.unionWith S.union
421429 ins = M.insertWith (M.unionWith S.union) cd
422430
423431 unconditionalDeps :: [Term] -> Deps
@@ -441,7 +449,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
441449 , viMethod = Nothing
442450 }) | (v, i) <- zip args [0..]]
443451 deps i = M.singleton (metameth, Arg i) S.empty
444− bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]
452+ bruijns = reverse [(n, \cd -> M.singleton cd (deps i)) | (i, n) <- zip [0..] args]
445453 cond = S.singleton (metameth, Result)
446454 metameth = mkFieldName ctorName methNo
447455 (args, body) = unfoldLams t