Idris function getting a type mismatch error

Question

I'm new to Idris. I'm working on the following function

average :  String -> Double
average str 
    = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords

where
    wordCount : String -> Nat
    wordCount str = length (words str)

    allLengths : List String -> List Nat
    allLengths strs = map length strs

I keep getting the following error

Type checking ./average.idr
average.idr:5:47:
  |
5 |                   totalLength = sum (allLengths (words str)) in
  |                                   ^
When checking right hand side of average with expected type
        Double

When checking argument x to type constructor =:
        Type mismatch between
                Nat (Type of Main.average, wordCount str _)
        and
                _ -> _ (Is Main.average, wordCount str _ applied to too many arguments?)

Holes: Main.average

I know as much that I have declared average to return a Double but the declaration I have written for average doesn't return a double. This is where I'm stumped. I expected the cast to do the job.

Answer 1

Your indentation's off. In the docs, they say

When writing Idris programs both the order in which definitions are given and indentation are significant ... New declarations must begin at the same level of indentation as the preceding declaration. Alternatively, a semicolon ; can be used to terminate declarations.

Try this ...

average :  String -> Double
average str 
    = let numWords = wordCount str
          totalLength = sum (allLengths (words str)) in
          cast totalLength / cast numWords

I guess in yours it's parsing everything in average after wordCount str as arguments to wordCount str which leads to a type error cos Nat doesn't take arguments