Type of \type, \typeof expressions is inconsistently integer in PVL

[wandernauta]

The \type and \typeof operators return a type<...> value according to some (early) passes, but an integer according to the (later) classToRef pass, leading to confusing type errors or crashes.

This PVL program causes VerCors to crash with an internal type error ("Expected type<ref>, but got int"):

class A {
}

type<A> foo() {
   return \type(A);
}

[52.5%] VerCors › Transformation › encodeByValueClassUsageInternal type error: CoercionErrors must not bubble. Expression `1` could not be coerced to `type``
[INFO] Done: VerCors (at 18:55:23, duration: 00:00:03)
vct.main.stages.Transformation$TransformationCheckError: The classToRef rewrite caused the AST to no longer typecheck:
======================================
16     type flatten;
   17     exc = null;
                   [-
   18     flatten = 1;
                    -]
   19     return1 = flatten;
   20     flatten;
--------------------------------------
[1/1] Expected the type of this expression to be `type<ref>`, but got int.
======================================
	at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:254)
	at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:233)
	at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:25)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166)
	at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:25)
	at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:24)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
	at hre.progress.Progress$.foreach(Progress.scala:24)
	at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:233)
	at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:32)
	at vct.main.stages.Transformation.run(Transformation.scala:227)
	at vct.main.stages.Transformation.run(Transformation.scala:200)
	at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
	at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
	at hre.stages.Stages.$anonfun$run$1(Stages.scala:101)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at hre.stages.Stages.run(Stages.scala:98)
	at hre.stages.Stages.run$(Stages.scala:95)
	at hre.stages.StagesPair.run(Stages.scala:145)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64)
	at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.util.Time$.logTime(Time.scala:23)
	at vct.main.modes.Verify$.runOptions(Verify.scala:99)
	at vct.main.Main$.runMode(Main.scala:107)
	at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.io.Watch$.booleanWithWatch(Watch.scala:58)
	at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.runOptions(Main.scala:95)
	at vct.main.Main$.main(Main.scala:50)
	at vct.main.Main.main(Main.scala)
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!
[ERROR] ! VerCors has crashed !
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!

The following PVL program verifies, so the "real" type of these expressions seems to indeed be an integer:

class A {
}

void foo() {
    assert \type(A) == 1;
}

[INFO] Verification completed successfully.

However, type checks in earlier passes reject the fix that the error message seems to suggest ("Expected the type of this expression to be int, but got type<A_1234>"):

class A {
}

int foo() {
   return \type(A);
}

======================================
At /home/wander/IdeaProjects/vercors/examples/concepts/basic/example.pvl
--------------------------------------
    3  
    4  int foo() {
                 [--------
    5      return \type(A);
                  --------]
    6  }
    7
--------------------------------------
[1/1] Expected the type of this expression to be `int`, but got type<A_409144295>.
======================================

Version: 3313255 (dev branch).

This issue was found by fuzzing.