adds another testcase and attempts to fix unit tests

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GhostTyping.scala

@@ -184,7 +184,7 @@ trait GhostTyping extends GhostClassifier { this: TypeInfoImpl =>
         case sp: ap.Symbolic => sp.symb.ghost
         case ap.PointerType(base) => isTypeGhost(base)
       }
-      case _ => Violation.violation(s"expected a type but got $t")
+      case _ => false
     }
   }
 

src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala

@@ -315,6 +315,30 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
     frontend.testProg(input, expected)
   }
 
+  test("Ghost Erasure: ghost types should be erased") {
+    val input =
+      s"""
+         |package pkg
+         |type Struct struct {
+         |    f int
+         |    ghost g int
+         |}
+         |ghost type GhostStruct struct {
+         |    f int
+         |}
+         |ghost type GhostIntDef int
+         |ghost type GhostIntAlias = int
+         |""".stripMargin
+    val expected =
+      s"""
+         |package pkg
+         |type Struct struct {
+         |    f int
+         |}
+         |""".stripMargin
+    frontend.testProg(input, expected)
+  }
+
   /* ** Stubs, mocks, and other test setup  */
 
   class TestFrontend {