Always infer a multiplicity of W. Since we can pass a linear function to
one which expects an unrestricted argument, this gives the more general
result if the multiplicity is otherwise unknown.
This makes things like 'maybe id (+) x y' type check again even in the
presence of an 'id' which is declared linear!
This is the same as %auto_implicits in Idris 1, but with a more
appropriate name, because auto implicits are something else.
'%unbound_implicits off' turns off implicit forall bindings. See test
basic033 for an example.
In a small change from Idris 1, this lifts to the nearest binder or
block, so doesn't lift past an explicit "do" in particular. Blocks are:
- case branches
- if branches
- scope of local function definitions, or any binder
- do blocks
It's a big patch, but the summary is that it's okay to use a pattern in
an erased position if either:
- the pattern can also be solved by unification (this is the same as
'dot patterns' for matching on non-constructor forms)
- the argument position is detaggable w.r.t. non-erased arguments, which
means we can tell which pattern it is without pattern matching
The second case, in particular, means we can still pattern match on
proof terms which turn out to be irrelevant, especially Refl.
Fixes#178
When we check a scope in RigW, need to mark all linear things outside
that scope as irrelevant within the scope (since the scope may be used
multiple times).
This fixes the issue where some Scheme compiler like mit-scheme is
installed and that gets picked up first, leading to an infinite
loop in the tests.
Also see attached image in the PR.
This changes the behaviour of 'auto' implicits so that by default they
return the first result, rather than checking for unique results. This
is consistent with Idris 1. However, we still want to check for
uniqueness somtimes (for example, with interface search, which should
reject overlapping results) so the 'uniqueSearch' option means that any
auto implicit search for the type should check uniqueness of results.
Fixes#169
This is to help Idris2 codegen the correct scripts on NixOS where
Racket and Chicken aren't installed in the standard locations, and
the /usr/bin/env trampoline is disabled at package build time.
This now matches the existing Chez behavior.
Also, fixed the test runner to restore the correct working directory
after a failed test, and fixed the top-level Makefile to allow the
IDRIS2_VERSION variable to be queried without building the project.
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
Fixes#132. When getting the names in the block, we need to return the
fully explicit name, because we can't assume they'll all be in the same
namespace as we can have namespaces inside parameters blocks.
Can't use a local which has 'erased' as its type, since that's just been
substituted in while working out how many arguments a local function
needs to have. Also need to ensure we've searched for default hints when
encountering IBindImplicits rather than after because otherwise it might
find the wrong instance.
Both these problems result it terms which don't type check getting past
the elaborator! So, also added a --debug-elab-check flag to check the
result of elaboration. It's not on by default because there are cases
where it really hurts performance, typically when inferring implicits
with lots of sharing. So we'll keep it as a debug flag, for now at
least.
See e.g. Applicative instance in Data.Vect. This allows implementations
to use implicits at run time (by default, they'd be 0 multiplicity so
erased, but it might be useful to have an index available at run time).
At the moment, the parser requires implicits to be given before
constraints. Ideally it should be possible to give them in any order.
I'll come back to this.
