Better mismatch errors for type unions and intersections #18737

fwbrasil · 2023-10-20T14:19:29Z

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 · 2023-10-21T12:08:49Z

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 · 2023-10-21T12:11:21Z

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.

This is a partial fix of scala#18737. We still can't explain the differences concisely, but at least we shorten the comparison traces by showing only steps that contributed to the overall failure and by avoiding repetitions.

fwbrasil · 2023-10-21T21:59:02Z

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 · 2023-10-23T08:30:08Z

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.

This is a partial fix for #18737. We still can't explain the differences concisely, but at least we shorten the comparison traces by showing only steps that contributed to the overall failure and by avoiding repetitions.

This is a partial fix of #18737. We still can't explain the differences concisely, but at least we shorten the comparison traces by showing only steps that contributed to the overall failure and by avoiding repetitions. [Cherry-picked afa2e30]

fwbrasil added area:reporting Error reporting including formatting, implicit suggestions, etc better-errors Issues concerned with improving confusing/unhelpful diagnostic messages itype:enhancement stat:needs triage Every issue needs to have an "area" and "itype" label labels Oct 20, 2023

nicolasstucki added area:typer and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Oct 20, 2023

odersky mentioned this issue Oct 21, 2023

Shorten traces for TypeMismatch errors under -explain #18742

Merged

nicolasstucki assigned odersky Oct 23, 2023

odersky removed their assignment Oct 23, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Better mismatch errors for type unions and intersections #18737

Better mismatch errors for type unions and intersections #18737

fwbrasil commented Oct 20, 2023 •

edited

Loading

odersky commented Oct 21, 2023 •

edited

Loading

odersky commented Oct 21, 2023 •

edited

Loading

fwbrasil commented Oct 21, 2023

odersky commented Oct 23, 2023

Better mismatch errors for type unions and intersections #18737

Better mismatch errors for type unions and intersections #18737

Comments

fwbrasil commented Oct 20, 2023 • edited Loading

Compiler version

Minimized example

Output Error/Warning message

Why this Error/Warning was not helpful

Suggested improvement

odersky commented Oct 21, 2023 • edited Loading

odersky commented Oct 21, 2023 • edited Loading

fwbrasil commented Oct 21, 2023

odersky commented Oct 23, 2023

fwbrasil commented Oct 20, 2023 •

edited

Loading

odersky commented Oct 21, 2023 •

edited

Loading

odersky commented Oct 21, 2023 •

edited

Loading