Add error message tests

src/Core/AutoSearch.idr

@@ -68,9 +68,9 @@ searchIfHole fc defaults trying ispair (S depth) def top env arg
               | Nothing => throw (CantSolveGoal fc [] top)
          let Hole _ inv = definition gdef
               | _ => pure () -- already solved
-         let top' = if ispair 
-                       then type gdef
-                       else top
+         top' <- if ispair 
+                    then normaliseScope defs [] (type gdef)
+                    else pure top
 
          argdef <- searchType fc rig defaults trying depth def top' env 
                               !(normaliseScope defs env (argType arg))

src/Idris/Error.idr

@@ -115,7 +115,7 @@ perror (AllFailed ts)
   where
     pAlterror : (Maybe Name, Error) -> Core String
     pAlterror (Just n, err)
-       = pure $ "If " ++ show n ++ ": " ++ !(perror err) ++ "\n"
+       = pure $ "If " ++ show !(getFullName n) ++ ": " ++ !(perror err) ++ "\n"
     pAlterror (Nothing, err)
        = pure $ "Possible error:\n\t" ++ !(perror err)
 

src/TTImp/ProcessDef.idr

@@ -320,7 +320,8 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
                             Rig0 => InType
                             _ => InExpr
          log 5 $ "Checking RHS " ++ show rhs
-         rhstm <- checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
+         rhstm <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+                       checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
          clearHoleLHS
 
          logTerm 5 "RHS term" rhstm

tests/Main.idr

@@ -25,6 +25,8 @@ idrisTests : List String
 idrisTests
     = ["basic001",
        "coverage001", "coverage002",
+       "error001", "error002", "error003", "error004", "error005",
+       "error006",
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",

tests/idris2/error001/Error.idr

@@ -0,0 +1,6 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+wrong : a -> Vect (S n) a -> Vect (S n) a
+wrong x xs = x :: x 

tests/idris2/error001/expected

@@ -0,0 +1,7 @@
+1/1: Building Error (Error.idr)
+Error.idr:6:19--7:1:While processing right hand side of Main.wrong at Error.idr:6:1--7:1:
+When unifying a and Vect ?k a
+Mismatch between:
+	a
+and
+	Vect ?k ?a

tests/idris2/error001/run

@@ -0,0 +1,3 @@
+$1 --check Error.idr
+
+rm -rf build

tests/idris2/error002/Error.idr

@@ -0,0 +1,6 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+wrong : a -> Vect (S n) a -> Vect (S n) a
+wrong xs = x :: xs

tests/idris2/error002/expected

@@ -0,0 +1,3 @@
+1/1: Building Error (Error.idr)
+Error.idr:6:12--6:14:While processing right hand side of Main.wrong at Error.idr:6:1--7:1:
+Undefined name x

tests/idris2/error002/run

@@ -0,0 +1,3 @@
+$1 --check Error.idr
+
+rm -rf build

tests/idris2/error003/Error.idr

@@ -0,0 +1,12 @@
+import Data.List
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+length : Vect n a -> Nat
+length [] = Z
+length (x :: xs) = S (length xs)
+
+wrong : Nat -> Nat
+wrong x = length x

tests/idris2/error003/expected

@@ -0,0 +1,21 @@
+1/1: Building Error (Error.idr)
+Error.idr:12:18--13:1:While processing right hand side of Main.wrong at Error.idr:12:1--13:1:
+Sorry, I can't find any elaboration which works. All errors:
+If Main.length: When unifying Nat and Vect ?n ?a
+Mismatch between:
+	Nat
+and
+	Vect ?n ?a
+
+If Data.List.length: When unifying Nat and List ?a
+Mismatch between:
+	Nat
+and
+	List ?a
+
+If Prelude.length: When unifying Nat and String
+Mismatch between:
+	Nat
+and
+	String
+

tests/idris2/error003/run

@@ -0,0 +1,3 @@
+$1 --check Error.idr
+
+rm -rf build

tests/idris2/error004/Error1.idr

@@ -0,0 +1,8 @@
+import Data.List
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+wrong : String
+wrong = show (the (Vect _ _) [1,2,3,4])

tests/idris2/error004/Error2.idr

@@ -0,0 +1,16 @@
+import Data.List
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+Show a => Show (Vect n a) where
+  show [] = "END"
+  show (x :: xs) = show x ++ ", " ++ show xs
+
+Show (Vect n Integer) where
+  show [] = "END"
+  show (x :: xs) = show x ++ ", " ++ show xs
+
+wrong : String
+wrong = show (the (Vect _ _) [1])

tests/idris2/error004/expected

@@ -0,0 +1,12 @@
+1/1: Building Error1 (Error1.idr)
+Error1.idr:8:9--9:1:While processing right hand side of Main.wrong at Error1.idr:8:1--9:1:
+Can't find an implementation for Show (Vect (S (S (S (S Z)))) Integer)
+1/1: Building Error2 (Error2.idr)
+Error2.idr:11:1--15:1:While processing right hand side of Main.showPrec at Error2.idr:11:1--15:1:
+Multiple solutions found in search. Possible correct results:
+	Show implementation at Error2.idr:11:1--15:1
+	Show implementation at Error2.idr:7:1--11:1
+Error2.idr:16:9--17:1:While processing right hand side of Main.wrong at Error2.idr:16:1--17:1:
+Multiple solutions found in search. Possible correct results:
+	Show implementation at Error2.idr:11:1--15:1
+	Show implementation at Error2.idr:7:1--11:1

tests/idris2/error004/run

@@ -0,0 +1,4 @@
+$1 --check Error1.idr
+$1 --check Error2.idr
+
+rm -rf build

tests/idris2/error005/IfErr.idr

@@ -0,0 +1,7 @@
+data Wibble = Wobble
+
+foo : a -> a -> Bool
+foo x y = x == y
+
+bar : Wibble -> Wibble -> Bool
+bar x y = x == y

tests/idris2/error005/expected

@@ -0,0 +1,5 @@
+1/1: Building IfErr (IfErr.idr)
+IfErr.idr:4:11--6:1:While processing right hand side of Main.foo at IfErr.idr:4:1--6:1:
+Can't find an implementation for Eq a
+IfErr.idr:7:11--8:1:While processing right hand side of Main.bar at IfErr.idr:7:1--8:1:
+Can't find an implementation for Eq Wibble

tests/idris2/error005/run

@@ -0,0 +1,3 @@
+$1 --check IfErr.idr
+
+rm -rf build

tests/idris2/error006/IfErr.idr

@@ -0,0 +1,24 @@
+showIfEq : (Eq a, Show a) => a -> a -> String
+showIfEq x y = if x == y then show x else "Nope"
+
+topeq : Eq a => a -> a -> Bool
+topeq x y = x == y
+
+data Foo = MkFoo | MkBar
+
+-- Should only show the first interface search failure in the tuple
+-- (Ideally it would keep going and find all the failures, but that is
+-- hard to achieve and this way is better than displaying the whole
+-- top level search when only part of it is relevant)
+
+test : Int -> String
+test x = showIfEq MkFoo MkBar
+
+Eq Foo where
+  MkFoo == MkFoo = True
+  MkBar == MkBar = True
+  _ == _ = False
+
+test2 : String
+test2 = showIfEq MkFoo MkBar
+

tests/idris2/error006/expected

@@ -0,0 +1,5 @@
+1/1: Building IfErr (IfErr.idr)
+IfErr.idr:15:10--17:1:While processing right hand side of Main.test at IfErr.idr:15:1--17:1:
+Can't find an implementation for Eq Foo
+IfErr.idr:23:9--25:1:While processing right hand side of Main.test2 at IfErr.idr:23:1--25:1:
+Can't find an implementation for Show Foo

tests/idris2/error006/run

@@ -0,0 +1,3 @@
+$1 --check IfErr.idr
+
+rm -rf build

tests/ttimp/eta002/expected

@@ -1,4 +1,5 @@
 Processing as TTImp
+Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
 Eta.yaff:16:10--17:1:When unifying: ($resolved76 ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) ?Main.{x:16}_[] ?Main.{x:16}_[]) and ($resolved76 ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) (({arg:8} : Integer) -> (({arg:9} : Integer) -> $resolved84)) $resolved85 \x : Char => \y : ?Main.{_:12}_[x[0]] => ($resolved85 ?Main.{_:13}_[x[1], y[0]] ?Main.{_:14}_[x[1], y[0]]))
 	Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
 Yaffle> Bye for now!

tests/ttimp/qtt001/expected

@@ -1,4 +1,5 @@
 Processing as TTImp
+QTT.yaff:14:1--16:1:When elaborating right hand side of Main.dupbad:
 QTT.yaff:14:13--16:1:There are 2 uses of linear name x
 Yaffle> Main.foo : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just x a a))
 Yaffle> Main.bar : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just x a a))