From c861845757ec05763d6b0aa3a72df9457c8532e6 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 7 Sep 2021 00:41:08 +0100 Subject: [PATCH] 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. --- src/TTImp/Elab/Check.idr | 12 +++++++ tests/Main.idr | 1 + tests/idris2/error021/DeepAmbig.idr | 50 +++++++++++++++++++++++++++++ tests/idris2/error021/expected | 11 +++++++ tests/idris2/error021/run | 4 +++ 5 files changed, 78 insertions(+) create mode 100644 tests/idris2/error021/DeepAmbig.idr create mode 100644 tests/idris2/error021/expected create mode 100644 tests/idris2/error021/run diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 59462b082..281061fd1 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -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 : _} -> diff --git a/tests/Main.idr b/tests/Main.idr index 39080c93c..fad17580c 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -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", diff --git a/tests/idris2/error021/DeepAmbig.idr b/tests/idris2/error021/DeepAmbig.idr new file mode 100644 index 000000000..40822c100 --- /dev/null +++ b/tests/idris2/error021/DeepAmbig.idr @@ -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 diff --git a/tests/idris2/error021/expected b/tests/idris2/error021/expected new file mode 100644 index 000000000..3a22c6325 --- /dev/null +++ b/tests/idris2/error021/expected @@ -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 + ^^ + diff --git a/tests/idris2/error021/run b/tests/idris2/error021/run new file mode 100644 index 000000000..bed0bf023 --- /dev/null +++ b/tests/idris2/error021/run @@ -0,0 +1,4 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner -Werror --check DeepAmbig.idr +