Type error with type annotations containing quantifiers and the Unkown type

[br4sco]

The following program

include "string.mc"

recursive
let foldl2 : all a. all b. all c. Unknown =
  lam f. lam acc: a. lam seq1: [b]. lam seq2: [c].
    let g = lam acc : (a, [b]). lam x2.
      match acc with (acc, [x1] ++ xs1) then (f acc x1 x2, xs1)
      else error "foldl2: Cannot happen!"
    in
    if geqi (length seq1) (length seq2) then
      match foldl g (acc, seq1) seq2 with (acc, _) in acc
    else foldl2 (lam acc. lam x1. lam x2. f acc x2 x1) acc seq2 seq1
end

mexpr
print (int2string (foldl2 (lam acc. lam x1. lam x2. addi acc (addi x1 x2)) 0 [1, 2, 3] [3, 2, 1]))

gives the following type error

ERROR </home/oerikss/Documents/workspaces/miking/miking/tmp.mc 4:13-9:6>:
* Expected an expression of type: (a -> c -> b -> a) -> a -> [c] -> [b] -> a
*    Found an expression of type: (a -> b -> c -> a) -> a -> [b] -> [c] -> a
* (errors: types b != c)
* When type checking the expression
let foldl2 : all a. all b. all c. Unknown =
  lam f. lam acc: a. lam seq1: [b]. lam seq2: [c].
    let g = lam acc : (a, [b]). lam x2.
      match acc with (acc, [x1] ++ xs1) then (f acc x1 x2, xs1)
      else error "foldl2: Cannot happen!"
    in

Changing the annotation to

let foldl2 : all a. all b. all c. (a -> b -> c -> a) -> a -> [b] -> [c] -> a = ...

makes the program type check.

This issue is possibly the source of the problem discussed in #829, and it might be related to #793.