This is needed because the existing version won't build the Prelude
correctly as it doesn't do import...as correctly.
I don't believe this affects Idris2-boot, since it has its own Prelude.
There is an argument that, for import public, this should be automatic
(that is, the publicly imported things should be reexported with the
parent namespace). I decided not to do this, because another use of
import public which we do a lot in the Idris 2 code base is purely as a
convenience, where we still expect things to be in their original
namespace.
Also, where there's a choice between things being explicit and implicit,
I prefer to err on the side of explicit now.
So, if what you really want in an API is to reexport, you can do that,
but explicitly.
We only need to reload the defined names so that we can set up the
aliases - everything else is already loaded, and in particular adding
hints twice will break implicit search.
Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".
The ports are rather straight forward and I have purposefully written
the documentation to be beginner friendly.
Note, I have diverged from Idris1 over the naming of the projection
functions to make them consistent with `Pair` and `DPair`.
The flag takes a natural number as argument
It would be ideal to generalise the argument parser to be able
to parse any argument of any type, but right now we only add
`RequiredNat` as a new flag option.
If we have a delayed thing, but we don't yet know the expected type,
don't commit to forcing because the expected type might turn out to be a
delay.
Fixes#395
'convert' doesn't solve holes, so might reject things that are solvable.
This can be an issue when resolving interfaces, because we were using
convert for arguments of the invertible holes that arise when trying to
resolve them. Fixes#66.
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
