Skip to content

Type alias for dependent function type expanded incorrectly when nested #5592

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.

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

Closed
kory33 opened this issue Dec 10, 2018 · 9 comments · Fixed by #11847
Closed

Type alias for dependent function type expanded incorrectly when nested #5592

kory33 opened this issue Dec 10, 2018 · 9 comments · Fixed by #11847

Comments

@kory33
Copy link

kory33 commented Dec 10, 2018

This occurs on the latest master.

For the code below, the type of eqSymmetric1, eqSymmetric2 and eqSymmetric3 should all be equivalent.

object Test {
  type Obj
  type Forall[F[_]] = (x: Obj) => F[x.type]

  trait =::=[A, B] { def sub[F[_]]: F[A] => F[B]; def commute: B =::= A = this.sub[[b] => b =::= A](implicitly[A =::= A]) }
  implicit def typeEq[A]: A =::= A = new =::=[A, A] { def sub[F[_]]: F[A] => F[A] = identity }

  // these are both fine
  val eqReflexive1: (x: Obj) => (x.type =::= x.type) = { x: Obj => implicitly }
  val eqReflexive2: Forall[[x] => x =::= x] = { x: Obj => implicitly }

  // this compiles
  val eqSymmetric1: (x: Obj) => ((y: Obj) => ((x.type =::= y.type) => (y.type =::= x.type))) = {
    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
  }

  /** crashes (assertion failed)
  val eqSymmetric2: Forall[[x] => (y: Obj) => (x =::= y.type) => (y.type =::= x)] = {
    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
  }*/

  /** type error
  val eqSymmetric3: Forall[[x] => Forall[[y] => (x =::= y) => (y =::= x)]] = {
    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
  }
  */
}

However, when eqSymmetric2 is included, the compiler crashes with:

exception occurred while typechecking Test.scala
exception occurred while compiling Test.scala
java.lang.AssertionError: assertion failed: (y: Test.Obj): _ <: Test.Obj =::= y.type => y.type =::= _ <: Test.Obj & (y: Test.Obj): v1.type =::= y.type => y.type =::= v1.type / MethodType(List(y), List(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj)), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Function1),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TypeBounds(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Nothing),TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj)), TermParamRef(y))), AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TermParamRef(y), TypeBounds(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Nothing),TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj))))))) & MethodType(List(y), List(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj)), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Function1),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TermParamRef(v1), TermParamRef(y))), AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TermParamRef(y), TermParamRef(v1)))))) while compiling Test.scala
Exception in thread "main" java.lang.AssertionError: assertion failed: (y: Test.Obj): _ <: Test.Obj =::= y.type => y.type =::= _ <: Test.Obj & (y: Test.Obj): v1.type =::= y.type => y.type =::= v1.type / MethodType(List(y), List(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj)), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Function1),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TypeBounds(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Nothing),TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj)), TermParamRef(y))), AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TermParamRef(y), TypeBounds(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Nothing),TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj))))))) & MethodType(List(y), List(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),type Obj)), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Function1),List(AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TermParamRef(v1), TermParamRef(y))), AppliedType(TypeRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),module class Test$)),class =::=),List(TermParamRef(y), TermParamRef(v1))))))
        at dotty.DottyPredef$.assertFail(DottyPredef.scala:38)
        at dotty.tools.dotc.core.Types$AndType$.apply(Types.scala:2675)
        at dotty.tools.dotc.core.TypeComparer.andType$$anonfun$1(TypeComparer.scala:1571)
        at dotty.tools.dotc.core.TypeComparer.liftIfHK(TypeComparer.scala:1609)
        at dotty.tools.dotc.core.TypeComparer.andType(TypeComparer.scala:1571)
        at dotty.tools.dotc.core.TypeComparer.glb(TypeComparer.scala:1389)
        at dotty.tools.dotc.core.Types$Type.$amp(Types.scala:915)
        at dotty.tools.dotc.core.TypeComparer.distributeAnd(TypeComparer.scala:1647)
        at dotty.tools.dotc.core.TypeComparer.andType(TypeComparer.scala:1565)
        at dotty.tools.dotc.core.TypeComparer.glb(TypeComparer.scala:1389)
        at dotty.tools.dotc.core.Types$Type.$amp(Types.scala:915)
        at dotty.tools.dotc.core.Denotations$Denotation.infoMeet$2(Denotations.scala:439)
        at dotty.tools.dotc.core.Denotations$Denotation.infoMeet$2(Denotations.scala:419)
        at dotty.tools.dotc.core.Denotations$Denotation.mergeSingleDenot$1(Denotations.scala:538)
        at dotty.tools.dotc.core.Denotations$Denotation.mergeDenot$1(Denotations.scala:455)
        at dotty.tools.dotc.core.Denotations$Denotation.$amp(Denotations.scala:561)
        at dotty.tools.dotc.core.Types$Type.goRefined$1(Types.scala:653)
        at dotty.tools.dotc.core.Types$Type.go$1(Types.scala:569)
        at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:702)
        at dotty.tools.dotc.core.Types$Type.memberBasedOnFlags(Types.scala:533)
        at dotty.tools.dotc.core.Types$Type.nonPrivateMember(Types.scala:523)
        at dotty.tools.dotc.core.Types$abstractTermNameFilter$.apply(Types.scala:4985)
        at dotty.tools.dotc.core.Types$Type.memberNames$$anonfun$1(Types.scala:731)
        at scala.collection.TraversableLike.$anonfun$filterImpl$1(TraversableLike.scala:247)
        at scala.collection.immutable.Set$Set1.foreach(Set.scala:95)
        at scala.collection.TraversableLike.filterImpl(TraversableLike.scala:246)
        at scala.collection.TraversableLike.filterImpl$(TraversableLike.scala:244)
        at scala.collection.AbstractTraversable.filterImpl(Traversable.scala:104)
        at scala.collection.TraversableLike.filter(TraversableLike.scala:258)
        at scala.collection.TraversableLike.filter$(TraversableLike.scala:258)
        at scala.collection.AbstractTraversable.filter(Traversable.scala:104)
        at dotty.tools.dotc.core.Types$Type.memberNames(Types.scala:731)
        at dotty.tools.dotc.core.Types$Type.memberNames(Types.scala:733)
        at dotty.tools.dotc.core.Types$Type.memberDenots(Types.scala:747)
        at dotty.tools.dotc.core.Types$Type.abstractTermMembers(Types.scala:754)
        at dotty.tools.dotc.core.Types$SAMType$.unapply(Types.scala:4229)
        at dotty.tools.dotc.typer.Typer.decomposeProtoFunction(Typer.scala:757)
        at dotty.tools.dotc.typer.Typer.typedFunctionValue(Typer.scala:837)
        at dotty.tools.dotc.typer.Typer.typedFunction(Typer.scala:772)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1934)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1979)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2010)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2022)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:2085)
        at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:683)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1932)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1979)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2010)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2022)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:2085)
        at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:683)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1932)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1979)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2010)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2022)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:2085)
        at dotty.tools.dotc.typer.Typer.typedValDef(Typer.scala:1461)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1909)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1978)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2010)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2022)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:2041)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:2074)
        at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:1633)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1915)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1978)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2010)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2022)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:2041)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:2074)
        at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:1751)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1957)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1979)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2010)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2022)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:2085)
        at dotty.tools.dotc.typer.FrontEnd.typeCheck$$anonfun$1(FrontEnd.scala:60)
        at scala.compat.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)
        at dotty.tools.dotc.typer.FrontEnd.monitor(FrontEnd.scala:34)
        at dotty.tools.dotc.typer.FrontEnd.typeCheck(FrontEnd.scala:64)
        at dotty.tools.dotc.typer.FrontEnd.runOn$$anonfun$2(FrontEnd.scala:88)
        at scala.compat.java8.JProcedure1.apply(JProcedure1.java:18)
        at scala.compat.java8.JProcedure1.apply(JProcedure1.java:10)
        at scala.collection.immutable.List.foreach(List.scala:388)
        at dotty.tools.dotc.typer.FrontEnd.runOn(FrontEnd.scala:88)
        ...

and when eqSymmetric3 is included, a type error is given:

-- [E007] Type Mismatch Error: Test.scala:21:72 --------------------------------
21 |    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
   |                                                                        ^
   |found:    (y: Test.Obj) => Test.Obj(x) =::= y.type => y.type =::= Test.Obj(x)
   |required: (x: Test.Obj) => (_ <: Test.Obj =::= x'.type => x'.type =::= _ <: Test.Obj) & 
   |  Test.Forall[[y] => Test.Obj(x) =::= y' => y' =::= Test.Obj(x)]
   |
   |where:    x  is a value in an anonymous function in object Test
   |          x' is a reference to a value parameter
   |          y  is a reference to a value parameter
   |          y' is a type variable
-- [E007] Type Mismatch Error: Test.scala:21:74 --------------------------------
21 |    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
   |                                                                          ^
   |found:    (x: Test.Obj) => (x: Test.Obj) => (_ <: Test.Obj =::= x.type => x.type =::= _
   |   <: Test.Obj
   |) & Test.Forall[[y] => x'.type =::= y => y =::= x'.type]
   |required: Test.Forall[[x] => Test.Forall[[y] => x'' =::= y' => y' =::= x'']]
   |
   |where:    x   is a reference to a value parameter
   |          x'  is a reference to a value parameter
   |          x'' is a type variable
   |          y   is a type variable
   |          y'  is a type variable
two errors found
@Blaisorblade
Copy link
Contributor

The compiler seems to crash because it's trying to construct the And of two method types (which are not value types as defined in the spec), instead of two function types (which are, and can be combined in an intersection), but it's not clear why MethodTypes would be there — or even why an and is being constructed (tho that might be ok).

Replacing eqSymmetric2 with the following also gives a type error, similar to the one you show:

  type Foo = [x] => (y: Obj) => (x =::= y.type) => (y.type =::= x)
  val eqSymmetric2: Forall[Foo] = {
    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
  }
-- [E007] Type Mismatch Error: mytmp/i5592.scala:20:72 -------------------------
20 |    { x: Obj => { y: Obj => { xEqy: x.type =::= y.type => xEqy.commute } } }
   |                                                                        ^
   |found:    (y: Test.Obj) => Test.Obj(x) =::= y.type => y.type =::= Test.Obj(x)
   |required: (y: Test.Obj) => (_ <: Test.Obj =::= y'.type => y'.type =::= _ <: Test.Obj) &
   |  Test.Foo[Test.Obj(x)]
   |
   |where:    y  is a reference to a value parameter
   |          y' is a reference to a value parameter
one error found

liufengyun added a commit that referenced this issue Dec 17, 2018
Fix #5592: Fix & of method type refinements
@kory33
Copy link
Author

kory33 commented Dec 18, 2018

Although the crash is resolved in 158ccd7, I believe the test which was added by this commit should not be a negative test, since I expect the types of eqsymmetric2 and eqsymmetric3 to be expanded to that of eqsymmetric1.

For reference, the code on eqSymmetric2, with the test code above, produces a type error

-- [E007] Type Mismatch Error: Test.scala:23:70 --------------------------------
23 |    { x: Obj => { y: Obj => { xEqy: EQ[x.type, y.type] => xEqy.commute } } } // error // error
   |                                                                      ^
   |Found:    Test.EQ[Test.Obj(x), Test.Obj(y)] => Test.EQ[Test.Obj(y), Test.Obj(x)]
   |Required: Test.EQ[_ <: Test.Obj, Test.Obj(y)] => Test.EQ[Test.Obj(y), Test.Obj(x)]
-- [E007] Type Mismatch Error: Test.scala:23:74 --------------------------------
23 |    { x: Obj => { y: Obj => { xEqy: EQ[x.type, y.type] => xEqy.commute } } } // error // error
   |                                                                          ^
   |Found:    (x: Test.Obj) => (y: Test.Obj) => Test.EQ[_ <: Test.Obj, y.type] => 
   |  Test.EQ[y.type, x.type]
   |Required: Test.Forall[[x] => (y: Test.Obj) => Test.EQ[x', y'.type] => Test.EQ[y'.type, x']
   |  ]
   |
   |where:    x  is a reference to a value parameter
   |          x' is a type variable
   |          y  is a reference to a value parameter
   |          y' is a reference to a value parameter

nicolasstucki pushed a commit to dotty-staging/dotty that referenced this issue Jan 5, 2019
In `distributeAnd` we need to combine refinements in the same
way denotation infos are combined, with special treatement of
method and poly types.
@kory33
Copy link
Author

kory33 commented Jan 10, 2019

@Blaisorblade the issue (of the wrong/unintuitive alias expansion) does not seems to be resolved. Would you mind reopening this?

@Blaisorblade
Copy link
Contributor

I can’t look closely, but the output seems indeed nonsensical. At the very least I can’t tell where y’ comes from. In fact, that’s another variable named y, which the compiler adds a ‘ to, to point out it’s not the same as y. Why that’d be the case, I don’t know.

@kory33
Copy link
Author

kory33 commented Jan 11, 2019

I believe there is a separate bug in the pretty print of the error message here.

For example, take

-- [E007] Type Mismatch Error: Test.scala:23:74 --------------------------------
23 |    { x: Obj => { y: Obj => { xEqy: EQ[x.type, y.type] => xEqy.commute } } } // error // error
   |                                                                          ^
   |Found:    (x: Test.Obj) => (y: Test.Obj) => Test.EQ[_ <: Test.Obj, y.type] => 
   |  Test.EQ[y.type, x.type]
   |Required: Test.Forall[[x] => (y: Test.Obj) => Test.EQ[x', y'.type] => Test.EQ[y'.type, x']
   |  ]
   |
   |where:    x  is a reference to a value parameter
   |          x' is a type variable
   |          y  is a reference to a value parameter
   |          y' is a reference to a value parameter

In the Required section, there is a type x bound by Forall and value parameter y, which I think are meant for x' and y' respectively.

@Blaisorblade
Copy link
Contributor

Re pretty-print: to be sure x’ is not a legal name in Scala. The ‘ is added to distinguish different identifiers which happen to have the same name. In other words, to undo shadowing. I filed a bug about this because I also find it misleading.

So, in the message you quote, the compiler thinks there are two identifiers named x, and they are different. Which is even correct, since x’ is a type variable, and Forall instantiates it to x.type.

However, maybe x should indeed be x’ in Forall[[x]; that would indeed be a pretty-printing bug.

@kory33
Copy link
Author

kory33 commented Jan 15, 2019

I was having a close look on the following code, which I expect to compile:

object Test {
  def assertEqType[A, B >: A <: A]: Unit = Unit
  def assertSubType[A, B >: A]: Unit = Unit

  {
    // type error(does not conform to lower bound A)
    assertSubType[
      (x: Unit) => ((y: Unit) => x.type =:= y.type),
      ([F[_]] => (z: Unit) => F[z.type])[[x] => (y: Unit) => x =:= y.type]
    ]

    // compiles
    assertEqType[
      ([F[_]] => (z: Unit) => F[z.type])[[x] => ([F[_]] => (z: Unit) => F[z.type])[[y] => x =:= y]],
      ([F[_]] => (z: Unit) => F[z.type])[[x] => (y: Unit) => x =:= y.type]
    ]
  }
}

checking the typed tree of the code, it seems like the type (x: Unit) => ((y: Unit) => x.type =:= y.type) is expanded to

(Unit =>
 ((Unit => =:=[_, _]) {
  def apply(y: Unit): =:=[_, _]
 })
) {
 def apply(x: Unit): (Unit => =:=[x.type, _]) {
  def apply(y: Unit): =:=[x.type, y.type]
 }
}

and the type ([F[_]] => (z: Unit) => F[z.type])[[x] => (y: Unit) => x =:= y.type] is expanded to

(Unit =>
 ((Unit => =:=[_, _]) {
  def apply(y: Unit): =:=[_, y.type]
 })
) {
 def apply(z: Unit): (Unit => =:=[z.type, _]) {
  def apply(y: Unit): =:=[z.type, y.type]
 }
}

which is actually a subtype of the first one. Since the type lambda version is somehow giving a more concrete type, I believe these issues come from parent type in the (refined) expansion of dependent type.

Is there any particular reason why we need to calculate the upper bound U of the expanded type (T => U) { def apply(...): ... } of dependent function type, instead of giving it up to Any and expecting more information to be recovered from refinement part?

@odersky
Copy link
Contributor

odersky commented Mar 6, 2020

Closing for inactivity and a lack of direction what should be done here.

@odersky
Copy link
Contributor

odersky commented Mar 22, 2021

It looks like this is fixed by #11847

odersky added a commit to dotty-staging/dotty that referenced this issue Mar 22, 2021
Approximating type maps should not compute illegal unreducible wildcard applications.
Instead they should propagate the Range outwards

Fixes scala#5592
michelou pushed a commit to michelou/scala3 that referenced this issue Mar 25, 2021
Approximating type maps should not compute illegal unreducible wildcard applications.
Instead they should propagate the Range outwards

Fixes scala#5592
michelou pushed a commit to michelou/scala3 that referenced this issue Apr 14, 2021
Approximating type maps should not compute illegal unreducible wildcard applications.
Instead they should propagate the Range outwards

Fixes scala#5592
@Kordyjan Kordyjan added this to the 3.0.0 milestone Aug 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants