Support for Ghost Types

[ArquintL]

This PR adds support for Ghost Types, i.e., the ability to mark a named type or type alias as ghost such that this type is erased. This feature came up in the context of structs that are declared for verification-only purposes and, thus, contain only ghost fields.

In addition, this PR makes PPermissionType and PPredType ghost types, which did not use to be the case.

[jcp19]

Oh, cool!

Do I see it correctly that, for two instances x and y of ghost struct type T (containing at least one field), x == y will always yield true? If so, maybe we can change the encoding such that it matches === in those cases.

[Felalolf]

I only have one minor comment, the rest seems fine.

[ArquintL]

I'm not the biggest fan of special casing the encoding for ghost structs as this seems rather confusing to users. Instead, I've implemented a type checker warning for this case in the separate PR #826

[jcp19]

I'm not the biggest fan of special casing the encoding for ghost structs as this seems rather confusing to users. Instead, I've implemented a type checker warning for this case in the separate PR #826

Hmm, in that case, I would rather throw a type error rather than a warning, given that == between ghost structs becomes rather useless. In fact, I think that the current solution introduces a special case - so far, for all ghost types, == matches ===. With the introduction of ghost structs, this will no longer be the case.

The way I see it, ghost structs are useful as alternatives to ADT with a single constructor. However, for ADTs we do have a meaningful ==, whereas for ghost structs, we can only resort to ===.

EDIT: To add to this, I had two instances where I was bitten by the unexpected semantics for ==, one in a first attempt while trying out these changes in scion (I changed some types to be ghost structs instead of adts and, without noticing, some of my specs became vacuously true), and one instance with my student who was verifying the go standard library stated a lemma that was also vacuously true without noticing. If you really insist on keeping these semantics for equality, then I think that reporting anything less than a type error here is way too dangerous.

[ArquintL]

I agree with your statement that ghost types use == like ===. My fear is related to the different semantics between a ghost struct and a struct with just ghost fields, which feels like very similar things to me, but maybe I'm wrong here and we should indeed have == mean different things for ghost structs and structs with just ghost fields

[ArquintL]

@jcp19 I've now implemented equality (==) for ghost structs to match ===. Could you take a look at the most recent commit? In particular, I have the impression that type equality for StructT was missing some checks, namely that the fields have the same names. Is this correct?