Idris2/tests/idris2/with003/expected
Guillaume ALLAIS 7ccc47712e [ re #1087 ] Better error messages in the REPL
(as well as in type signatures now that I know how to do that)
2021-02-19 12:34:19 +00:00

72 lines
2.6 KiB
Plaintext

1/1: Building Main (Main.idr)
Main> Error: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:66--1:81
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
^^^^^^^^^^^^^^^
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:38--1:64
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
^^^^^^^^^^^^^^^^^^^^^^^^^^
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:38--1:64
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
^^^^^^^^^^^^^^^^^^^^^^^^^^
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:66--1:81
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
^^^^^^^^^^^^^^^
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:38--1:64
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
^^^^^^^^^^^^^^^^^^^^^^^^^^
Main> Error: Can't find an implementation for Num ().
(interactive):1:61--1:65
1 | with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
^^^^
Main> Error: Ambiguous elaboration. Possible results:
Prelude.Nil
Data.Vect.Nil
(interactive):1:4--1:6
1 | :t []
^^
Main> [] : Vect 0 ?elem
Main> [] : List ?a
Main> Error: When unifying Vect 0 ?elem and List ?a.
Mismatch between: Vect 0 ?elem and List ?a.
(interactive):1:34--1:41
1 | :t with [Vect.Nil, Prelude.(::)] [1,2,3]
^^^^^^^
Main> the (Maybe Integer) (pure 4) : Maybe Integer
Main> Expected 'case', 'if', 'do', application or operator expression.
(interactive):1:4--1:5
1 | :t with [] 4
^
Main> Bye for now!