From 91739fed49dede16361590fb9357edceb3d76f64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Wed, 1 Nov 2023 16:07:07 +0100
Subject: [PATCH] do not use underlying type when inferring the type of some
 (#701)

---
 .../info/implementation/typing/ghost/GhostExprTyping.scala     | 3 +--
 1 file changed, 1 insertion(+), 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
index afbcf63e5..9629169a3 100644
--- 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")
       }