We already did this, but missed a few cases due to the way arguments are
elaborated. So now, when checking an LHS, we don't allow LHS argument
types to be inferred from the pattern, but rather they must be inferred
from elsewhere. To do this, we keep track of the constraints which would
be solved when inferring the type, and make sure they don't solve any
new metavariables. Fixes#1510, and also now gets the error location
right as a bonus!
Because it relies on the source file that I've just fixed for the
linter. I think I've now spent more time pleasing the linter than fixing
the actual bug...
We need to fully evaluate, not just the public export names, otherwise
we don't pattern match properly and potentially generate catch all
patterns we don't mean.
Fixes#1537
This is an approximate check of arguments - if we can find an argument
that differs at the head, there's no point in checking further. This can
be a significant shortcut when conversion checking two large terms that
only differ very slightly, as it saves checking big arguments
unnecessarily.
Why:
* To implement robust cross-project go-to-definition in LSP
i.e you can jump to definition of any global name coming
from library dependencies, as well as from the local project files.
What it does:
* Modify `FC`s to carry `ModuleIdent` for .idr sources,
file name for .ipkg sources or nothing for interactive runs.
* Add `--install-with-src` to install the source code alongside
the ttc binaries. The source is installed into the same directory
as the corresponding ttc file. Installed sources are made read-only.
* As we install the sources pinned to the related ttc files we gain
the versioning of sources for free.
Need to use the 8 byte version of Ints for the shortcut version of
reading TTCs too, otherwise we'll read the wrong hash and build things
unnecessarily.
The cast to float needs to happen before the division, otherwise integer
division will be performed, and as a result `CLOCKS_PER_NSEC` will
always be 0 if `CLOCKS_PER_SEC` < `NSEC_PER_SEC`.
* Add utility functions to treat All as a heterogeneous container
* Distinguish RefC Int and Bits types
* Change RefC Integers to be arbitrary precision
* Add RefC Bits maths operations
* Make RefC div and mod Euclidean
* Add RefC bit-ops tests
* Add RefC integer comparison tests
* Add RefC IntN support
For LSP these functionality is helpful. When we have a way to
request all the names we known about, we can use the information
for different purposes, such as, suggesting names to fill the
holes, or creating document symbols map for a module.
