@@ -157,7 +157,7 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
157157
158158 etaExpand :: [Name] -> Term -> Term
159159 etaExpand [] t = t
160− etaExpand (n : ns) t = etaExpand ns (App t (P Bound n Erased))
160+ etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))
161161
162162 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
163163 getDepsSC fn es vs ImpossibleCase = M.empty
@@ -166,8 +166,10 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
166166 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)
167167 getDepsSC fn es vs (Case n alts)
168168 -- we case-split on this variable, which necessarily marks it as used
169− = M.map (S.union casedVar) -- add the usage to all effects
170− $ unionMap (getDepsAlt fn es vs casedVar) alts -- in the whole subtree
169+ -- hence we add a new dependency whose only preconditions are that the result
170+ -- of this function is used at all
171+ = M.insertWith S.union (S.singleton (fn, Result)) casedVar -- add this dep to all deps
172+ $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree
171173 where
172174 casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
173175
@@ -222,18 +224,17 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
222224 -- applications may add items to Cond
223225 getDepsTerm vs bs cd app@(App _ _)
224226 | (fun, args) <- unApply app = case fun of
225− -- these depend on whether the referred thing uses the argument
226− P Ref n _ -> node n args
227− P (DCon _ _) n _ -> node n args
228−
229− -- this does not
230− P (TCon _ _) n _ -> unconditionalDeps args
227+ -- constructors
228+ P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
229+ P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used
231230
232231 -- a bound variable might draw in additional dependencies,
233232 -- think: f x = x 0 <-- here, `x' _is_ used
234− -- also, the arguments must be considered used
235− -- since we don't know what's in the variable
236− P Bound n _ -> var n `ins` unconditionalDeps args
233+ P _ n _
234+ | Just var <- M.lookup n vs
235+ -> var `ins` unconditionalDeps args
236+ | otherwise
237+ -> node n args -- depends on whether the referred thing uses its argument
237238
238239 -- we interpret applied lambdas as lets in order to reuse code here
239240 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
@@ -249,13 +250,15 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
249250 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args
250251 where
251252 ins = M.insertWith S.union cd
252− var n = fromMaybe (error $ "non-existent bound variable: " ++ show n) (M.lookup n vs)
253253 node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip [0..]
254254 getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t
255255 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args
256256
257+ -- projections (= methods)
258+ getDepsTerm vs bs cd (Proj t i) | ("PROJ", t, S.toList cd) `traceShow` False = undefined
259+ getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t
260+
257261 -- the easy cases
258− getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t
259262 getDepsTerm vs bs cd (Constant _) = M.empty
260263 getDepsTerm vs bs cd (TType _) = M.empty
261264 getDepsTerm vs bs cd Erased = M.empty