diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 0a6633aa4c107a81abbb020683059d55bb441b9f..a5d0deb5d96f641954de045bdb8b4cb9cda85faa 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -526,24 +526,24 @@ trait CodeExtraction extends ASTExtractors { ccd.setFields(fields) - // Validates type parameters - parent foreach { pct => - if(pct.classDef.tparams.size == tparams.size) { - val pcd = pct.classDef - val ptps = pcd.tparams.map(_.tp) + ccd + } - val targetType = AbstractClassType(pcd, ptps) - val fromChild = CaseClassType(ccd, ptps).parent.get + // Validates type parameters + parent foreach { pct => + if(pct.classDef.tparams.size == tparams.size) { + val pcd = pct.classDef + val ptps = pcd.tparams.map(_.tp) - if (fromChild != targetType) { - outOfSubsetError(sym.pos, "Child type should form a simple bijection with parent class type (e.g. C[T1,T2] extends P[T1,T2])") - } - } else { - outOfSubsetError(sym.pos, "Child classes should have the same number of type parameters as their parent") + val targetType = AbstractClassType(pcd, ptps) + val fromChild = cd.typed(ptps).parent.get + + if (fromChild != targetType) { + outOfSubsetError(sym.pos, "Child type should form a simple bijection with parent class type (e.g. C[T1,T2] extends P[T1,T2])") } + } else { + outOfSubsetError(sym.pos, "Child classes should have the same number of type parameters as their parent") } - - ccd } //println(s"Body of $sym")