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.

Author: edwinb

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 : _} ->

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",

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

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
+                                                                ^^
+

tests/idris2/error021/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner -Werror --check DeepAmbig.idr
+