Skip to content

The inferred type of foldr is wrong

Currently the typechecker infers the following incorrect type for foldr:

myFoldr : forall {a1:Type}. forall {b1:Type}. forall {c1:Type}. (a1 -> c1 -> b1) -> b1 -> List a1 -> b1

As expected, the problem is in the recursive equation. i.e

-- typechecker/test/cases/should-typecheck/foldr-recurse.hs
myFoldr function el (Cons xel xels) = function xel (myFoldr function el xels) 

Gets the type: myFoldr : forall {a1:Type}. forall {b1:Type}. forall {c1:Type}. forall {d1:Type}. (b1 -> d1 -> c1) -> a1 -> List b1 -> c1