Implement uniformity check for type recursion

[paulyoung]

I'm getting the following error when trying to type check the file below. This is a more relatable and minimal example of an issue I ran into when trying to do something similar.

Tested against 003de63 (the latest on master at time of writing)

(unknown location): internal error, Stack overflow

Last environment:
Raised by primitive operation at file "typing.ml", line 297, characters 10-28

Called from file "typing.ml" (inlined), line 285, characters 13-36

Called from file "typing.ml", line 625, characters 13-30

Called from file "typing.ml", line 587, characters 2-23

Called from file "typing.ml", line 1030, characters 7-26

Called from file "typing.ml", line 1009, characters 2-56

Called from file "typing.ml", line 614, characters 11-42

Called from file "typing.ml", line 587, characters 2-23

Called from file "typing.ml", line 981, characters 6-45

Called from file "typing.ml", line 951, characters 10-59

Called from file "typing.ml", line 553, characters 24-52

Called from file "typing.ml", line 297, characters 10-28

Called from file "typing.ml" (inlined), line 285, characters 13-36

Called from file "typing.ml", line 625, characters 13-30

Called from file "typing.ml", line 587, characters 2-23

Called from file "typing.ml", line 905, characters 8-57

Called from file "list.ml", line 111, characters 24-34

Called from file "typing.ml", line 882, characters 4-72

Called from file "typing.ml", line 863, characters 9-61

Called from file "typing.ml", line 607, characters 11-49

Called from file "typing.ml", line 587, characters 2-23

Called from file "typing.ml", line 1030, characters 7-26

Called from file "typing.ml", line 1009, characters 2-56

Called from file "typing.ml", line 614, characters 11-42

Called from file "typing.ml", line 587, characters 2-23

Called from file "typing.ml", line 981, characters 6-45

Called from file "typing.ml", line 951, characters 10-59

Called from file "typing.ml", line 553, characters 24-52

Called from file "typing.ml", line 297, characters 10-28

Called from file "typing.ml" (inlined), line 285, characters 13-36

Called from file "typing.ml", line 625, characters 13-30

Called from file "typing.ml", line 587, characters 2-23

Called from file "typing.ml", line 905, characters 8-57

Called from file "list.ml", line 111, characters 24-34

Called from file "typing.ml", line 882, characters 4-72

Called from file "typing.ml", line 834, characters 11-63

Called from file "typing.ml", line 370, characters 8-41

Called from file "typing.ml", line 297, characters 10-28

Called from file "typing.ml" (inlined), line 285, characters 13-36

Called from file "typing.ml", line 970, characters 31-50

Called from file "typing.ml", line 1056, characters 16-42

Called from file "typing.ml", line 22, characters 6-9

Called from file "typing.ml" (inlined), line 28, characters 6-27

Called from file "typing.ml", line 1022, characters 16-59

Called from file "typing.ml", line 22, characters 6-9

Called from file "typing.ml" (inlined), line 28, characters 6-27

Called from file "typing.ml", line 1023, characters 16-66

Called from file "typing.ml", line 22, characters 6-9

Called from file "typing.ml" (inlined), line 28, characters 6-27

Called from file "typing.ml", line 1023, characters 16-66

Called from file "typing.ml", line 1009, characters 2-56

Called from file "typing.ml" (inlined), line 1227, characters 2-40

Called from file "pipeline.ml", line 154, characters 43-70

Called from file "pipeline.ml", line 116, characters 37-52

Called from file "pipeline.ml", line 149, characters 10-41

Called from file "pipeline.ml", line 186, characters 8-23

Called from file "pipeline.ml", line 251, characters 15-33

Called from file "main.ml", line 69, characters 35-62

Called from file "main.ml", line 98, characters 4-23

type Array<A> = {
  value : A[];

  /* (unknown location): internal error, Stack overflow */
  /* bind : <B> (A -> Array<B>) -> Array<B>; */
};

let Array = new Self {
  init = func <A>(value_ : A[]) : Array<A> {
    new self {
      value = value_;

      bind = func <B>(f : A -> Array<B>) : Array<B> {
        Self.bind<A, B>(self, f);
      };
    };
  };

  bind = func <A, B>(xs : Array<A>, f : A -> Array<B>) : Array<B> {
    var ys : B[] = [];
    for (i in xs.value.keys()) {
      ys := arrayConcat<B>(ys, f(xs.value[i]).value);
    };
    Array.init<B>(ys);
  };
};

func arrayConcat<A>(xs : A[], ys : A[]) : A[] {
  switch(xs.len(), ys.len()) {
    case (0, 0) { []; };
    case (0, _) { ys; };
    case (_, 0) { xs; };
    case (xsLen, ysLen) {
      Array_tabulate<A>(xsLen + ysLen, func (i : Nat) : A {
        if (i < xsLen) {
          xs[i];
        } else {
          ys[i - xsLen];
        };
      });
    };
  };
};


/* Contrived bind usage */

/* Static class member bind works as expected */
let xs1 = Array.init<Nat>([ 1, 2, 3, 4 ]);
let ys1 = Array.bind<Nat, Nat>(xs1, func (x : Nat) : Array<Nat> {
  Array.init<Nat>([x * x]);
});

for (y in ys1.value.vals()) {
  printInt(y);
};

/* Instance member bind can't be called because it can't be added to the type
 * without causing a stack overflow.
 */
/* type error, field name bind does not exist in type */
/*
let xs2 = Array.init<Nat>([ 1, 2, 3, 4 ]);
let ys2 = xs2.bind<Nat>(func (x : Nat) : Array<Nat> {
  Array.init<Nat>([x * x]);
});

for (y in ys2.value.vals()) {
  printInt(y);
};
*/

The type alone is fine:

type Array<A> = {
  value : A[];
  bind : <B> (A -> Array<B>) -> Array<B>;
};

In case it's somehow relevant, using a class is fine and behaves as expected:

class Array<A>(value_ : A[]) {
  value = value_;

  bind = func <B>(f : A -> Array<B>) : Array<B> {
    let xs : A[] = value;
    var ys : B[] = [];
    for (i in xs.keys()) {
      ys := arrayConcat<B>(ys, f(xs[i]).value);
    };
    Array<B>(ys);
  };
};

So the issue seems related to init returning an Array which has a bind field that returns an Array.

[paulyoung]

Replacing Self with Array and vice-versa makes no difference.

[rossberg]

Here is a more minimal example:

type Array<A> = {
  bind : <B> (A -> Array<B>) -> ();
};

let xs : Array<Nat> = new {
  bind<B>(f : Nat -> Array<B>) {};
};

I know what the problem is, and this particular example could be fixed (for the price of making type checking more expensive).

However, more broadly, this code does something we so far intended to forbid anyway, namely, it uses "non-uniform recursion" in a type definition, that is, there is a recursive use of a type name with different type arguments than its own parameters. Allowing that with equi-recursive types makes type-checking undecidable in general, i.e., the type-checker may not terminate because you are generating infinitely large type derivations. There is a TODO in the type checker somewhere to add a check flagging a type definition like Array as illegal.

We could try to relax this restriction somehow, though it is quite difficult to identify weaker but sufficient criteria to prevent bad cases.

[paulyoung]

@rossberg thanks for explaining.

I'll leave this open as a reminder to make this fail to type check but feel free to close.

[rossberg]

I leave it open as a tracking issue for implementing the check; changed title accordingly.

[paulyoung]

I was thinking that an alternative way of achieving the example I provided was to do something like the following, but it's not possible without being able to access self/this within the body of a class.

Is that something that could be supported?

class Array<A>(value_ : A[]) {
  value = value_;

  bind = func <B>(f : A -> Array<B>) : Array<B> {
    array.bind<A, B>(self, f);
  };
};

let array = new {
  bind = func <A, B>(xs : Array<A>, f : A -> Array<B>) : Array<B> {
    var ys : B[] = [];
    for (i in xs.value.keys()) {
      ys := arrayConcat<B>(ys, f(xs.value[i]).value);
    };
    Array<B>(ys);
  };
};

[rossberg]

I'm afraid that may run into the same problem, because of a class definition's dual role as a type definition. Currently classes are nominal, which may save this, but I'm not sure we want to keep it that way, so I'd rather be conservative.

As for "self" in class definitions, yes this absolutely needs fixing, too. The only blocker is finding a syntax that fits with the rest of the language. I have a local branch where I allow "class C(...) = self { ... }", which is the best I could come up with so far, but requires the "=".

[paulyoung]

I gave the changes in #79 a try at some point over the holiday and think I may have encountered the same issue.

As expected (based on the diff in #79) I get some errors at first:

class Array<A>(value_ : A[]) = self {
  value = value_;

  bind = func <B>(f : A -> Array<B>) : Array<B> {
    array.bind<A, B>(self, f);
  };
};

let array = new {
  bind = func <A, B>(xs : Array<A>, f : A -> Array<B>) : Array<B> {
    var ys : B[] = [];
    for (i in xs.value.keys()) {
      ys := arrayConcat<B>(ys, f(xs.value[i]).value);
    };
    Array<B>(ys);
  };
};

/* Stub */
let arrayConcat = func <A>(xs : A[], ys : A[]) : A[] {
  xs;
};

Untitled.as:5.22-5.26: type error, expression of type
  {bind : <B>(A/6 -> Array<B>) -> Array<B>; value : A/6[]}
cannot produce expected type
  Array<A/6>

---

I added some additional like keywords and it caused the type checker to use 100% CPU and continue increasing in memory usage the longer it ran. I'm only showing 1 redundant like below but orignally I had added more.

class Array<A>(value_ : A[]) = self {
  value = value_;

-  bind = func <B>(f : A -> Array<B>) : Array<B> {
+  bind = func <B>(f : A -> Array<B>) : like Array<B> {
    array.bind<A, B>(self, f);
  };
};

let array = new {
-  bind = func <A, B>(xs : Array<A>, f : A -> Array<B>) : Array<B> {
+  bind = func <A, B>(xs : like Array<A>, f : A -> Array<B>) : Array<B> {
    var ys : B[] = [];
    for (i in xs.value.keys()) {
      ys := arrayConcat<B>(ys, f(xs.value[i]).value);
    };
    Array<B>(ys);
  };
};

/* Stub */
let arrayConcat = func <A>(xs : A[], ys : A[]) : A[] {
  xs;
};

In this small example I was able to trigger a stack overflow (output below) but at the time it showed no sign of stopping and I eventually killed it.

(unknown location): internal error, Stack overflow

Last environment:

Raised by primitive operation at file "typing.ml", line 299, characters 10-28
Called from file "typing.ml" (inlined), line 287, characters 13-36
Called from file "typing.ml", line 627, characters 13-30
Called from file "typing.ml", line 589, characters 2-23
Called from file "typing.ml", line 983, characters 4-23
Called from file "typing.ml", line 964, characters 2-47
Called from file "typing.ml", line 616, characters 11-42
Called from file "typing.ml", line 589, characters 2-23
Called from file "typing.ml", line 939, characters 6-45
Called from file "typing.ml", line 909, characters 10-50
Called from file "typing.ml", line 555, characters 24-52
Called from file "typing.ml", line 299, characters 10-28
Called from file "typing.ml" (inlined), line 287, characters 13-36
Called from file "typing.ml", line 627, characters 13-30
Called from file "typing.ml", line 589, characters 2-23
Called from file "typing.ml", line 887, characters 8-57
Called from file "list.ml", line 111, characters 24-34
Called from file "typing.ml", line 864, characters 4-68
Called from file "typing.ml", line 827, characters 11-51
Called from file "typing.ml", line 950, characters 13-66
Called from file "typing.ml", line 1009, characters 14-31
Called from file "typing.ml", line 22, characters 6-9
Called from file "typing.ml" (inlined), line 28, characters 6-27
Called from file "typing.ml", line 976, characters 16-50
Called from file "typing.ml" (inlined), line 964, characters 2-47
Called from file "typing.ml", line 1170, characters 2-40
Called from file "pipeline.ml", line 154, characters 43-70
Called from file "pipeline.ml", line 116, characters 37-52
Called from file "pipeline.ml", line 149, characters 10-41
Called from file "pipeline.ml", line 186, characters 8-23
Called from file "pipeline.ml", line 251, characters 15-33
Called from file "main.ml", line 69, characters 35-62
Called from file "main.ml", line 98, characters 4-23

This works as expected:

class Array<A>(value_ : A[]) = self {
  value = value_;

  bind = func <B>(f : A -> Array<B>) : Array<B> {
    array.bind<A, B>(self, f);
  };
};

let array = new {
-  bind = func <A, B>(xs : Array<A>, f : A -> Array<B>) : Array<B> {
+  bind = func <A, B>(xs : like Array<A>, f : A -> Array<B>) : Array<B> {
    var ys : B[] = [];
    for (i in xs.value.keys()) {
      ys := arrayConcat<B>(ys, f(xs.value[i]).value);
    };
    Array<B>(ys);
  };
};

/* Stub */
let arrayConcat = func <A>(xs : A[], ys : A[]) : A[] {
  xs;
};

[rossberg]

Well, non-termination may or may not manifest itself as a stack overflow, depending on whether it loops in a tail recursion or not.

[crusso]

@paulyoung, @rossberg

I think this error is actually unrelated to non-regular types

Untitled.as:5.22-5.26: type error, expression of type
  {bind : <B>(A/6 -> Array<B>) -> Array<B>; value : A/6[]}
cannot produce expected type
  Array<A/6>

It appears to be an instance of issue #150; which was fixed in fixed in 8a11b26

[rossberg]

@crusso, I think you're right.

[nomeata]

Now at https://dfinity.atlassian.net/browse/AST-20

[nomeata]

Look what I found: A at least P2 level issue that’s 15 months old, and got dropped on the floor due to the Jira migration :-)

[nomeata]

Just run

> type Foo<A> = Foo<(A,A)>;

in the interpreter to see how it fails.

[nomeata]

Closing in favor of #1279