Fix type-checker crash when encountering an invalid ADT (#897)

* adds bug witness

* fixes crash in the type-checker when typing a match expression for an ADT that has type UnknownType

Author: ArquintL

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

@@ -9,7 +9,7 @@ package viper.gobra.frontend.info.implementation.typing.ghost
 import org.bitbucket.inkytonik.kiama.util.Messaging.noMessages
 import viper.gobra.ast.frontend.{PExpression, PFieldDecl, PIdnNode, PMatchAdt}
 import viper.gobra.frontend.info.base.SymbolTable.{AdtClause, AdtDestructor, AdtDiscriminator, BoundVariable, BuiltInFPredicate, BuiltInMPredicate, DomainFunction, GhostRegular, MatchVariable, Predicate}
-import viper.gobra.frontend.info.base.Type.{AdtClauseT, AssertionT, FunctionT, Type}
+import viper.gobra.frontend.info.base.Type.{AdtClauseT, AssertionT, FunctionT, Type, UnknownType}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.util.Violation.violation
 
@@ -46,8 +46,13 @@ trait GhostIdTyping { this: TypeInfoImpl =>
 
     case MatchVariable(decl, p, context) => p match {
       case PMatchAdt(clause, fields) =>
-        val clauseT = context.symbType(clause).asInstanceOf[AdtClauseT]
-        clauseT.typeAt(fields.indexOf(decl))
+        val clauseT = context.symbType(clause)
+        clauseT match {
+          case clauseT: AdtClauseT => clauseT.typeAt(fields.indexOf(decl))
+          // the following case is possible, e.g., if the clause is not well-defined
+          // and, thus, `clauseT` is `UnknownType`:
+          case _ => UnknownType
+        }
 
       case e: PExpression => context.typ(e)
       case _ => violation("untypeable")

src/test/resources/regressions/features/adts/match-error1.gobra

@@ -0,0 +1,29 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package matcherror1
+
+// this test case checks that Gobra does not crash when
+// typing a match expression if the corresponding ADT type
+// is not well-defined.
+
+ghost type Trace adt {
+    RootEntry{}
+    SendEntry{
+        //:: ExpectedOutput(type_error)
+        msg InexistentType // unknown identifier
+        prev Trace
+    }
+}
+
+ghost
+decreases _ // assume termination instead of using `len(t)`, which would cause another type error
+ensures   0 <= res
+pure func (t Trace) length() (res int) {
+    return match t {
+        case RootEntry{}: 0
+        // we need a recursive call to trigger the error in a previous version of Gobra
+        //:: ExpectedOutput(type_error)
+        case SendEntry{_, ?p}: 1 + p.length() // `length` is an unknown identifier as `Trace` is malformed
+    }
+}