Some foreign function symbols not found when using type providers

[joshvera]

This fails to compile:

module Main
import Providers

%include C "math.h"
%lib C "m"
%language TypeProviders

round : Float -> IO Float
round x = mkForeign (FFun "round" [FFloat] FFloat) x

provideTwo : IO (Provider Float)
provideTwo = return $ Provide !(round 2.3)

%provide (two : Float) with provideTwo

main : IO ()
main = putStrLn $ show two

with:

Symbol "round" not found
INTERNAL ERROR: Could not call foreign function "round" with args [EBind Pi {binderTy = [__]} <<fn>>,FFun ("round") (Prelude.List.:: (FTy) (FFloat) (Prelude.List.Nil (FTy))) (FFloat),2.3,TheWorld]
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

test026.idr manages to call readFile without issues, but it seems we compile that specially. Could it be an issue with mkForeign and type providers?

[david-christiansen]

In this case, you just need to get Idris to dynamically load the C lib in question using %dynamic.

There are some issues with laziness and type providers right now - I fixed them on an airplane a couple hours ago and I'll send a PR after I test it a bit more and perhaps sleep :-)

[joshvera]

@david-christiansen Thanks! Then this was an issue with linking the library statically and has nothing to do with the laziness issues you mentioned right? Shall I close this out?

[david-christiansen]

If you've made your (perfectly reasonable) code work by adding a %dynamic directive, then I don't think this is a bug, and it should probably be closed. If adding this does not fix it, then there may be a previously unknown issue with the dynamic linking.