Possible glitch in typing?

#1

A student wrote this code; the idea is to type createBoard(2, 3) to produce [[0, 0], [0, 0], [0, 0]]. (This is just a first draft to get the structure right!)

let createBoard: (int, int) => list(list(int)) =
  (width, height) => {
    let rec createList: (int, 'a) => list('a) =
      (length, content) =>
        switch (length) {
        | 0 => []
        | _ => [content, ...createList(length - 1, content)]
        };
    createList(width, createList(height, 0));
  };

In VSCode, this generates an error in the 2nd-to-last line, saying that createList(height, 0) is of type list(int), but int was expected. That seemed odd to me, and I dug in a little deeper. When I write

let createBoard: (int, int) => list(list(int)) =
  (width, height) => {
    let rec createList: (int, 'a) => list('a) =
      (length, content) =>
        switch (length) {
        | 0 => []
        | _ => [content, ...createList(length - 1, content)]
        };
    //let k = createList(height, 0);
    let t = createList;
    []
  };

everything compiles fine, and I get a warning about t being unused, but hovering over it tells me that it has type (int, 'a) => list('a), which is comforting.

But when I uncomment that previous line:

let createBoard: (int, int) => list(list(int)) =
  (width, height) => {
    let rec createList: (int, 'a) => list('a) =
      (length, content) =>
        switch (length) {
        | 0 => []
        | _ => [content, ...createList(length - 1, content)]
        };
    let k = createList(height, 0);
    let t = createList;
    []
  };

hovering over t shows it’s of type (int, int) => list(int).

I’m not sure how that can be the case — invoking a procedure should not change its type, if I understand correctly. I’ve written the corresponding code in ReScript, and the error persists.

Any insights?

#2

If you want createList to be polymorphic on its second argument, you need to add a forall. Here’s a version that works as you expect:

let createBoard: (int, int) => list(list(int)) =
  (width, height) => {
    let rec createList: 'a. (int, 'a) => list('a) =
      (length, content) =>
        switch (length) {
        | 0 => []
        | _ => [content, ...createList(length - 1, content)]
        };
    let k = createList(height, 0);
    let t = createList;
    [];
  };

For more information, the polymorphism chapter in the OCaml manual explains this in detail: https://v2.ocaml.org/manual/polymorphism.html

#3

Thanks. I went and read the cited chapter, and there was a lot of talk about mutable things (which doesn’t seem to apply) and records (which doesn’t seem to apply), and I still didn’t understand, although I did try out the solution and see that it works. What baffles me is why this version of the original code also works:

let rec createList: (int, 'a) => list('a) =
  (length, content) =>
    switch (length) {
    | 0 => []
    | length when length > 0 => [content, ...createList(length - 1, content)]
    | _ => failwith("nonpositive length")
    };
let createBoard: (int, int) => list(list(int)) =
  (width, height) => createList(width, createList(height, 0));
createBoard(3, 5);

The only distinction seems to be that createList is defined outside the context of createBoard, but nothing in the chapter tells me why this would change the type inferred for it. Can you explain this apparent contradiction?