@@ -102,15 +102,16 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
102102
103103 -- these have been discovered as builtins but are not listed
104104 -- among Idris.Primitives.primitives
105− , it "mkForeignPrim" [2]
106− , it "mkForeign" [1]
107− , mn "__MkPair" [0,1]
105+ , mn "__MkPair" [0,1]
108106
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
110109 , it "prim__believe_me" [2]
111110
112111 -- in general, all other primitives use all their arguments
113112 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]
113+
114+ -- mkForeign* functions are special-cased below
114115 ]
115116 ]
116117
@@ -232,10 +233,19 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns
232233 -- applications may add items to Cond
233234 getDepsTerm vs bs cd app@(App _ _)
234235 | (fun, args) <- unApply app = case fun of
236+
235237 -- constructors
236238 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything
237239 P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used
238240
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.
245+ P _ (UN n) _
246+ | n `elem` map T.pack ["mkForeign", "mkForeignPrim", "mkLazyForeignPrim"]
247+ -> unconditionalDeps (drop 1 args)
248+
239249 -- a bound variable might draw in additional dependencies,
240250 -- think: f x = x 0 <-- here, `x' _is_ used
241251 P _ n _