viperproject/silver

Generic domain function application needs trivial type variable map with uninsightful error message

nilscrm opened this issue · 0 comments

If one wants to create a simple generic domain to represent an option type, one could use this (simplified) example:

domain Option[T]  {

  function none_val(): Option[T]

  function some_of(x: T): Option[T]

  axiom {
    (forall x: T :: { some_of(x) } some_of(x) != none_val())
  }
}

This works perfectly fine in VS Code, however, when one want to implement this in Silver, troubles can occur.
The generic function call some_of(x) can be modeled as

vpr.DomainFuncApp(someOf, Seq(vpr.LocalVar("x", T)()), Map.empty)()

This code, however, throws an exception:

java.lang.Exception: Internal error in type system - unexpected non-ground type <T>

It is non-obvious from this error that the actual problem is the empty type variable map. Even in the generic case where you want to keep the generic type T a type variable map from T to T needs to be specified like this:

vpr.DomainFuncApp(someOf, Seq(vpr.LocalVar("x", T)()), Map(T -> T))()

Two possible solution might be to either have a default value for the type variable map or to make the error message clearer.