Error messages

• Pretty bad error messages. Let’s try to list some:
• This happened when I tried to import Data.Nat which does not exist. However, it doesn’t say in which file!

$ make idris –build calc.ipkg Entering directory `./src’ Can’t find import Data/Nat make: * [build] Error 1

• Could do ‘implementation Layout String’ in calc.idr because it was defined in Lightyear.Strings (but I wasn’t importing that and Idris was asking for an implementation).

• Cannot say “export public”, only “public export”. Error message is:

➯ make check doc idris –checkpkg babyml.ipkg Entering directory `./src’ ./Syntax.idr:16:1: error: expected: “)”, “->”, “;”, “in”, ambiguous use of a left-associative operator, ambiguous use of a non-associative operator, ambiguous use of a right-associative operator, declaration, end of input, matching application expression export public ^ Type checking ./Syntax.idr make: * [check] Error 1

• Weird error was due to not having a Show instance on one of my datatypes.

➯ make idris –build babyml.ipkg Entering directory `./src’ Type checking ./TypeCheck.idr TypeCheck.idr:17:9: When checking right hand side of TypeCheck.check with expected type Either TypeError Ty

When checking an application of function TypeCheck.typeError: Can’t disambiguate since no name has a suitable type: Prelude.List.++, Prelude.Strings.++ make: * [build] Error 1

Other

• Expected to have an (>>) operator. Wasn’t there…