Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Tuple#tail along with shapeless.labelled.FieldType encoding triggers type error #16481

Closed
mrdziuban opened this issue Dec 8, 2022 · 3 comments
Closed

Tuple#tail along with shapeless.labelled.FieldType encoding triggers type error #16481

mrdziuban opened this issue Dec 8, 2022 · 3 comments
Labels
area:match-types itype:bug stat:needs spec

Comments

@mrdziuban
Copy link

Compiler version

3.2.1

Minimized code

https://scastie.scala-lang.org/mrdziuban/kOxLqWh4S5iXYTAqxvY6gw/11

// Equivalent encoding to shapeless
// https://github.com/milessabin/shapeless/blob/main/core/shared/src/main/scala/shapeless/labelled.scala#L24-L32
type FieldType[K, +V] = V with KeyTag[K, V]
trait KeyTag[K, +V] extends Any
def field[K]: [v] => v => FieldType[K, v] = [v] => (v: v) => v.asInstanceOf[FieldType[K, v]]

type SB = FieldType["str", String] *: FieldType["bool", Boolean] *: EmptyTuple
type ISB = FieldType["int", Int] *: SB

val isb: ISB = field["int"](1) *: field["str"]("foo") *: field["bool"](true) *: EmptyTuple
val sb: SB = isb.tail

Output

-- [E007] Type Mismatch Error: /Users/matt/scala-3-playground/src/main/scala/example/Test.scala:14:15
14 |  val sb: SB = isb.tail
   |               ^^^^^^^^
   |Found:    Tuple.Tail[(example.Test.FieldType[("int" : String), Int],
   |  example.Test.FieldType[("str" : String), String]
   |, example.Test.FieldType[("bool" : String), Boolean])]
   |Required: example.Test.SB
   |
   |Note: a match type could not be fully reduced:
   |
   |  trying to reduce  Tuple.Tail[
   |  (example.Test.FieldType[("int" : String), Int],
   |    example.Test.FieldType[("str" : String), String]
   |  , example.Test.FieldType[("bool" : String), Boolean])
   |]
   |  failed since selector  (example.Test.FieldType[("int" : String), Int],
   |  example.Test.FieldType[("str" : String), String]
   |, example.Test.FieldType[("bool" : String), Boolean])
   |  is uninhabited (there are no values of that type).
   |----------------------------------------------------------------------------
   | Explanation (enabled by `-explain`)
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |
   | Tree: example.Test.isb.tail[
   |
   |     (example.Test.FieldType[("int" : String), Int],
   |       example.Test.FieldType[("str" : String), String]
   |     , example.Test.FieldType[("bool" : String), Boolean])
   |
   | ]
   | I tried to show that
   |   Tuple.Tail[
   |   (example.Test.FieldType[("int" : String), Int],
   |     example.Test.FieldType[("str" : String), String]
   |   , example.Test.FieldType[("bool" : String), Boolean])
   | ]
   | conforms to
   |   example.Test.SB
   | but the comparison trace ended with `false`:
   |
   |   ==> AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB)
   |     ==> AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple)))))
   |       ==> MatchType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple),TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB)))),List(HKTypeLambda(List(_$15, xs), List(TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Any)), TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple))), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class runtime)),class MatchCase),List(AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),*:),List(TypeParamRef(_$15), TypeParamRef(xs))), TypeParamRef(xs))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple)))))
   |         ==> TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple)  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple)))))
   |         <== TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple)  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))) = false
   |       <== MatchType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple),TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB)))),List(HKTypeLambda(List(_$15, xs), List(TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Any)), TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple))), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class runtime)),class MatchCase),List(AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),*:),List(TypeParamRef(_$15), TypeParamRef(xs))), TypeParamRef(xs))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))) = false
   |     <== AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))) = false
   |   <== AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB) = false
   |
   | The tests were made under a constraint with:
   |  uninstantiated variables: This
   |  constrained types:
   |   [This >: (example.Test.isb : example.Test.ISB) <: NonEmptyTuple]:
   |     Tuple.Tail[This]
   |  bounds:
   |      This >: (example.Test.isb : example.Test.ISB) <: NonEmptyTuple
   |  ordering:
    ----------------------------------------------------------------------------
Explanation
===========
[error]
Tree: example.Test.isb.tail[
[error]
    (example.Test.FieldType[("int" : String), Int],
      example.Test.FieldType[("str" : String), String]
    , example.Test.FieldType[("bool" : String), Boolean])
[error]
]
I tried to show that
  Tuple.Tail[
  (example.Test.FieldType[("int" : String), Int],
    example.Test.FieldType[("str" : String), String]
  , example.Test.FieldType[("bool" : String), Boolean])
]
conforms to
  example.Test.SB
but the comparison trace ended with `false`:
[error]
  ==> AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB)
    ==> AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple)))))
      ==> MatchType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple),TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB)))),List(HKTypeLambda(List(_$15, xs), List(TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Any)), TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple))), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class runtime)),class MatchCase),List(AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),*:),List(TypeParamRef(_$15), TypeParamRef(xs))), TypeParamRef(xs))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple)))))
        ==> TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple)  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))
        <== TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple)  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))) = false
      <== MatchType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple),TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB)))),List(HKTypeLambda(List(_$15, xs), List(TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Any)), TypeBounds(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Nothing),TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),trait Tuple))), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class runtime)),class MatchCase),List(AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),*:),List(TypeParamRef(_$15), TypeParamRef(xs))), TypeParamRef(xs))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))) = false
    <== AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(str)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Predef),type String))), AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(bool)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Boolean))), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class scala)),object Tuple$package),type EmptyTuple))))) = false
  <== AppliedType(TypeRef(TermRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),Tuple),Tail),List(TypeVar(TypeParamRef(This) -> AppliedType(TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class *:),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type FieldType),List(ConstantType(Constant(int)), TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int))), TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB))))))  <:  TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class example)),module class Test$)),type SB) = false
[error]
The tests were made under a constraint with:
 uninstantiated variables: This
 constrained types:
  [This >: (example.Test.isb : example.Test.ISB) <: NonEmptyTuple]:
    Tuple.Tail[This]
 bounds:
     This >: (example.Test.isb : example.Test.ISB) <: NonEmptyTuple
 ordering:

Expectation

The compiler can prove that Tuple.Tail[ISB] =:= SB
@mrdziuban mrdziuban added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Dec 8, 2022
@prolativ prolativ added area:match-types and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Dec 9, 2022
@prolativ
Copy link
Contributor

prolativ commented Dec 9, 2022

I think it's because the compiler cannot reduce a type when it contains and intersection with a final type, like a String or it's singleton version, e.g. these two snippets don't compile

trait Tag
type Id[A] = A
type Tagged = ("abc" with Tag) match
  case Id[t] => t
val ev = summon[Tagged =:= ("abc" with Tag)]
trait Foo
trait Tag
type Id[A] = A
type Tagged = (Foo with Tag) match
  case Id[t] => t
val ev = summon[Tagged =:= (Foo with Tag)]

but this one does:

trait Tag
type Id[A] = A
type Tagged = (String with Tag) match
  case Id[t] => t
val ev = summon[Tagged =:= (String with Tag)]

@prolativ
Copy link
Contributor

prolativ commented Dec 9, 2022

Actually I'm not really sure something like "abc" with Tag should be considered a valid type.
Could such types cause some soundness issues? @odersky @smarter

@mrdziuban
Copy link
Author

I just found (thanks to milessabin/shapeless#1200) that using type KeyTag[K, +V] instead of trait makes it work -- https://scastie.scala-lang.org/mrdziuban/kOxLqWh4S5iXYTAqxvY6gw/12

That said, feel free to close this if you think the behavior is reasonable

@WojciechMazur WojciechMazur closed this as not planned Won't fix, can't repro, duplicate, stale Dec 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
area:match-types itype:bug stat:needs spec
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@mrdziuban @prolativ @WojciechMazur