on master help sign in
Merge pull request #2222 from ziman/ffi-erasure-fix

Fix erasure from mkForeignPrim.

commit756bfb1373895da0abaf5ce606c71258273edf3e authorDavid Christiansen <david@davidchristiansen.dk> dateFri 1 May 2015, 14:54 (11 years ago) parent59f5e640d332f8
1 file changed+4−5
src/Idris/Erasure.hs+4−5
src/Idris/Erasure.hs+4−5
@@ -382,12 +382,11 @@ buildDepMap ci used externs ctx startNames
382382 P (DCon _ _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used
383383
384384 -- mkForeign* calls must be special-cased because they are variadic
385− -- All arguments must be marked as used, except for the first one,
386− -- which is the (Foreign a) spec that defines the type
387− -- and is not needed at runtime.
385+ -- All arguments must be marked as used, except for the first four,
386+ -- which define the call type and are not needed at runtime.
388387 P _ (UN n) _
389− | n `elem` map T.pack ["mkForeignPrim"]
390− -> unconditionalDeps args -- (drop 1 args)
388+ | n == T.pack "mkForeignPrim"
389+ -> unconditionalDeps $ drop 4 args
391390
392391 -- a bound variable might draw in additional dependencies,
393392 -- think: f x = x 0 <-- here, `x' _is_ used