Better mismatch errors for type unions and intersections

[fwbrasil]

Compiler version

3.3.0

Minimized example

A common encoding for libraries is to use intersection and union types to express requirements a computation might have. For example, ZIO uses a type intersection for the environment channel and an union for the error channel, Tapir uses a similar approach to express capabilities, and Kyo uses an intersection to represent the set of pending algebraic effects.

def test1(v: String & Integer & List[String]) = ()
def test2(v: String & Long) = test1(v)

def test3(v: String | Integer | List[String]) = ()
def test4(v: String | Long) = test3(v)

Output Error/Warning message

[error] -- [E007] Type Mismatch Error: test.scala:14:56
[error] 14 |  def test2(v: String & Long) = test1(v)
[error]    |                                                        ^
[error]    |                               Found:    (v : String & Long)
[error]    |                               Required: String & Integer & List[String]
[error]    |
[error]    | longer explanation available when compiling with `-explain`
[error] -- [E007] Type Mismatch Error: test.scala:17:56
[error] 17 |  def test4(v: String | Long) = test3(v)
[error]    |                                                        ^
[error]    |                               Found:    (v : String | Long)
[error]    |                               Required: String | Integer | List[String]
[error]    |
[error]    | longer explanation available when compiling with `-explain

Why this Error/Warning was not helpful

Users normally have issues to understand where the mismatch is since the types can end up accumulating several components.

Suggested improvement

Provide a message that highlights where the differences are. Ideally, it should also consider variance. For example, a contravariant type parameter can receive an intersection that has a subset of its components without issues.

zio-clippy is a good source of inspiration although it's specific to ZIO. It improves error messages by parsing and transforming them.

cc/ @hmemcpy

[odersky]

I agree it would be a HUGE improvement if TypeMismatch errors could be diagnosed more precisely. But it's also a huge undertaking. TypeComparer goes through a maze of many possible paths to prove a subtype relation that in the end does not hold. For instance, I append the current output with -explain, which just records the possibilities that were tried and is as such not very helpful except for experts. How to condense that without giving false or misleading info? It's certainly a challenging task.

2 |def test2(v: String & Long) = test1(v)
  |                                    ^
  |                                 Found:    (v : String & Long)
  |                                 Required: String & Integer & List[String]
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: v
  | I tried to show that
  |   (v : String & Long)
  | conforms to
  |   String & Integer & List[String]
  | but the comparison trace ended with `false`:
  |
  |   ==> (v : String & Long)  <:  String & Integer & List[String]
  |     ==> (v : String & Long)  <:  String & Integer
  |       ==> (v : String & Long)  <:  String
  |         ==> (v : String & Long)  <:  String
  |           ==> String  <:  String (left is approximated)
  |           <== String  <:  String (left is approximated) = true
  |         <== (v : String & Long)  <:  String = true
  |       <== (v : String & Long)  <:  String = true
  |       ==> (v : String & Long)  <:  Integer
  |         ==> glb(<notype>, <notype>)
  |         <== glb(<notype>, <notype>) = <notype>
  |         ==> String & Long  <:  Integer (left is approximated)
  |           ==> glb(<notype>, <notype>)
  |           <== glb(<notype>, <notype>) = <notype>
  |           ==> String  <:  Integer (left is approximated)
  |             ==> String  <:  Integer (left is approximated)
  |             <== String  <:  Integer (left is approximated) = false
  |           <== String  <:  Integer (left is approximated) = false
  |           ==> Long  <:  Integer (left is approximated)
  |           <== Long  <:  Integer (left is approximated) = false
  |         <== String & Long  <:  Integer (left is approximated) = false
  |       <== (v : String & Long)  <:  Integer = false
  |     <== (v : String & Long)  <:  String & Integer = false
  |   <== (v : String & Long)  <:  String & Integer & List[String] = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------
-- [E007] Type Mismatch Error: test.scala:5:36 ---------------------------------
5 |def test4(v: String | Long) = test3(v)
  |                                    ^
  |                                 Found:    (v : String | Long)
  |                                 Required: String | Integer | List[String]
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: v
  | I tried to show that
  |   (v : String | Long)
  | conforms to
  |   String | Integer | List[String]
  | but the comparison trace ended with `false`:
  |
  |   ==> (v : String | Long)  <:  String | Integer | List[String]
  |     ==> String | Long  <:  String | Integer | List[String]
  |       ==> String  <:  String | Integer | List[String]
  |         ==> String  <:  String | Integer | List[String]
  |           ==> String  <:  String | Integer
  |             ==> String  <:  String
  |               ==> String  <:  String
  |               <== String  <:  String = true
  |             <== String  <:  String = true
  |           <== String  <:  String | Integer = true
  |         <== String  <:  String | Integer | List[String] = true
  |       <== String  <:  String | Integer | List[String] = true
  |       ==> Long  <:  String | Integer | List[String]
  |         ==> Long  <:  String | Integer
  |           ==> Long  <:  String
  |             ==> Long  <:  String
  |             <== Long  <:  String = false
  |           <== Long  <:  String = false
  |           ==> Long  <:  Integer
  |           <== Long  <:  Integer = false
  |         <== Long  <:  String | Integer = false
  |         ==> Long  <:  List[String]
  |         <== Long  <:  List[String] = false
  |       <== Long  <:  String | Integer | List[String] = false
  |     <== String | Long  <:  String | Integer | List[String] = false
  |     ==> (v : String | Long)  <:  String | Integer
  |       ==> String | Long  <:  String | Integer
  |         ==> String  <:  String | Integer
  |           ==> String  <:  String | Integer
  |             ==> String  <:  String
  |               ==> String  <:  String
  |               <== String  <:  String = true
  |             <== String  <:  String = true
  |           <== String  <:  String | Integer = true
  |         <== String  <:  String | Integer = true
  |         ==> Long  <:  String | Integer
  |           ==> Long  <:  String
  |             ==> Long  <:  String
  |             <== Long  <:  String = false
  |           <== Long  <:  String = false
  |           ==> Long  <:  Integer
  |           <== Long  <:  Integer = false
  |         <== Long  <:  String | Integer = false
  |       <== String | Long  <:  String | Integer = false
  |       ==> (v : String | Long)  <:  String
  |         ==> (v : String | Long)  <:  String
  |           ==> lub(String, <notype>, canConstrain=false, isSoft=true)
  |           <== lub(String, <notype>, canConstrain=false, isSoft=true) = <notype>
  |           ==> String | Long  <:  String (left is approximated)
  |             ==> String  <:  String (left is approximated)
  |               ==> String  <:  String (left is approximated)
  |               <== String  <:  String (left is approximated) = true
  |             <== String  <:  String (left is approximated) = true
  |             ==> Long  <:  String (left is approximated)
  |             <== Long  <:  String (left is approximated) = false
  |           <== String | Long  <:  String (left is approximated) = false
  |         <== (v : String | Long)  <:  String = false
  |       <== (v : String | Long)  <:  String = false
  |       ==> (v : String | Long)  <:  Integer
  |         ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
  |         <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
  |         ==> String | Long  <:  Integer (left is approximated)
  |           ==> String  <:  Integer (left is approximated)
  |             ==> String  <:  Integer (left is approximated)
  |             <== String  <:  Integer (left is approximated) = false
  |           <== String  <:  Integer (left is approximated) = false
  |         <== String | Long  <:  Integer (left is approximated) = false
  |       <== (v : String | Long)  <:  Integer = false
  |       ==> String | Long  <:  String | Integer (left is approximated)
  |         ==> String  <:  String | Integer (left is approximated)
  |           ==> String  <:  String | Integer (left is approximated)
  |             ==> String  <:  String (left is approximated)
  |               ==> String  <:  String (left is approximated)
  |               <== String  <:  String (left is approximated) = true
  |             <== String  <:  String (left is approximated) = true
  |           <== String  <:  String | Integer (left is approximated) = true
  |         <== String  <:  String | Integer (left is approximated) = true
  |         ==> Long  <:  String | Integer (left is approximated)
  |           ==> Long  <:  String (left is approximated)
  |             ==> Long  <:  String (left is approximated)
  |             <== Long  <:  String (left is approximated) = false
  |           <== Long  <:  String (left is approximated) = false
  |           ==> Long  <:  Integer (left is approximated)
  |           <== Long  <:  Integer (left is approximated) = false
  |         <== Long  <:  String | Integer (left is approximated) = false
  |       <== String | Long  <:  String | Integer (left is approximated) = false
  |     <== (v : String | Long)  <:  String | Integer = false
  |     ==> (v : String | Long)  <:  List[String]
  |       ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
  |       <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
  |       ==> String | Long  <:  List[String] (left is approximated)
  |         ==> String  <:  List[String] (left is approximated)
  |           ==> String  <:  List[String] (left is approximated)
  |           <== String  <:  List[String] (left is approximated) = false
  |         <== String  <:  List[String] (left is approximated) = false
  |       <== String | Long  <:  List[String] (left is approximated) = false
  |     <== (v : String | Long)  <:  List[String] = false
  |     ==> String | Long  <:  String | Integer | List[String] (left is approximated)
  |       ==> String  <:  String | Integer | List[String] (left is approximated)
  |         ==> String  <:  String | Integer | List[String] (left is approximated)
  |           ==> String  <:  String | Integer (left is approximated)
  |             ==> String  <:  String (left is approximated)
  |               ==> String  <:  String (left is approximated)
  |               <== String  <:  String (left is approximated) = true
  |             <== String  <:  String (left is approximated) = true
  |           <== String  <:  String | Integer (left is approximated) = true
  |         <== String  <:  String | Integer | List[String] (left is approximated) = true
  |       <== String  <:  String | Integer | List[String] (left is approximated) = true
  |       ==> Long  <:  String | Integer | List[String] (left is approximated)
  |         ==> Long  <:  String | Integer (left is approximated)
  |           ==> Long  <:  String (left is approximated)
  |             ==> Long  <:  String (left is approximated)
  |             <== Long  <:  String (left is approximated) = false
  |           <== Long  <:  String (left is approximated) = false
  |           ==> Long  <:  Integer (left is approximated)
  |           <== Long  <:  Integer (left is approximated) = false
  |         <== Long  <:  String | Integer (left is approximated) = false
  |         ==> Long  <:  List[String] (left is approximated)
  |         <== Long  <:  List[String] (left is approximated) = false
  |       <== Long  <:  String | Integer | List[String] (left is approximated) = false
  |     <== String | Long  <:  String | Integer | List[String] (left is approximated) = false
  |   <== (v : String | Long)  <:  String | Integer | List[String] = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------
2 errors found

[odersky]

Note also that if actual and expected types are syntactically similar, we already do color-based diffing. The problem arises when they are not syntactically similar.

[fwbrasil]

Although the type resolution mechanism has to explore multiple paths to determine soundness, wouldn't it be possible to improve the error at a later stage after the mismatch is detected? If there's a mismatch of union or intersection types, it seems a simple diff could produce a good error message as zio-clippy does. Variance might make a generic logic more difficult to implement since I image zio-clippy assumes ZIO's specific variance behavior.

Another path that could be interesting to explore is allowing libraries to define custom type mismatch error reporting. I'd say that would be even more convenient since libraries could provide more advanced error messages considering their APIs and common user mistakes. I tried to implement that via implicits and macros but I couldn't create a mechanism that doesn't interfere with the type inference of Kyo computations.

[odersky]

I did a partial fix in #18742, which improves the situation in that it makes -explain traces more concise and a little bit less scary.

For the rest, if someone else has a good idea how to make concrete progress and has time to explore this, please have a go at this.