@@ -347,9 +347,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
347347 -- applications may add items to Cond
348348 getDepsTerm vs bs cd app@(App _ _)
349349 | (fun, args) <- unApply app = case fun of
350− -- constructors
350+ -- instance constructors -> create metamethod deps
351+ P (DCon _ _) ctorName@(SN (InstanceCtorN className)) _
352+ -> conditionalDeps ctorName args -- regular data ctor stuff
353+ `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff
354+
355+ -- ordinary constructors
351356 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
352− P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used
357+ P (DCon _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used
353358
354359 -- mkForeign* calls must be special-cased because they are variadic
355360 -- All arguments must be marked as used, except for the first one,
@@ -365,7 +370,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
365370 -- local name that refers to a method
366371 | Just var <- M.lookup n vs
367372 , Just meth <- viMethod var
368− -> node meth args -- use the method instead
373+ -> viDeps var `ins` conditionalDeps meth args -- use the method instead
369374
370375 -- local name
371376 | Just var <- M.lookup n vs
@@ -375,7 +380,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
375380 -- global name
376381 | otherwise
377382 -- depends on whether the referred thing uses its argument
378− -> node n args
383+ -> conditionalDeps n args
379384
380385 -- TODO: could we somehow infer how bound variables use their arguments?
381386 V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)
@@ -395,15 +400,31 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
395400 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args
396401 where
397402 ins = M.insertWith (M.unionWith S.union) cd
398− unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args
399403
400− node :: Name -> [Term] -> Deps
401− node n = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices
404+ unconditionalDeps :: [Term] -> Deps
405+ unconditionalDeps = unionMap (getDepsTerm vs bs cd)
406+
407+ conditionalDeps :: Name -> [Term] -> Deps
408+ conditionalDeps n
409+ = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices
402410 where
403411 indices = map Just [0 .. getArity n - 1] ++ repeat Nothing
404412 getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional
405413 getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional
406414
415+ methodDeps :: Name -> (Int, Term) -> Deps
416+ methodDeps ctorName (methNo, t) = getDepsTerm vars bruijns cond t
417+ where
418+ vars = M.fromList [(v, VI
419+ { viDeps = M.singleton (metameth, Arg i) S.empty
420+ , viFunArg = Just i
421+ , viMethod = Nothing
422+ }) | (v, i) <- zip args [0..]]
423+ bruijns = reverse [\cd -> M.singleton cd (M.singleton (metameth, Arg i) S.empty) | i <- [0..length args-1]]
424+ cond = S.singleton (metameth, Result)
425+ metameth = mkField ctorName methNo
426+ (args, body) = unfoldLams t
427+
407428 -- projections
408429 getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n
409430 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t
@@ -444,6 +465,11 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
444465 lamToLet (x:xs) t = App (lamToLet xs t) x
445466 lamToLet [] t = t
446467
468+ -- split "\x_i -> T(x_i)" into [x_i] and T
469+ unfoldLams :: Term -> ([Name], Term)
470+ unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')
471+ unfoldLams t = ([], t)
472+
447473 mkField :: Name -> Int -> Name
448474 mkField ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")
449475