no file location to error message in a %provide directive

[colin-adams]

I'm working on getting idris-sqlite to compile in 0.11.

Most of it is working. One of the last problems was a message with no file location:

- + Errors (1)
 `-- (no file) line 0 col -1:
     Can't find implementation for Handler Sqlite m

Eventually, with help from Melvar, I found that changing

%provide (db : DB "test.sqlite")
  with run (getSchemas "test.sqlite")

to

%provide (db : DB "test.sqlite")
  with run {m = IO} (getSchemas "test.sqlite")

cured the problem. It would have been quicker to resolve if I had file name and line number information.

[david-christiansen]

It should definitely report errors correctly.

Here's a minimized example:

module P

%language TypeProviders

%provide (x : Nat) with (return (Provide foo))

dumps:

- + Errors (1)
 `-- (no file) line 0 col -1:
     When checking argument x to constructor Prelude.Providers.Provide:
             No such variable foo

There are also general problems with propagating type information here:

module P

%language TypeProviders

%provide (x : Nat) with (return (Provide 42))

yields:

- + Errors (1)
 `-- (no file) line 0 col -1:
     Can't find implementation for Monad m

and even return requires the argument m to be explicitly given!

Even this does not work:

module P

%language TypeProviders

%provide (x : Nat) with (return {m=IO} (Provide 42))

failing with

- + Errors (1)
 `-- (no file) line 0 col -1:
     Expected provider type IO (Prelude.Providers.Provider Prelude.Nat.Nat), got IO (Prelude.Providers.Provider Integer) instead.

where the types aren't even properly pretty-printed.

I suppose that's what I get for having this be my first major contribution to Idris!

Finally, the thing that works is

module P

%language TypeProviders

%provide (x : Nat) with (return {m=IO} (Provide (the Nat 42)))

Blech!