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.
For the types of local names, don't write out the environment - it's
going to be repeated for every name, mostly it's unhelpful, and if you
want to see the types of other names you can ask directly. This can save
a huge amount of time when environments are slightly complicated.
If a default method implementation refers to another method in the
interface, it's going to be one from the interface being defined, so
push it through explicitly.
This is only going to be guaranteed to be the case for default method
implementations - we can't assume anything for other implementations.
Fixes#77
Sometimes we swap the arguments, to reduce code duplication, but we need
to remember we've done that since (1 x : a) -> b is valid for an
argument of type (x : a) -> b, but not vice versa (that is, we have a
teensy bit of subtying to deal with, for convenience...).
This fix seems a bit ugly, but we do at least now propagate the
information. Fixes#82.
This is supported by Idris 1 and is handy for breaking cycles in
modules. To achieve this, we just need to make sure that complete
definitions aren't overwritten with empty definitions on loading.
Checking the let expression in full can break sharing when unifying the
types, and it's unnecessary because we've already checked the type of
the scope unifies with the expected type.
Fixes#63
Elaborate the scope of a let without the computational behaviour,
meaning that `let x = v in e` is equivalent to `(\x => e) v`. This makes
things more consistent (in that let bindings already don't propagate
inside case or with blocks) at the cost of not being able to rely on the
computational behaviour in types. More importantly, it removes a
significant potential source of slowness.
Fixes#58
If you need the computational behaviour, you can use a local function
definition instead.
Fixes#42. If we don't do this, the name is treated in the saem way as
an unbound implicit, which is not what we want, so update with the
method applied to the parameters.
We were only doing implicits, so add auto implicits too. It's slightly
tricky, because we might also have implicits given of the form @{x}
which stands for the next auto implicit.
Fixes#50
Just like all other pi-bound things, if m is an unbound implicit and we
have m ?x = m y as a unification problem, we can conclude ?x = y because
it has to be true for all ms.
This was implemented in Blodwen but I hadn't got around to it yet for
Idris2... fortunately it's a bit easier in Idris2!
Fixes#44
We were only checking parameters, meaning that there were potential
clashes leading to confusing behaviour, and meaning that it was somehow
relevant what the names were in the interface!
Now by marking a method as multiplicity 0, we can explicitly say that
it's compile time only, so we can use it to compute types based on other
erased things - see tests/idris2/interface008 for a small example.
This fixes#8 - at least in that it allows the interface to be expressed
properly now, although the multiplicity annotations mean that
unfortunately it can't be compatible with Idris 1.
A local variable can't be applied to itself when searching (otherwise,
for example, we could end up trying something like id id id id id id etc
forever). So remove it from the environment before searching for its
arguments.
This and the previous patch fix#24. (Or, at least, the minimised cases
reported as part of it!)
We can't begin a search until we know what we're searching for! For some
reason I forgot to add this case, and without it the search space can
explode, or we might find an answer too soon and commit to the wrong
thing!
Fixes#36
This means that even if the relevant parameters aren't used by a method
body, the method can still see what the implicits are (though they will
be 0 multiplicity).
This is relevant to #8, but doesn't really fix it because we still need
a way of saying that methods are 0 multiplicity.
This is part of what we used to have in Enum but I think it's better to
separate the two. Added implementations for Nat, and anything in
Integral/Ord/Neg, so that we get range syntax (at least when its
implemeted) for the most useful cases.
This required a small change to auto implicit search (and I'm still not
sure about this). Now search arguments right to left, because solving
later arguments may resolve earlier arguments by unification and this
can happen in particular when chasing parent interfaces (which may have
fewer parameters).
Now supports with applications on the RHS when auto implicits are
involved. Auto implicit bound names in patterns now become searches on
the rhs in a with-application (I should write this construct up properly
in a paper some time!)
Elaborate via either === (homogeneous equality) or ~=~ (heterogeneous
equality) both of which are synonyms for Equal. This is to get the Idris
1 behaviour that equality is homogeneous by default to reduce the need
for type annotations, but heterogeneous if that doesn't work.
This was left over from Blodwen (where it was also wrong :)) but the way
we apply metavariables now means we don't need to do anything fancy when
unelaborating them for pretty printing.
This has shown up a problem with 'case' which is hard to fix - since it
works by generating a function with the appropriate type, it's hard to
ensure that let bindings computational behaviour is propagated while
maintaining appropriate dependencies between arguments and keeping the
let so that it only evaluates once. So, I've disabled the computational
behaviour of 'let' inside case blocks. I hope this isn't a big
inconvenience (there are workarounds if it's ever needed, anyway).
Need to add by full name, due to ordering of loading (the name it's
attached to may not be resolved yet!). This doesn't seem to cause any
performance problems but we can revisit if it does.
Don't use the type of a scrutinee to restrict possible patterns, because
it might have been refined by a Rig0 argument that has a missing case.
Instead, generate all the possible cases and check that the generated
ones are impossible (there's no obvious change in performance)
Small change needed to fix one - assume given implicits which are of the
form x@_ arise from types. It's a bit of a hack but I don't think
there's any need for anything more complicated.
Only valid if unifying the pattern at the end doesn't solve any
metavariables. Also when elaborating applications of fromInteger etc to
constants on the LHS we need to be in expression mode, then reduce the
result later.
This was a slight difference from Blodwen that wasn't accounted for -
there might be lets in the nested environment, so when building the
expanded application type, make sure we go under them
