type checker doesn't catch type error

[shriram]

The definition of lz-map below has an intentional error: I wanted to see what would happen if I failed to thunk the rest argument to lz-link. There's no error at all. However, once I add the check block afterwards, I get an error in the first test (take(5, twos)). If I add a thunk to the penultimate line of lz-map it type-checks and runs correctly (but, boy, is it slow as molasses).

data Stream<T>:
  | lz-link(h :: T, t :: ( -> Stream<T>))
end

fun lz-first<T>(s :: Stream<T>):
  cases (Stream) s:
    | lz-link(h, t) => h
  end
end

fun lz-rest<T>(s :: Stream<T>):
  cases (Stream) s:
    | lz-link(h, t) => t()
  end
end

rec ones = lz-link(1, {(): ones})

fun nats-from(n :: Number):
  lz-link(n, {(): nats-from(n + 1)})
end
nats = nats-from(0)

fun take<T>(n :: Number, s :: Stream<T>):
  ask:
    | n == 0 then: empty
    | n > 0  then:
      link(lz-first(s), take(n - 1, lz-rest(s)))
  end
end

check:
  take(5, ones) is [list: 1, 1, 1, 1, 1]
  take(5, nats) is [list: 0, 1, 2, 3, 4]
end

fun lz-map<A, B>(f :: (A -> B), s :: Stream<A>):
  lz-link(
    f(lz-first(s)),
    lz-map(f, lz-rest(s)))
end

check:
  twos = lz-map({(n): n + 1}, ones)
  nat-1 = lz-map({(n): n + 1}, nats)
  take(5, twos) is [list: 2, 2, 2, 2, 2]
  take(5, nat-1) is [list: 1, 2, 3, 4, 5]
end

[blerner]

1. Even if we comment out the check block, the rest of this program does produce a type error, complaining that lz-map call on line 40 should have a thunk type but doesn't. So the type checker is correct here regardless of the check block

2. The display of unbound type variables is ugly (<?-1>, <?-2> etc). Matthew and I agree we should present these as names, eg as spreadsheet-column names A,...Z,AA...AZ,BA...BZ etc, while avoiding any names already seen. So the message here would look like, "The type constraint ( -> Stream<A>) was incompatible with the type constraint Stream<A>, for some unknown type A", assuming that nothing in the current type inference problem used the name A already.