Type unification error in forperm

[superaxander]

While attempting to replicate a VerCors issue I ran into this Viper crash (running with Silicon on the master branch):

java.lang.RuntimeException: type unification error - should report and not crash
	at scala.sys.package$.error(package.scala:27)
	at viper.silver.parser.Translator.expInternal(Translator.scala:503)
	at viper.silver.parser.Translator.exp(Translator.scala:351)
	at viper.silver.parser.Translator.expInternal(Translator.scala:480)
	at viper.silver.parser.Translator.exp(Translator.scala:351)
	at viper.silver.parser.Translator.expInternal(Translator.scala:541)
	at viper.silver.parser.Translator.exp(Translator.scala:351)
	at viper.silver.parser.Translator.expInternal(Translator.scala:468)
	at viper.silver.parser.Translator.exp(Translator.scala:351)
	at viper.silver.parser.Translator.$anonfun$translate$22(Translator.scala:85)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at viper.silver.parser.Translator.translate(Translator.scala:85)
	at viper.silver.parser.Translator.$anonfun$translate$16(Translator.scala:58)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at viper.silver.parser.Translator.translate(Translator.scala:58)
	at viper.silver.frontend.SilFrontend.doTranslation(SilFrontend.scala:362)
	at viper.silver.frontend.SilFrontend.doTranslation$(SilFrontend.scala:356)
	at viper.silicon.SiliconFrontend.doTranslation(Silicon.scala:319)
	at viper.silicon.SiliconFrontend.doTranslation(Silicon.scala:319)
	at viper.silver.frontend.DefaultFrontend.translation(Frontend.scala:250)
	at viper.silver.frontend.DefaultFrontend.translation$(Frontend.scala:248)
	at viper.silicon.SiliconFrontend.translation(Silicon.scala:319)
	at viper.silver.frontend.DefaultPhases.$anonfun$Translation$1(Frontend.scala:115)
	at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1(Frontend.scala:62)
	at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted(Frontend.scala:60)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at viper.silver.frontend.Frontend.runAllPhases(Frontend.scala:60)
	at viper.silver.frontend.Frontend.runAllPhases$(Frontend.scala:59)
	at viper.silicon.SiliconFrontend.runAllPhases(Silicon.scala:319)
	at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:208)
	at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:182)
	at viper.silicon.SiliconFrontend.execute(Silicon.scala:319)
	at viper.silicon.SiliconRunnerInstance.runMain(Silicon.scala:392)
	at viper.silicon.SiliconRunner$.main(Silicon.scala:380)
	at viper.silicon.SiliconRunner.main(Silicon.scala)

I've created a minimised example file:

domain Pointer[]  {
}

domain F  {
  function foo(bar: F): Ref
}

field int: Int
field f: F

function ptrDeref(p: Pointer[]): Ref

method baz()
  ensures [true, (forperm this: Pointer[] [foo(ptrDeref(this).f).int] :: false)]

Note that I had to use the [] after Pointer to avoid a parsing error.

I would expect to get some error that explains that using forperm like this is not allowed, instead of a crash. A different version without the F domain gave me the error "Quantified arguments can only be used directly" which I guess would be the error to expect here too.