Dafny's occurs-check for type synonyms can be tricked

[plaidfinch]

Dafny will correctly rule out the following bad type synonyms; they're equi-recursive, and should not be permitted:

type Bad = set<Bad>
type Bad = (Bad, Bad)
type Bad = map<Bad, Bad>

However, Dafny seems not to detect cycles deeper than one level of nesting; the following type synonyms are all accepted:

type Bad = set<set<Bad>>
type Bad = seq<(Bad, Bad)>
type Bad = map<int, set<Bad>>

...and so on.

Any of these will cause a fatal crash in the Dafny verification process whenever Bad is mentioned. For instance, any of the above type synonyms, when paired with the below definition, crash Dafny:

predicate UhOh(bad: Bad)

It seems that the syntactic occurs check only looks one level deep; it should recursively descend the structure of the type.