We need to make sure they are inferred again when elaborating methods,
so substitute in a _ in method types before substituting in the explicit
parameters.
In future, it might (probably will) also be useful to allow giving the
implicit parameters explicitly when defining implementations.
Fixes#374
It's worth delaying in case doing some more work (and some more
interface resolution) can make the type more concrete. This makes
test linear011 work more smoothly, and will help with this sort of
program in general.
A better way, later, would be to try elaborating and delay only if the
type is not yet known. We have the facilities, but it's too fiddly for
me to want to implement it right now...
We need to check below top level too, since there could be holes that
we're happy to resolve by searching. The linearity test added
illustrates a place where this is needed.
The namespace parser was not requiring a minimum indentation and instead
based its indentation on the following line, which meant that a line like:
namespace Foo
foodef : Int
placed foodef into namespace Foo instead of the module's top level.
And so made it unclear when a namespace ends.
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:
- it's easier for backend authors if the type of IO operations is
slightly less restrictive. For example, if it's in HasIO, that limits
alternative implementations, which might be awkward for some
alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
instance (I have personally never encountered one - if they turns out
to exist, again, we can revisit!)
This addresses the case where you'd see an error of:
Ambiguous elaboration at:
r <- pure []
Possible correct results:
[]
[]
[]
By changing it to:
Possible correct results:
Main.Nil
PrimIO.Nil
Prelude.Nil
The output directory was previously called the executable directory, but I changed it because the output is not always an executable (depending on the code generator).
The code generators can now distinguish between where to place the (temporary) build files and the resulting output files.
unelabBinder was losing information for the purpose of displaying names
nicely. This is typically wanted but when working with elabortation it's
useful to have all the information you can get. Things like record field
names would be lost when querying with GetType but are now retained.
It takes a long time to run, but it is basically all
the testing we need of the API, if this works it's
unlikely to be broken. It requires a change in the build
system, so don't enable it for now.
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
