diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 24e54b367f982c37a8b0d539c0fa1c40e73f7f47..8e778b4d9fd91c4fdaa9a9302ee3179f76babc04 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -427,9 +427,8 @@ object ExprOps extends GenTreeOps[Expr] {
 
       // Untuple
       case Let(id, Tuple(es), b) =>
-        val tps = es map (_.getType)
-        val ids = tps.zipWithIndex.map {
-          case (tp, ind) => FreshIdentifier(id + (ind + 1).toString, tp, true)
+        val ids = es.zipWithIndex.map { case (e, ind) =>
+          FreshIdentifier(id + (ind + 1).toString, e.getType, true)
         }
         val theMap: Map[Expr, Expr] = es.zip(ids).zipWithIndex.map {
           case ((e, subId), ind) => TupleSelect(Variable(id), ind + 1) -> Variable(subId)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 6620ebb6ad5149742cae3369470c2091776bf9dd..3b9e396b01e3fa5c0353e591aec14ec0d232eb3a 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -823,8 +823,8 @@ object Expressions {
     require(index >= 1)
 
     val getType = tuple.getType match {
-      case TupleType(ts) =>
-        require(index <= ts.size)
+      case tp@TupleType(ts) =>
+        require(index <= ts.size, s"Got index $index for '$tuple' of type '$tp")
         ts(index - 1)
 
       case _ =>
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index e43c882c234d55f68b14b13aff1187fbd6d74b3e..ac28c93cb63879879ef395387277021c550b2eec 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -122,7 +122,7 @@ object TypeOps extends GenTreeOps[TypeTree] {
 
       prefix.lastOption
 
-    case (TupleType(args1), TupleType(args2)) =>
+    case (TupleType(args1), TupleType(args2)) if args1.size == args2.size =>
       val args = (args1 zip args2).map(p => leastUpperBound(p._1, p._2))
       if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
 
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 6518d65fbcec5d365164f2b6213e40f563fb3233..f5976191343c7fe08f3c4b9164c5f2815727c9c3 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -138,7 +138,7 @@ object Types {
     def unapply(t: TypeTree): Option[(Seq[TypeTree], Seq[TypeTree] => TypeTree)] = t match {
       case CaseClassType(ccd, ts) => Some((ts, ts => CaseClassType(ccd, ts)))
       case AbstractClassType(acd, ts) => Some((ts, ts => AbstractClassType(acd, ts)))
-      case TupleType(ts) => Some((ts, Constructors.tupleTypeWrap _))
+      case TupleType(ts) => Some((ts, TupleType))
       case ArrayType(t) => Some((Seq(t), ts => ArrayType(ts.head)))
       case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
       case BagType(t) => Some((Seq(t), ts => BagType(ts.head)))