After ... discussion and testing ... the only section of this bug report that needs action is the section Explicitly calling T.from x

The following focuses on Table but of course similar issues will appear for Column and other cases where we use intersection types to 'refine' types.

We are relying on intersection types to implement some kind of subtyping relationship, or more precisely a type-extension mechanism, allowing us to have a base type like Table and a type that contains some additional backend-specific functionality - e.g. DB_Table.

We create instances of table and immediately use refine_table method to return a multi-value Table & DB_Table. The user should never be able to get a 'raw' Table or DB_Table without the other part available (though it may be hidden and require a cast).

As was mentioned in some discussions, our cast y = x:T is supposed to act as a kind-of instanceof check.

When we create a database table, we give it the compound Table & DB_Table type. As the value flows through the program, because of various casts, parts of this compound type may become hidden.

However, to upkeep the 'subtyping' metaphor, we should never allow one part of such intersection type to be completely removed. For the user, removing part of the intersection type means that they can no longer bring it back using instanceof. Imagine a scenario where the user queries a database table. They get an object that is DB_Table & Table. Via passing it around (not transforming it, just passing it around as-is) it somehow loses DB_Table part. Now the user wants to use it in a place that expects DB_Table. Even via casting, the DB_Table part can no longer be brought back. This is a problem - the user is clearly holding a database table, but because this part of intersection type got removed, they cannot use it as DB_Table anymore.

Below I summarize situations that we've found that completely remove parts of an intersection type instead of merely hiding them:

Cast to a type that is available but hidden

Currently we could not find a simple repro, so maybe the issue was just something intermittent. We will create a separate ticket if this issue comes back.

Currently it seems that if I have x : A & (hidden B) (I will mark types that are present but not visible as 'hidden'), and there exists a conversion B.from A, then casting x to B seems to prefer using the conversion instead of just uncovering the already existing hidden B.

The primary issue is - calling a conversion hides the A part, whereas if we used the already existing B part, A would only become hidden but would still be available.

It also unnecessarily calls the conversion which may be costly, even though the result is already present in the EnsoMultiValue, just hidden. This is less problematic but also not ideal.

TODO repro

Explicitly calling T.from x

The syntaxes y = x:T and y = T.from x are very similar, but not equivalent.

The former allows for multi types - y = x : A&B which the latter does not support.

But most importantly, if x has type T & U then x:T will only hide the U part, but T.from x completely removes the U part.

As described above this is causing problems, so probably T.from x should keep all existing types, if the type T can already be found among the intersection type (visible or hidden). There is no need to call any actual conversion code if T can be found.

Example

from Standard.Base import all

type A
    A_Ctor a
type B
    B_Ctor b

B.from that:A =
    B.B_Ctor that

main =
    ab = A.A_Ctor 12 : A & B
    IO.println "ab : "+(Meta.Multi_Type.get ab . to_text)

    b = B.from ab
    IO.println "b : "+(Meta.Multi_Type.get b . to_text)

    # No longer possible because `B.from` removed the `A` part
    a = b : A
    IO.println "a : "+(Meta.Multi_Type.get a . to_text)

yields

ab : A & B
b : B
Execution finished with an error: Type error: expected expression to be A, but got B.
        at <enso> test.main(test.enso:19:9-9)
Type error: expected expression to be A, but got B.

Calling B.from ab removes the A part and then it can no longer be uncovered. If it instead just uncovered B and hidden A, it would still be possible to uncover it later.