Unresolved Generic Recursive Reference being Captured

[ScottCarda-MS]

In the runtime repo, there is a circuit defined as follows:

function GenRecursionPartial<'T> (x : 'T, cnt : Int) : 'T {        
    if (cnt == 0) {
        return x;
    }
    else {
        let fct = GenRecursionPartial(_, cnt - 1);
        return fct(x);
    }
}

This circuit shouldn't be allowed because we don't support capturing unresolved generic references. The fct is doing exactly that by capturing the recursive call omitting the argument that would have resolved its type parameter. After having captured this generic, one would now expect to be able to do:

...
let temp = fct("Hi");
let temp2 = fct(3);
...

But of course this is not allowed as we don't handle captured generics like this in the language.

The reason this is happening is because of the ambiguity in the data structure that represents the type parameter resolution, and the way we represent an unresolved type parameter. The data structure only contains the name of the callable to which the type parameter belongs, the name of the type parameter, and the resolving type. This is not enough information to be able to determine which instance of the type parameter is being resolved. In this case the compiler is getting confused because it can't tell the difference between a reference to the context's GenRecursionPartial.T and a reference to the recursive call's GenRecursionPartial.T.

The way unresolved type parameters are represented is that the type parameter is shown to resolve to itself, i.e. Foo.T -> Foo.T means that Foo.T is unresolved. In this case, however the GenRecursionPartial.T -> GenRecursionPartial.T, which is supposed to indicate that GenRecursionPartial.T is unresolved is mistakenly being interpreted as the call's GenRecursionPartial.T being resolved to the context's GenRecursionPartial.T, which is not the case. This is causing the definition of fct to be incorrectly resolved without the appropriate error.

[ScottCarda-MS]

The related runtime issue to remove this circuit is found here: https://github.com/microsoft/qsharp-runtime/issues/343

[bamarsha]

If this bug is fixed, would

function GenRecursionPartial<'T>(x : 'T, cnt : Int) : 'T {        
    if (cnt == 0) {
        return x;
    }
    else {
        let fct = GenRecursionPartial<'T>(_, cnt - 1);
        return fct(x);
    }
}

still be a valid program?

[ScottCarda-MS]

@samarsha No it would not. The linked issue for in the runtime repo is for removing that test case.

[bamarsha]

My example is different from that test case: it adds a <'T> after the second GenRecursionPartial.

[ScottCarda-MS]

My example is different from that test case: it adds a <'T> after the second GenRecursionPartial.

Oh sorry I didn't notice that it was different. Yes your example would work fine, as the 'T in that context could only refer to the calling context's GenRecursionPartial.T.

[bettinaheim]

@ScottCarda-MS The issue has nothing to do with the representation - it is merely a bug in the implementation (I simply forgot). https://github.com/microsoft/qsharp-compiler/pull/576 contains the fix.