Fix reachability by retaining spaces of Prod params

[dwijnand]

When intersecting a product type space with a type space, if the two
types aren't related, we must retain the spaces of the parameters,
otherwise the intersection will represent a bigger space of values that
it should (leading to a false positive unreachability warning).

I actually think that the first condition, isSubType(tp1, tp2), should
be true, because Bar is a subtype of Foo[X], provided X is
instantiated to Nothing. Maybe that's not isSubType but something
else (because we want forSome X, not forAll X). But, either way, fixing
that the intersection doesn't overpromise (i.e. lie) is a good fix
anyways.

[dwijnand]

This is what the log looks like for the part I mean. I've fixed this now by making the intersection return Prod(Bar & Foo[X], [1 (Typ((1 : Int)))]). But ideally I would want to somehow make Bar <:< Foo[X] return true. To do that I think I need to replace the instantiated X for a fresh variable, allowing it to become instantiated to Nothing. @odersky do you know how to do that mapping?

[log elimOpaque]   ==> Bar(1) & _: Foo[X]?
[log elimOpaque]     ==> Bar <:< Foo[X]?
[log elimOpaque]       ==> isSubType Bar <:< Foo[X]?
[log elimOpaque]         ==> isSubType Foo[Nothing] <:< Foo[X] (left is approximated)?
[log elimOpaque]           ==> isSubType X <:< Nothing?
[log elimOpaque]             ==> isSubType Any <:< Nothing (left is approximated)?
[log elimOpaque]             <== isSubType Any <:< Nothing (left is approximated) = false
[log elimOpaque]           <== isSubType X <:< Nothing = false
[log elimOpaque]         <== isSubType Foo[Nothing] <:< Foo[X] (left is approximated) = false
[log elimOpaque]       <== isSubType Bar <:< Foo[X] = false
[log elimOpaque]     <== Bar <:< Foo[X] = false
[log elimOpaque]     ==> Foo[X] <:< Bar?
[log elimOpaque]       ==> isSubType Foo[X] <:< Bar?
[log elimOpaque]       <== isSubType Foo[X] <:< Bar = false
[log elimOpaque]     <== Foo[X] <:< Bar = false
[log elimOpaque]   <== Bar(1) & _: Foo[X] = Bar(1) (Prod(Bar & Foo[X], [1 (Typ((1 : Int)))])

[dwijnand]

This fixes the issue, so it's mergeable as it is, but I'm asking as I would like to see if I can improve it further.

[odersky]

Creating new type variables looks like GADT territory. Maybe @abgruszecki can comment. For the space logic it looks OK to me, but I am no expert. @liufengyun could you take a quick look?

[odersky]

I am not an expert, so I can't comment on the logic. It looks reasonable to me and I found no other problems.

[liufengyun]

LGTM, thanks for the fix @dwijnand 👍

[liufengyun]

Aside: We could experiment by introducing a space called Unknown(tp: Type) for this case later.

Edited: Sorry, I meant the case above (the 1st case).

[dwijnand]

The case is only for Empty, when the two types are provably disjoint, so I'm not sure what we'd want to preserve the type for. But I'm not against the idea.

[dwijnand]

Btw, I sort of introduced this regression when I made the change in 202b63e without realising I was forgetting the subpatterns of the product spaces (the components/params).