Make desugaring/elaboration of interfaces, interface implementations,
records, and parameter blocks take into account the pragma
`%unbound_implicits off`.
Main changes:
(a) Execute the pragma also during desugaring
(b) Check whether `isUnboundImplicits` is on at each desugaring step
Alternatives I didn't take:
(1) Changing `findBindableNames` to effectfully check the flag.
Rationale:
Apart from turning a pure function into an effectful one, this
would mean repeatedly calling `findBindableNames`, only to do
nothing once the flag is read.
(2) Adding another function that takes multiple places (list of terms)
that might contain bindable names, and before dispatching
`findBindableNames` on each term, checking the flag.
Rationale: I didn't want to add another abstraction. (weak
rationale)
@edwinb @gallais : if you prefer (2), I can do that.
My first attempt at refolding natural constants led to all names
being printed with their namespace prefixes. This fixes that,
most notably by introducing the massive `mapPTermM` function in
`Idris.Syntax`.
Simply removing rewrites took me down from a user time of ~1m8s
to ~54s when running `make test`. The (small) code duplication
in `scan` is a bit annoying.
We could have a core unindexed data structure and then only export
pseudo-constructors with the right phantom arguments. Not sure it
is worth it yet though.
A more principled solution would of course be to make sure the backend
gets rid of the code corresponding to rewrites altogether!
We should be able to comment out any part of a program that parses
and still get a program that parses. This means we need to properly
ignore `{-` and `-}` when hidden behind a `--` comment or inside of
a string literal.
This is a temporary hack (no, honestly...) until we get some syntax for
prioritising specific names like the 'with' disambiguation in Idris 1.
There are better ways to achieve this, but this will make the REPL
easier to play with for new users.
Executables now get built and deleted. Install doesn't do anything with
the executable, and --clean only deletes the executable itself (not any
support files or libraries that might also have been generated in the
exec directory)
The names weren't fully explicit in the elaborator, so ambiguity
resolution wasn't able to take advantage of type-directed pruning. Now
they're explicit (but hard-coded, which we should fix later...) so they
can be resolved more easily.
This means we delay ambiguity resolution properly if we hit a depth
error, which means that we can come back to it later and hopefully be
able to resolve it by type on a second attempt.
This is the most likely cause of type checking being too slow, at least
in cases where there's not too much type level computation, so rather
than explore for ages, give up after going under too many ambiguous
names during elaboration.
The depth limit is configurable, with %ambiguity_depth <level>, but it's
very unlikely you'll ever want to do that rather than disambiguating
explicitly.
Do two passes through delayed elaborators (it's impossible to predict
dependency order). Possibly this should keep going as long as it's
making progress? I'll consider that later.
This is a tweak we used in Idris 1: In the end, if there is ambiguity,
and some names generate unification constraints but exactly one doesn't,
take the one that doesn't.
