This involves making 'unelab' aware of nested names so that it can
remove the parameters from names in the current block. It's a bit of a
hacky solution, but it is also the easiest one.
Ideally we'd build the getter types directly, rather than using unelab,
but that's one to save for another time.
Fixes#1482
Convert `App.Control.Exception` interface to an alias to `HasErr`.
Probably `Exception` interface need to be deprecated or removed.
Note similar problem exists with `PrimIO` calling `PrimIO, Exception`,
also need to be fixed.
Fix this scenario:
```
throwBoth : Has [Exception String, Exception Int] es => App es ()
throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
```
With this commit it works, before this commit it failed with:
```
Error: While processing right hand side of throwOne. Can't find an implementation for Exception Int (String :: es).
TestException.idr:8:48--8:57
|
8 | throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
| ^^^^^^^^^
```
Pragma once is supported by all compilers for the last ten years.
Better use it instead of include guards (which use different styles
in different files).
If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
This is set to 1 second by default. Usually if it hasn't found a result
by then, it never will, but given that we find the first batch of
results then sort them, the timeout also stops us fruitlessly searching
for more solutions.
Hopefully 1s is more than enough for CI too. There is a mechanism to
change the timeout (%search_timeout) so if it turns out that CI needs
longer in some cases, we can increase it there.
I haven't documented this yet, but proof/definition search needs
documenting in general. I'll get to that.
The timer mechanism may also be useful elsewhere - I'm considering it
for ambiguity warnings, because the ambiguity depth limit isn't working
very well for that.
The option is hidden being a flag (`-Xcheck-hashes`) so that by default `touch`ing
a file is enough to get it recompiled.
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
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
