mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
Abandon ambiguity resolution on undefined name (#1907)
* Abandon ambiguity resolution on undefined name This has finally annoyed me enough to do something about it. If we get a "no such variable" error there's no point exploring other branches. * Removes spaces from test file One day I'll update the linter to ignore test files. We should really accept literally anything as a possiblity for test files, even if removing the spaces is tidier. * Reset context before throwing in 'successful' Although I don't think this is strictly necessary for a fatal error, we should still for the sake of tidiness reset the state when backtracking.
This commit is contained in:
parent
9865765d1d
commit
c861845757
@ -580,8 +580,20 @@ successful allowCons ((tm, elab) :: elabs)
|
||||
put EST est
|
||||
put MD md
|
||||
put Ctxt defs
|
||||
when (abandon err) $ throw err
|
||||
elabs' <- successful allowCons elabs
|
||||
pure (Left (tm, err) :: elabs'))
|
||||
where
|
||||
-- Some errors, it's not worth trying all the possibilities because
|
||||
-- something serious has gone wrong, so just give up immediately.
|
||||
abandon : Error -> Bool
|
||||
abandon (UndefinedName _ _) = True
|
||||
abandon (InType _ _ err) = abandon err
|
||||
abandon (InCon _ _ err) = abandon err
|
||||
abandon (InLHS _ _ err) = abandon err
|
||||
abandon (InRHS _ _ err) = abandon err
|
||||
abandon (AllFailed errs) = any (abandon . snd) errs
|
||||
abandon _ = False
|
||||
|
||||
export
|
||||
exactlyOne' : {vars : _} ->
|
||||
|
@ -69,6 +69,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
|
||||
"error006", "error007", "error008", "error009", "error010",
|
||||
"error011", "error012", "error013", "error014", "error015",
|
||||
"error016", "error017", "error018", "error019", "error020",
|
||||
"error021",
|
||||
-- Parse errors
|
||||
"perror001", "perror002", "perror003", "perror004", "perror005",
|
||||
"perror006", "perror007", "perror008", "perror009", "perror010",
|
||||
|
50
tests/idris2/error021/DeepAmbig.idr
Normal file
50
tests/idris2/error021/DeepAmbig.idr
Normal file
@ -0,0 +1,50 @@
|
||||
|
||||
namespace A
|
||||
export
|
||||
x : Bool -> Bool
|
||||
x = not
|
||||
|
||||
namespace B
|
||||
export
|
||||
x : Nat -> Bool
|
||||
x Z = True
|
||||
x _ = False
|
||||
|
||||
%ambiguity_depth 1000
|
||||
|
||||
-- There's an undefined name very deep here - if we don't take a shortcut,
|
||||
-- this shows all the ambiguous branches with the undefined named!
|
||||
test : Nat -> Bool
|
||||
test val
|
||||
= x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ va
|
11
tests/idris2/error021/expected
Normal file
11
tests/idris2/error021/expected
Normal file
@ -0,0 +1,11 @@
|
||||
1/1: Building DeepAmbig (DeepAmbig.idr)
|
||||
Error: While processing right hand side of test. Undefined name va.
|
||||
|
||||
DeepAmbig:50:59--50:61
|
||||
46 | x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
47 | x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
48 | x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
49 | x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $
|
||||
50 | x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ x $ va
|
||||
^^
|
||||
|
4
tests/idris2/error021/run
Normal file
4
tests/idris2/error021/run
Normal file
@ -0,0 +1,4 @@
|
||||
rm -rf build
|
||||
|
||||
$1 --no-color --console-width 0 --no-banner -Werror --check DeepAmbig.idr
|
||||
|
Loading…
Reference in New Issue
Block a user