diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index f64c0521985846e8a8ff17f2c83d64ac34e4b7f4..4b458b5d8cbd041f0e59879a8b1e82624e24a3f4 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -319,6 +319,9 @@ object TypeOps {
           case Error(tpe, desc) =>
             Error(tpeSub(tpe), desc).copiedFrom(e)
           
+          case Hole(tpe, alts) =>
+            Hole(tpeSub(tpe), alts.map(srec)).copiedFrom(e)
+
           case g @ GenericValue(tpar, id) =>
             tpeSub(tpar) match {
               case newTpar : TypeParameter => 
diff --git a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
index 57f37ed34792070df06a704f1d1d2e074691959f..c7ce03cf7e6a9ba856f6ffd462e0e390b2ca59b7 100644
--- a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
@@ -61,4 +61,19 @@ class TypeOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
     assert(isSubtypeOf(listD.typed, listD.typed), "List[T] <: List[T]")
   }
 
+  test("instantiateType Hole") { ctx =>
+    val tp1 = TypeParameter.fresh("a")
+    val tp2 = TypeParameter.fresh("b")
+
+    val tpd = TypeParameterDef(tp1)
+
+    val e1 = Hole(tp1, Nil)
+    val e2 = instantiateType(e1, Map(tpd -> tp2), Map())
+
+    e2 match {
+      case Hole(tp, _) => assert(tp == tp2, "Type should have been substituted")
+      case _ => fail("Incorrect expr shape, should be a Hole")
+    }
+  }
+
 }