do not use underlying type when inferring the type of some (#701)

viperproject · Nov 1, 2023 · 91739fe · 91739fe
1 parent 4c1c3dd
commit 91739fe
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
@@ -262,8 +262,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
     case POptionNone(t) => OptionT(typeSymbType(t))
     case POptionSome(e) =>
       val et = exprType(e)
-      val ut = underlyingType(et)
-      ut match {
+      et match {
         case Single(t) => OptionT(t)
         case t => violation(s"expected a single type, but got $t")
       }