Type checking, type inference, and unification bug(s) with higher rank types

[dhil]

In using Links' first-class polymorphism I have stumbled upon what appears to be a curious interaction amongst the type checker, type inference engine, and the unification engine. Consider the following System F-y partial implementation of lists.

typename List(a) = forall t. ((a, t) {}-> t, t) {}-> t;

sig cons : (a, List(a)) {}-> List(a)
fun cons(x, xs)(cons, nil) { cons(x, xs(cons, nil)) }

sig foldr : ((a, b) {}-> b, b, List(a)) {}-> b
fun foldr(f, z, xs) { xs(f, z) }

sig dup : (List(a)) {}-> List(a)
fun dup(xs) { foldr(cons, xs, xs) }

The dup function appends a given list onto itself.

The program ought to type check, alas it fails in Links with the following error message.

test.links:43: Type error: The function
    `foldr'
has type
    `((a, List (a)) {}-> List (a), List (a), List (a)) {}-> List (a)'
while the arguments passed to it have types
    `(a, List (a)) {}-> List (a)'
and
    `List (a)'
and
    `List (a)'
and the currently allowed effects are
    `'
In expression: foldr(cons, xs, xs).

It complains about the definition of the dup function. On the surface the error message is rather silly as all the types appear to line up perfectly. By toggling unification tracing we can get a bit more information about what is going on.

...
Unification error: Cannot unify type variable 6609 with datatype List (_) because the type variable occurs unguarded inside the datatype

Curiously the guardedness check has kicked in, yet there is no recursive type, or recursion for that matter, in the source program! This seems like a bug to me!

If we inline the definition of foldr in dup, then we get another curious error

sig dup : (List(a)) {}-> List(a)
fun dup(xs) { xs(cons, xs) }

...
Unification error: Couldn't match ((a, List (a)) {}-> List (a), List (a)) {}-> List (a) against ((a, List (a)) {}-> List (a), List (a)) {}-@ _::Any
test.links:43: Type error: The function
    `xs'
has type
    `List (a)'
while the arguments passed to it have types
    `(a, List (a)) {}-> List (a)'
and
    `List (a)'
and the currently allowed effects are
    `'
In expression: xs(cons, xs).

Out of nowhere a linear function type appears! This seems like another bug to me!

[jamescheney]

Hmm. Something very strange is happening. I think the fact that it's a list type is irrelevant, the same thing happens with Church numerals:

typename Nat = forall t. ((t) {}-> t, t) {}-> t;

sig succ : (Nat) {}-> Nat
fun succ(x)(s,z) {s(x(s,z))}

sig rec : ((a) {}-> a, a,Nat) {}-> a
fun rec(s,z,n) {n(s,z)}

sig double : (Nat) {}-> Nat
fun double(n) {rec(succ,n,n)}

yields the same problem.

However, if you inline Nat in the above then already succ doesn't typecheck:

sig succ : (forall t. ((t) {}-> t, t) {}-> t) {}-> forall t. ((t) {}-> t, t) {}-> t
fun succ(x)(s,z) {s(x(s,z))}

you get this error:

<stdin>:2: Type error: The non-recursive function definition has type
    `(forall a.((a) {}-> a, a) {}-> a) {}-> (b::Any, c::Any) -d-> e::Any'
but it is annotated with type
    `(forall a.((a) {}-> a, a) {}-> a) {}-> forall f.((f) {}-> f, f) {}-> f'
In expression: fun succ(x)(s,z) {s(x(s,z))}.

Of course, this should not have typechecked in the first place, because the curried inner function needs to be broken out to get its own quantifiers:

sig succ : (forall t. ((t) {}-> t, t) {}-> t) {}-> forall t. ((t) {}-> t, t) {}-> t
fun succ(x) { 
  sig foo : forall t. ((t) {}-> t, t) {}-> t 
  fun foo(s,z) {s(x(s,z))} 
  ~foo
}

I think this is because type synonyms are not "referentially transparent" in the presence of first-class forall.

Then

sig rec : ((a) {}-> a, a,forall t. ((t) {}-> t, t) {}-> t) {}-> a
fun rec(s,z,n) {n(s,z)}

works. On the other hand

sig double : (forall t. ((t) {}-> t, t) {}-> t) {}-> forall t. ((t) {}-> t, t) {}-> t
fun double(n) {rec(succ,n,n)}

doesn't typecheck, but the reason is that to pass n to fold we need to freeze it to preserve the quantifiers:

sig double : (forall t. ((t) {}-> t, t) {}-> t) {}-> forall t. ((t) {}-> t, t) {}-> t
fun double(n) {rec(succ,~n,~n)}

If we undo the inlining, we get:

sig succ : (Nat) {}-> Nat
fun succ(x) { 
  sig foo : Nat
  fun foo(s,z) {s(x(s,z))} 
  ~foo
}

sig rec : ((a) {}-> a, a,Nat) {}-> a
fun rec(s,z,n) {n(s,z)}

sig double : (Nat) {}-> Nat
fun double(n) {rec(succ,~n,~n)}

then we get the same error as before (which makes sense because the definition of succ is irrelevant to typecheching double). So I conjecture that something is wrong with how aliases are treated if the aliased type is polymorphic. Time to write an ESOP paper, I guess.

[jamescheney]

I think the second problem, with linear types being guessed incorrectly, is because in general Links guesses a linear function type if it can, and doesn't revisit this choice later because it would make typechecking exponential. I think this is the intended behavior, though I can also rationalize calling it a bug (I'd like to see if we can use Garrett's approach to linearity using qualified types from ICFP16 here eventually.)

[slindley]

I haven't looked at this closely, but I did notice immediately that the original code shouldn't work because you would need to freeze any variable of type List(a) in order to ensure that it doesn't get instantiated... I guess this relates to @jamescheney's observation about polymorphic type aliases in some sense failing to be "referentially transparent".

It wouldn't surprise me at all if we assume in some places in the code that if the variable x has type T(a) then the term x has type T(a). However, this is a property that should not hold in the case that T(a) is an alias for a polymorphic type as x should be implicitly instantiated.