smpoulsen / terp Goto Github PK

There's something wrong with type inference (unification specifically) when inferring the type of a length function defined in terms of foldl (or foldr):

(letrec foldl
  (lambda (fn accumulator values)
    (if (empty? values)
        accumulator
        (foldl fn (fn accumulator (car values)) (cdr values)))))

(let length
    (lambda (ns)
      (foldl
       (lambda (acc n) (+ 1 acc))
       0
       ns)))

In the repl, length type-checks as:

terp> :t length
terp> length : (-> [Int] [Int])

Spent a little time investigating and my hunch is that it's because the accumulator for the fold in length is an int, so for some reason it's getting substituted back into the type variable for ns.

Not worth getting held up on now I don't think (other functions defined in terms of folds type-check fine; as verified by importing prelude/list.tp and checking the defined functions).