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

added constraint generator implementation match expressions type inference labels

Here is a more minimal reproducer:

until p f x = if p x then x else until p f (f x)

until-infer: FAIL (0.01s)
  Test output was different from './test/cases/should-typecheck/until-infer.output'. It was:
  until : forall {a1:Type}. forall {b1:Type}. (a1 -> Bool) -> (a1 -> b1) -> a1 -> a1

Even more minimal:

fix fun = fun (fix fun)

The (incorrect) inferred type: fix : forall {a1:Type}. forall {b1:Type}. (b1 -> a1) -> a1

The correct type: fix : forall {a1:Type}. (a1 -> a1) -> a1

mentioned in commit e241f41c

Fixed in e241f41c

closed