diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index bb3dd369bb56fe2572bc562847a04aab429c32a0..3370b6ae6f82e7e131277be078eaf824dca72c50 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -234,6 +234,7 @@ trait CodeExtraction extends ASTExtractors {
     }
 
     private var isMethod = Set[Symbol]()
+    private var methodToClass = Map[FunDef, LeonClassDef]()
 
     def extractClassDef(sym: Symbol, args: Seq[(String, Tree)], tmpl: Template): LeonClassDef = {
       val id = FreshIdentifier(sym.name.toString).setPos(sym.pos)
@@ -318,6 +319,7 @@ trait CodeExtraction extends ASTExtractors {
           val fd = defineFunDef(fsym)(defCtx)
 
           isMethod += fsym
+          methodToClass += fd -> cd
 
           cd.registerMethod(fd)
 
@@ -1040,7 +1042,7 @@ trait CodeExtraction extends ASTExtractors {
               IfExpr(r1, r2, r3).setType(lub)
 
             case None =>
-              outOfSubsetError(tr, "Both branches of ifthenelse have incompatible types")
+              outOfSubsetError(tr, "Both branches of ifthenelse have incompatible types ("+r2.getType.asString(ctx)+" and "+r3.getType.asString(ctx)+")")
           }
 
         case ExIsInstanceOf(tt, cc) => {
@@ -1104,10 +1106,11 @@ trait CodeExtraction extends ASTExtractors {
 
             case (IsTyped(rec, ct: ClassType), _, args) if isMethod(sym) =>
               val fd = getFunDef(sym, c.pos)
+              val cd = methodToClass(fd)
 
               val newTps = tps.map(t => extractType(t.tpe))
 
-              MethodInvocation(rec, fd.typed(newTps), args)
+              MethodInvocation(rec, cd, fd.typed(newTps), args)
 
             case (IsTyped(_, SetType(base)), "min", Nil) =>
               SetMin(rrec).setType(base)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 36019967bb663de8aed0a2057bb952181635e048..b5941c2836290d8bc20ee918f36b68fb9b45238f 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -85,7 +85,7 @@ object Extractors {
   object NAryOperator {
     def unapply(expr: Expr) : Option[(Seq[Expr],(Seq[Expr])=>Expr)] = expr match {
       case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPos(fi))))
-      case mi @ MethodInvocation(rec, fd, args) => Some((rec +: args, (as => MethodInvocation(as.head, fd, as.tail).setPos(mi))))
+      case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, (as => MethodInvocation(as.head, cd, tfd, as.tail).setPos(mi))))
       case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
       case And(args) => Some((args, And.apply))
       case Or(args) => Some((args, Or.apply))
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index e828312ba5e5ece266b092fb8909698cbe8d2a38..a09130ee050d485742f07cf943760e67d73fce41 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -68,7 +68,7 @@ object MethodLifting extends TransformationPhase {
             case None =>
               ctx.reporter.fatalError("`this` used out of a method context?!?")
           }
-        case mi @ MethodInvocation(rec, tfd, args) =>
+        case mi @ MethodInvocation(rec, cd, tfd, args) =>
           rec match {
             case IsTyped(rec, ct: ClassType) =>
               Some(FunctionInvocation(mdToFds(tfd.fd).typed(ct.tps ++ tfd.tps), rec +: args).setPos(mi))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index cac99098c04a10ef4eebe4da82124dc2bd48a207..d57b1c58aa5b1206cd027d4e719a8c17b5c84e8a 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -152,7 +152,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
         sb.append(".")
         pp(id, p)
 
-      case MethodInvocation(rec, tfd, args) =>
+      case MethodInvocation(rec, _, tfd, args) =>
         pp(rec, p)
         sb.append(".")
         pp(tfd.id, p)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 5eff8098e4bd7bbf4c65fbe442cf08eea4ccde1b..76f573553f448481b6d396242d592b0665861749 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -65,8 +65,19 @@ object Trees {
     val fixedType = tfd.returnType
   }
 
-  case class MethodInvocation(rec: Expr, tfd: TypedFunDef, args: Seq[Expr]) extends Expr with FixedType {
-    val fixedType = tfd.returnType
+  case class MethodInvocation(rec: Expr, cd: ClassDef, tfd: TypedFunDef, args: Seq[Expr]) extends Expr with FixedType {
+    val fixedType = {
+      // We need ot instanciate the type based on the type of the function as well as receiver
+      val fdret = tfd.returnType
+      val extraMap: Map[TypeParameterDef, TypeTree] = rec.getType match {
+        case ct: ClassType =>
+          (cd.tparams zip ct.tps).toMap  
+        case _ =>
+          Map()
+      }
+
+      instantiateType(fdret, extraMap)
+    }
   }
 
   case class This(ct: ClassType) extends Expr with FixedType with Terminal {