Fix treatment of 'this' in MethodLifting

'this' can be of a subtype while MethodLifting.
MethodLifting sometimes needs to insert type casts.

src/main/scala/leon/purescala/MethodLifting.scala

@@ -79,8 +79,8 @@ object MethodLifting extends TransformationPhase {
         val at = acd.typed
         val binder = FreshIdentifier(acd.id.name.toLowerCase, at, true)
         def subst(e: Expr): Expr = e match {
-          case This(`at`) =>
-            Variable(binder)
+          case This(ct) =>
+            asInstOf(Variable(binder), ct)
           case e =>
             e
         }
@@ -158,14 +158,19 @@ object MethodLifting extends TransformationPhase {
         nfd.addFlag(IsMethod(cd))
 
         if (cd.knownDescendants.forall( cd => (cd.methods ++ cd.fields).forall(_.id != fd.id))) {
-          val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
           // Don't need to compose methods
-          nfd.fullBody = postMap {
-            case th@This(ct) if ct.classDef == cd =>
-              Some(receiver.toVariable.setPos(th))
+          val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
+          def thisToReceiver(e: Expr): Option[Expr] = e match {
+            case th@This(ct) => //if ct.classDef == cd =>
+              Some(asInstOf(receiver.toVariable, ct).setPos(th))
             case _ =>
               None
-          }(instantiateType(nfd.fullBody, tparamsMap, paramsMap))
+          }
+          nfd.fullBody = instantiateType(
+            postMap(thisToReceiver)(nfd.fullBody),
+            tparamsMap,
+            paramsMap
+          )
         } else {
           // We need to compose methods of subclasses