Why doesn't this Idris snippet typecheck without an explicit type?

Question

I'm just getting started learning Idris, and I'm working through the book Type Driven Development with Idris. One of the example exercises from the second chapter is to write a function which, given a string, determines the average length of a word in that string. My solution was as follows:

average : String -> Double
average phrase =
  let werds = words phrase
      numWords = length werds
      numChars = the Nat (sum (map length werds)) in
  cast numChars / cast numWords

However, I had a lot of trouble arriving at this solution due to the numChars line. For some reason, this doesn't typecheck unless I make the type explicit using the Nat. The error states:

Can't disambiguate since no name has a suitable type:
        Prelude.List.length, Prelude.Strings.length

This doesn't make a whole lot of sense to me, since regardless of which definition of length is used, the return type is Nat. This is supported by the fact that this same sequence of operations can be done error-free in the REPL. What's the reason for this?

gallais gallais · Accepted Answer · 2017-07-14T11:54:18

This is indeed a weird one given that if you name the intermediate computation map length werds then Idris is able to infer the type:

average : String -> Double
average phrase =
  let werds    = words phrase
      numWords = length werds
      swerds   = map length werds
      numChars = sum swerds in
  cast numChars / cast numWords

And the REPL is also able to infer that sum . map length . words has type String -> Nat. If you don't get any satisfactory answer here, I suggest filing a bug report.

Why doesn't this Idris snippet typecheck without an explicit type?

2 Answers