Merge pull request #2744 from dunhamsteve/bang-fc

[ parser ] Better error messages for type mismatch on bang expressions

src/Idris/Desugar.idr

@@ -347,7 +347,7 @@ mutual
            put Bang ({ nextName $= (+1),
                        bangNames $= ((bn, fc, itm) ::)
                      } bs)
-           pure (IVar EmptyFC bn)
+           pure (IVar (virtualiseFC fc) bn)
   desugarB side ps (PIdiom fc ns term)
       = do itm <- desugarB side ps term
            logRaw "desugar.idiom" 10 "Desugaring idiom for" itm

tests/Main.idr

@@ -88,7 +88,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
        "error006", "error007", "error008", "error009", "error010",
        "error011", "error012", "error013", "error014", "error015",
        "error016", "error017", "error018", "error019", "error020",
-       "error021", "error022", "error023",
+       "error021", "error022", "error023", "error024",
        -- Parse errors
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006", "perror007", "perror008", "perror009", "perror010",

tests/idris2/error024/Error1.idr

@@ -0,0 +1,5 @@
+foo : Int -> IO Int
+foo x = pure x
+
+main : IO ()
+main = putStrLn !(foo 10)

tests/idris2/error024/expected

@@ -0,0 +1,15 @@
+1/1: Building Error1 (Error1.idr)
+Error: While processing right hand side of main. When unifying:
+    Int
+and:
+    String
+Mismatch between: Int and String.
+
+Error1:5:17--5:26
+ 1 | foo : Int -> IO Int
+ 2 | foo x = pure x
+ 3 | 
+ 4 | main : IO ()
+ 5 | main = putStrLn !(foo 10)
+                     ^^^^^^^^^
+

tests/idris2/error024/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check Error1.idr