Nullable inference not tracking Boolean logic correctly with Debug.Assert

[stephentoub]

Version:
3.0.0-beta4-19170-01+1deafee3682da88bf07d1c18521a99f47446cee8

#nullable enable
using System;
using System.Diagnostics;

class Program
{
    static void Main() { }

    static void Foo(object? first, object? second)
    {
        Debug.Assert(first != null || second != null);

        if (first != null)
        {
            Console.WriteLine(first.GetHashCode());
        }
        else
        {
            Console.WriteLine(second.GetHashCode());
        }
    }
}

This warns on the last line that second might be null ("Possible dereference of a null reference"), but the compiler should be able to see that's not possible, given the Assert that at least one of first or second is non-null and then that first is null.

cc: @cston, @jaredpar, @dotnet/nullablefc

[gafter]

We do not track the relationship between multiple variables. The specified analysis says that the state of a variable is either known not to be null, or else that it might contain null. After the assertion, we have no further information of that sort to add to the pool of knowledge.

In short, while a human can deduce that there is no problem on the last line, and perhaps so could a sufficiently powerful theorem prover, we have specified a realistic analysis that cannot and does not do what you expect. And the compiler implements that specified analysis.

[stephentoub]

It sounds like you're saying a more powerful one is feasible but we've decided it's not worth it. Ok. Just means more !s I guess... what's a few more when you already have a lot :)

[gafter]

We've settled on our current approach as a sweet spot balancing moderate complexity of analysis (i.e. implementable in a reasonable time frame and with reasonable performance) and customer value. I don't believe we've explicitly discussed (or "decided" against) a theorem-prover style analysis, which is what would be needed. The reason we didn't discuss it is that there is no member of the LDM that believes it would be an improvement over our current approach.

[stephentoub]

no member of the LDM that believes it would be an improvement over our current approach

Ok. It depends of course on how you define "an improvement". Fewer warnings due to more complete analysis seems like an improvement to me, but I get that it's a tradeoff.

[gafter]

@stephentoub you are a member of the LDM. Why don’t you propose that we drop our plans to release the nullable reference types feature in the C# 8 timeframe and spin up a team of engineers to develop a theorem-prover style analyzer for some indefinite future release?

[stephentoub]

Hyperbole isn't necessary here. I opened an issue to highlight cases that we're hitting not-infrequently while annotating corelib, in hopes of making the overall feature better, and I'm questioning statements that suggest it's not actually an issue that, if addressed, would make the situation better for our collective customers. I've also stated multiple times that I understand it's a tradeoff.

[gafter]

I agree my comment was unwarranted, and that there is customer value that our current approach doesn't address. We've looked at this sort of inference in passing in the context of contracts, but we've never gotten to the point that we think it is something we should do in the product. I'll open a language feature request corresponding to this product issue.

[stephentoub]

Thanks, Neal. Sounds good.