Compiler error, probably type inference bug with path-dependent types

Sorry, hit "Send" to fast.

You can verify the problem by downloading metascala from here: http://www.assembla.com/spaces/metascala/wiki

There is a deactivated test where the author seems to have hit the same problem:

http://trac.assembla.com/metascala/browser/src/metascala/test/UnitsTest....

I would be very grateful if someone could give me some hint ... or has some idea how a minimized example could look like.

Thanks and bye,


Simon

This gets even weirder.

It looks like it has nothing to do with the path-dependent types, I could reproduce it without going into the "negative" space.

I use a simplified version, which only uses one unit, length, to make things shorter. Have a look:

val length:  Quantity[_1] = 5 m              //Works
val area:    Quantity[_2] = length * length  //Works, too.
val length2: Quantity[_1] = area / length    //Doesn't work!

The code for Addables/Subtractables is pretty much the same (and equivalent).

I really wonder what's the problem here...

Any ideas?

I was able to produce a smaller example.

This code shows the problem:

object UnitsTest extends App {
  import Units._
  import Integers._
   
  val length1 = m(23)
  val length2 = m(17)
  val area: Quantity[_2, _0] = length1 * length2 // Works
  
  val time = s(42)
  val foo: Quantity[_1, _1] = time * length1  // Works
 
  val speed: Quantity[_1, _1#Neg] = length1 / time // Doesn't work
  /*
  type mismatch;
    found   :
      Units.Quantity[Subtractables.-[Integers._1,Integers._0],
                     Subtractables.-[Integers._0,Integers._1]]
    required:
      Units.Quantity[Integers._1,Integers._0]
  */
 
  val lengt3: Quantity[_1, _0] = length1 * length2 / length1 // Doesn't work
  /*
  type mismatch;
    found   :
      Units.Quantity[Subtractables.-[Addables.+[Integers._1,Integers._1],Integers._1],
                     Subtractables.-[Addables.+[Integers._0,Integers._0],Integers._0]]
    required:
      Units.Quantity[Integers._1,Integers.MNeg[Integers.MSucc[Integers._0]]]   
   */
}


Backing code is this:

object Units {
  import Integers._
  import Addables._
  import Subtractables._

  trait Unit {
    type M <: MInt
    type S <: MInt
  }
 
  final class TUnit[_M <: MInt, _S <: MInt] {
    type M = _M
    type S = _S
  }
 
  case class Quantity[M <: MInt, S <: MInt](value : Double) {
    type This = Quantity[M, S]
    def *[M2 <: MInt, S2 <: MInt](m : Quantity[M2, S2]) = Quantity[M + M2, S + S2](value * m.value)
    def /[M2 <: MInt, S2 <: MInt](m : Quantity[M2, S2]) = Quantity[M - M2, S - S2](value / m.value)
    def apply(v : Double) = Quantity[M, S](v * value)
  }
   
  val m = Quantity[_1, _0](1)
  val s = Quantity[_0, _1](1)
}

object Addables {
  trait Addable {
    type AddType <: Addable
    type Add[T <: AddType] <: AddType
  }

  type +[A1 <: Addable, A2 <: A1#AddType] = A1#cdcdcd[A2] 
}

object Subtractables {
  trait Subtractable {
    type SubType <: Subtractable
    type Sub[T <: SubType] <: SubType
  }

  type -[S1 <: Subtractable, S2 <: S1#SubType] = S1#Sub[S2]
}

object Comparables {
  import Booleans._

  trait Comparable {
    type CompareType <: Comparable
    type LessThan[T <: CompareType] <: Bool
  }
}


object Booleans {
  sealed trait Bool {
    type Not <: Bool
  }
 
  final class True extends Bool {
    type Not = False
  }
 
  final class False extends Bool {
    type Not = True
  }
}

object Integers {
  import Visitables._
  import Addables._
  import Subtractables._

  trait NatVisitor extends TypeVisitor {
    type Visit0 <: ResultType
    type VisitSucc[Pre <: Nat] <: ResultType
  }
 
  trait IntVisitor extends NatVisitor {
    type VisitNeg[Pos <: Nat] <: ResultType
  }
 
  sealed trait MInt extends Visitable[IntVisitor] with Addable with Subtractable {
    type AddType = MInt
    type SubType = MInt
    type Add[I <: MInt] <: MInt
    type Neg <: MInt
    type Succ <: MInt
    type Pre <: MInt
  }
 
  sealed trait Nat extends MInt {
    type Accept[V <: IntVisitor] = AcceptNatVisitor[V]
    type AcceptNatVisitor[V <: NatVisitor] <: V#ResultType
  }
 
  final class _0 extends Nat {
    type Add[I <: MInt] = I
    type AcceptNatVisitor[V <: NatVisitor] = V#Visit0
    type Neg = _0
    type Succ = MSucc[_0]
    type Pre = Succ#Neg
  }
 
  sealed trait Pos extends Nat
 
  final class MSucc[P <: Nat] extends Pos {
    type This = MSucc[P]
    type Add[N <: MInt] = P#cdcdcd[N]#Succ
    type AcceptNatVisitor[V <: NatVisitor] = V#VisitSucc[P]
    type Neg = MNeg[This]
    type Pre = P
    type Succ = MSucc[This]
  }
 
  final class MNeg[N <: Pos] extends MInt {
    type Add[N <: MInt] = N#cdcdcd[N#Neg]#Neg
    type Accept[V <: IntVisitor] = V#VisitNeg[N]
    type Neg = N
    type Succ = N#Pre#Neg
    type Pre = N#Succ#Neg
  }
 
  type _1 = MSucc[_0]
  type _2 = MSucc[_1]
  type _3 = MSucc[_2]
 
  val _0 = new _0
  val _1 = new _1
  val _2 = new _2
  val _3 = new _3
}

object Nats {
  import Utils._
  import Booleans._
  import Addables._
  import Comparables._
  import Visitables._

  trait NatVisitor extends TypeVisitor {
    type Visit0 <: ResultType
    type VisitSucc[Pre <: Nat] <: ResultType
  }
 
  sealed trait Nat extends Addable with Comparable {
    type CompareType = Nat
   
    type Pre
    type Is0 <: Bool
    type Add[T <: Nat] <: Nat
    type AddType = Nat
    type Accept[N <: NatVisitor] <: N#ResultType
    type Equals[N <: Nat] <: Bool
    type LessThan[N <: Nat] <: Bool

    def toInt : Int
  }
 
  final class _0 extends Nat {
    type Pre = Invalid
    type Is0 = True
    type Add[N <: Nat] = N
    type Accept[N <: NatVisitor] = N#Visit0

    type Equals[N <: Nat] = N#Is0
    type LessThan[N <: Nat] = N#Is0#Not

    def toInt = 0
  }
 
  final case class Succ[P <: Nat](toInt : Int) extends Nat {
    type Pre = P
    type Is0 = False
    type Add[N <: Nat] = Succ[P#cdcdcd[N]]
    type Accept[N <: NatVisitor] = N#VisitSucc[P]

    trait EqualsVisitor extends NatVisitor {
      type ResultType = Bool
      type Visit0 = False
      type VisitSucc[Pre <: Nat] = P#Equals[Pre]
    }

    type Equals[N <: Nat] = N#Accept[EqualsVisitor]

    trait LessThanVisitor extends NatVisitor {
      type ResultType = Bool
      type Visit0 = False
      type VisitSucc[Pre <: Nat] = P#LessThan[Pre]
    }

    type LessThan[N <: Nat] = N#Accept[LessThanVisitor]

    def +[N <: Nat](n : N) : Add[N] = Succ[P#cdcdcd[N]](toInt + n.toInt)
  }
 
  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]
 
  val _0 = new _0
  val _1 = new _1(1)
  val _2 = new _2(2)
  val _3 = new _3(3)
}

object Visitables {
  trait TypeVisitor {
    type ResultType
  }

  trait Visitable[V <: TypeVisitor] {
    type Accept[V2 <: V] <: V2#ResultType
  }
}

object Utils {
  final class Invalid

  case class TypeToValue[T, VT](value : VT) {
    def apply() = value
  }
}

Any ideas what's the problem or how can I debug it?

Thanks and bye,


Simon

scalac -explaintypes results in this output:

UnitsTest.scala:12: error: type mismatch;
 found   : Units.Quantity[Subtractables.-[Integers._1,Integers._0],Subtractables.-[Integers._0,Integers._1]]
 required: Units.Quantity[Integers._1,Integers.MNeg[Integers.MSucc[Integers._0]]]
  val speed: Quantity[_1, _1#Neg] = length1 / time // Doesn't work
                                            ^
Units.Quantity[Subtractables.-[Integers._1,Integers._0],Subtractables.-[Integers._0,Integers._1]] <: Units.Quantity[Integers._1,Integers.MNeg[Integers.MSucc[Integers._0]]]?
  Integers._1 <: Subtractables.-[Integers._1,Integers._0]?
    Integers.MSucc[Integers._0] <: Nothing?
      <notype> <: Nothing?
      false
    false
  false
false


UnitsTest.scala:22: error: type mismatch;
 found   : Units.Quantity[Subtractables.-[Addables.+[Integers._1,Integers._1],Integers._1],Subtractables.-[Addables.+[Integers._0,Integers._0],Integers._0]]
 required: Units.Quantity[Integers._1,Integers._0]
  val lengt3: Quantity[_1, _0] = length1 * length2 / length1 // Doesn't work
                                                   ^
Units.Quantity[Subtractables.-[Addables.+[Integers._1,Integers._1],Integers._1],Subtractables.-[Addables.+[Integers._0,Integers._0],Integers._0]] <: Units.Quantity[Integers._1,Integers._0]?
  Integers._1 <: Subtractables.-[Addables.+[Integers._1,Integers._1],Integers._1]?
    Integers.MSucc[Integers._0] <: Nothing?
      <notype> <: Nothing?
      false
    false
  false
false
two errors found

The <notype> and the Nothing look a bit suspicious ...