Fix #836 (#837)

* add witness of bug

* fix witness of bug

* fix 836

.gitignore

@@ -15,6 +15,7 @@ logger.log
 *.interp
 /gen/
 /.gobra/
+gobra_tmp/
 
 .bloop/
 .metals/

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

@@ -107,7 +107,13 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       }
       predWellDef ++ error(n, "Cannot reveal a predicate access.", n.pred.reveal)
 
-    case PTypeOf(e) => isExpr(e).out
+    case PTypeOf(e) =>
+      val isExp = isExpr(e).out
+      if (isExp.isEmpty) {
+        val typ = underlyingType(exprType(e))
+        error(e, s"typeOf expects an argument of an interface type, but got $e instead.", !typ.isInstanceOf[InterfaceT])
+      } else
+        isExp
     case PTypeExpr(t) => isType(t).out
     case n@ PIsComparable(e) => typOfExprOrType(e) match {
       case t if isInterfaceType(t) => noMessages

src/test/resources/regressions/issues/000836.gobra

@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue836
+
+func test1() {
+	var x int
+	//:: ExpectedOutput(type_error)
+	assert typeOf(x) == type[int]
+}
+
+func test2() {
+	var x interface{} = int(1)
+	assert typeOf(x) == type[int]
+}