@@ -102,15 +102,16 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
103 -- these have been discovered as builtins but are not listed
103 -- these have been discovered as builtins but are not listed
104 -- among Idris.Primitives.primitives
104 -- among Idris.Primitives.primitives
105− , it "mkForeignPrim" [2]
106− , it "mkForeign" [1]
107− , mn "__MkPair" [0,1]
105+ , mn "__MkPair" [0,1]
109− -- special prims: believe_me only uses its third argument
107+ -- believe_me only uses its third argument
108+ -- it is special-cased in usedNames above
110 , it "prim__believe_me" [2]
109 , it "prim__believe_me" [2]
112 -- in general, all other primitives use all their arguments
111 -- in general, all other primitives use all their arguments
113 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
112 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
114+ -- mkForeign* functions are special-cased below
@@ -232,10 +233,19 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
232 -- applications may add items to Cond
233 -- applications may add items to Cond
233 getDepsTerm vs bs cd app@(App _ _)
234 getDepsTerm vs bs cd app@(App _ _)
234 | (fun, args) <- unApply app = case fun of
235 | (fun, args) <- unApply app = case fun of
235 -- constructors
237 -- constructors
236 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
238 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
237 P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used
239 P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used
241+ -- mkForeign* calls must be special-cased because they are variadic
242+ -- All arguments must be marked as used, except for the first one,
243+ -- which is the (Foreign a) spec that defines the type
244+ -- and is not needed at runtime.
246+ | n `elem` map T.pack ["mkForeign", "mkForeignPrim", "mkLazyForeignPrim"]
247+ -> unconditionalDeps (drop 1 args)
239 -- a bound variable might draw in additional dependencies,
249 -- a bound variable might draw in additional dependencies,
240 -- think: f x = x 0 <-- here, `x' _is_ used
250 -- think: f x = x 0 <-- here, `x' _is_ used