This looks for an .ipkg file in a parent directory before loading the
given file, and loads it relative to the .ipkg's source directory, with
the options specified in the .ipkg.
The intention is to save all the editor modes having to do the same
thing, and especially makes it possible for the new vim mode to work
with ipkgs.
If the name is given (rather than, say, computed) update it so that it's
the data type name being defined - so ambiguities are resolved
immediately. Fixes#192
Pass through the types of the interface parameters to the top level
method types, because there might be information in there that we can't
otherwise infer. Fixes#188
This means we can say 'let x = foo' and have foo not be applied to its
implicit arguments, meaning that 'x' can be instantiated at whatever
implicits it needs through the scope.
This prevents display of shadowed names from case blocks/where clauses
that are now unusable. It does mean that constraint arguments aren't
displayed, unless given an explicit name - this may not be good, since
we might want to know which constraints are in scope, so it may yet need
a little tweaking.
This needed a bit of reorganisation, but it speeds up checking if a
module doesn't need rebuilding due to the import interfaces not
changing. Also it means that the "Type checking foo.idr" message is
displayed before parsing rather than after, which is probably better.
We've been generalising inferred function types to have multiplicity
RigW but sometimes (especially on lambdas) we need to infer the precise
type, so make a distinction.
This is pretty ugly, really. It would be better to be able to postpone
the choice until we know more, but it's not obvious to me how to achieve
that with the way unification is currently set up. The present way at
least works fine with code that doesn't use linearity, which is the
right default I think!
Now only abstracts over the environment once and deals with 'where'
clauses by rewriting the nested name with the rearranged environment. As
a result, it interacts far better with local definitions (i.e. where
blocks).
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.
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 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 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.
