Type checking corner case

[graymalkin]

sig MySig {
  eq: set MySig
}

fact {
  iden in eq
}

This bombs out while generating the CNF. It's probably possible to catch with the type checker, as iden has a larger type than eq.

This is of course easy to fix with

fact { 
    (MySig->MySig & iden) in eq
}

but it took me a few minutes to understand the error.

[aleksandarmilicevic]

What do you mean by "bombs out"? I just ran it and it gave me "no solution", which is expected. The reason why this model is unsatisfiable is because integers are automatically added to the universe, so, as you said, iden is always larger than eq, and hence iden in eq is unsatisfiable.

This model cannot be ruled out by the type checker because the satisfiability of iden in eq depends not only on the types, but also the bounds. For example, if you explicitly remove integers, the model becomes satisfiable:

sig MySig {
  eq: set MySig
}

fact {
  iden in eq
}

run {} for 0 Int

finds:

---INSTANCE---
integers={}
univ={MySig$0}
Int={}
seq/Int={}
String={}
none={}
this/MySig={MySig$0}
this/MySig<:eq={MySig$0->MySig$0}