Unexpected tuple recovery errors

[dipinhora]

In the following example (http://pony-playpen.lietar.net/?gist=c743e444341e9e721aa94a7e732efc5f):

actor Main
  new create(e: Env) =>
    var a: String iso = recover iso String end

    a = recover iso
        let z = consume ref a
        z.append("hello")
        consume z
    end

    (a, let b) = recover iso // changing `a` to `let c` makes it compile/work
        let z = consume ref a
        z.append("hello")
        (consume z, U32(1))
    end

the second recover causes the following error:

0.14.0 [release]
compiled with: llvm 3.9.1 -- cc (Ubuntu 5.4.0-6ubuntu1~16.04.4) 5.4.0 20160609
Error:
main.pony:11:16: right side must be a subtype of left side
    (a, let b) = recover iso // changing `a` to `let c` makes it compile/work
               ^
    Info:
    main.pony:3:12: String ref is not a subtype of String iso: ref is not a subcap of iso
        var a: String iso = recover iso String end
               ^
    main.pony:14:19: (String ref, U32 val) is not a pairwise subtype of (String iso, U32 val)
            (consume z, U32(1))
                      ^

Changing the (a, let b) to (let c, let b) allows it to compile successfully but changing to: (let c: String iso, let b) causes the same error again.

Another related example can be found at: http://pony-playpen.lietar.net/?gist=caf6ba62122eaa0d09df89e18fb65374

[Praetonus]

This error comes from the rules ironed out in #1123 to prevent unsafe recovery of tuples.

I think there are two solutions here

1. Improve the error message to better reflect the rules from #1123
2. Base tuple recovery logic on shared fields as briefly discussed in #1123. This could possibly be non-trival and/or lead to bad compilation times

We could also do both, and say which fields are shared in the error message.

[dipinhora]

@Praetonus I don't understand how the example is an unsafe recovery of the tuple since both elements seem safe.

If it's not too much trouble, could you explain why the example is unsafe?

[jemc]

@Praetonus in this week's call, I thought you mentioned another possible solution - expanding the rules to allow examples like this (recovering (ref, val) to (iso, val), while still disallowing recovery of tuples where more than one element is ref or box in the pre-recovered tuple.

[Praetonus]

@dipinhora This particular example is safe, but the compiler currently doesn't try to determine that and simply doesn't recover tuples with mutable elements, which prevents some safe cases from working.

@jemc Yeah this could work too. I think we can recover tuples when all elements but one are sendable (or trn when recovering to trn).

[jemc]

I think we can recover tuples when all elements but one are sendable

Yeah, that sounds right to me. That should cover anything that is possible to do by setting up a var outside the recover block, and assigning to it on the inside, which is obviously safe iff the cap for that var is sendable.

[dipinhora]

@Praetonus I don't know if it's possible or not, but having an error message that indicates the this is a current compiler limitation would be much better in my opinion. I spent a considerable amount of time trying to figure out what I was doing wrong in my more complex code before boiling it down to the example above.

If the compiler error indicated that this is a current limitation of tuple recovery and so is disallowed instead of giving the error it gave, I could have moved on to solving the problem in another way much earlier.

[Praetonus]

We discussed this during today's sync meeting. A more detailed error is desirable and probably possible.

We need to explore how to provide "deferred error contexts". When a tuple is recovered without actually lifting the capabilities because of safety reasons, an error context explaining that should be associated with the recover AST (or with the tuple type, depending on which one is easier to track down later). Then, if a subtyping error is encountered, the tuple error context should be reported alongside the subtyping error. If the program is correct, the error context should be discarded.