infinite loop during type-checking

[gelisam]

Somehow, giving the compiler some help in figuring out the type of (mk-phantom-1) causes it to loop forever :(

#lang kernel

(datatype (Phantom A)
  (mk-phantom-1))

-- correctly infers ∀α. (Phantom α)
(define mk-phantom-2
  (with-unknown-type [A]
    (the A
      (mk-phantom-1))))

-- loops forever
(define mk-phantom-3
  (with-unknown-type [A]
    (the (Phantom A)
      (mk-phantom-1))))

[david-christiansen]

Missing occurs check?

[gelisam]

We do have an occurs check for the type-checker... but not for the kind-checker! The problem is that we have a KMetaVar which points to itself, so zonkKindDefault calls itself forever.

[gelisam]

Turns out the problem was not quite an occurs-check.

An easy way to trigger the problem is to unify KMetaVar 1 with KMetaVar 2, and then to again unify KMetaVar 1 with KMetaVar 2. The second unification should be a no-op, but instead causes KMetaVar 2 to point to itself.

Before the first unification, KMetaVar 1 and KMetaVar 2 both point to nothing; that is, they are both roots.

The first unification is a flex-flex case with two roots, so we arbitrarily choose to make KMetaVar 1 point to KMetaVar 2.

The second unification is a flex-flex case with one root. We make the root KMetaVar 2 point to to the non-root KMetaVar 1. We thus have a loop: KMetaVar 2 now points to KMetaVar 1, which was already pointing to KMetaVar 2. And path-compression makes KMetaVar 2 point to itself.

[gelisam]

I have fixed the problem in #251, but separately, we should still add an occurs-check to the kind checker. Let's see, what kind of example would trigger the problem? :thinking:

[gelisam]

Ah, but of course, the type A A would do it!

It turns out that the syntax (A A) is not supported when A is introduced by with-unknown-type, but is allowed when A is introduced by datatype:

(datatype (InfiniteKind A)
  (mk-infinite-kind (Phantom (A A))))

[gelisam]

251 now has uses both examples in this file as a test, and fixes both bugs. Note that if I only added the kind-level occurs-check, then the first example would be rejected instead of accepted, so there really were two separate bugs.