type checker internal error

[shriram]

I can't see quite what's wrong with this program, and even if it's type-buggy there should be a proper error, not an internal error. I have a student stuck on a homework because of it…

import lists as L

fun consolidate<A, B>(huge :: List<A>, build :: List<A>)  -> List<B>: 
  cases (List<A>) huge: 
    | empty => build
    | link(f,r) => 
      consolidate(r, L.foldr(lam(acc, elt): link(elt, acc) end, build, f))
  end 
end 

produces

[blerner]

Could you reformat your code above? Looks like one of the branches is blank?

[shriram]

Oops, sorry. Done.

[blerner]

Ok, now I can reproduce the bug...but I can't explain it, or quite figure out what the program was supposed to be doing, anyway. It certainly does seem like none of the inputs have type B anywhere, so I don't see how you could produce a List<B> as your output. But even if I change everything to List<A> everywhere, I still get a type-inconsistency (not a crashy error, but a real type error message) that I don't immediately recognize why it's happening.

[sorawee]

A smaller program that produces the error:

fun f<A>(xs :: List<A>, x :: A)  -> Any: 
  fold(lam(acc, e): link(e, acc) end, xs, x)
end

The last argument of fold should be a list. By changing x to xs, it now type checks.

[sorawee]

This is fun.

fun f<A>(xs :: List<A>, x :: A)  -> Any: 
  fold(lam(_, e): link(e, empty) + empty end, xs, x)
end

produces an error, but

fun f<A>(xs :: List<A>, x :: A)  -> Any: 
  fold(lam(_, e): link(e, empty) end, xs, x)
end

does not.