Typechecker bug in the latest build of Alloy

[emina]

Below is an Alloy model that type checks and works as expected in the last stable release but fails to type check in the latest build.

This seems to be a bug in the type checker ...

module list          

one sig Null {}      

sig Str {}              

sig Node {
  data: one Str + Null,  
  next: one Node + Null  
}

sig List {
  head: one Node + Null  
}

one sig This extends List {}

pred Inv[next: Node->(Node + Null) ] {
  no ^next & iden
}

pred Pre[This: List, head:  List->(Node + Null), next: Node->(Node + Null)] {
  This.head != Null &&
  This.head.next != Null
}

pred Post[This: List, oldHead, head:  List->(Node + Null), oldNext, next: Node->(Node + Null)] {
  This.head.*next = This.oldHead.*oldNext && 
  let N = This.oldHead.*oldNext - Null |
   next = oldNext ++ ~(oldNext & N->N) ++
               This.oldHead->Null

}

fun near0[] : Node+Null { This.head }
fun mid0[] : Node+Null { near0.next }
fun far0[] : Node+Null { mid0.next }

fun next0[] : Node->(Node + Null) { next ++ (near0 -> far0) }
pred guard[] { far0 != Null }
fun next1[] : Node->(Node + Null) { next0 ++ (mid0 -> near0) }
fun near1[] : Node+Null { mid0 }
fun mid1[] : Node+Null { far0 }
fun far1[] : Node+Null { far0.next1 }

fun near2[] : Node+Null { guard => near1 else near0 }
fun mid2[] : Node+Null { guard => mid1 else mid0 }
fun far2[] : Node+Null { guard => far1 else far0 }

fun next2[] : Node->(Node + Null) { guard => next1 else next0 }
fun next3[] : Node->(Node + Null) { next2 ++ (mid2 -> near2) }
fun head0[] : List->(Node + Null)  { head ++ (This -> mid2) }

run {
  far2 = Null &&
  Inv[next] && 
  Pre[This, head, next] &&
  !(Inv[next3] && Post[This, head, head0, next, next3])
} for 1 List, 3 Node, 3 Str, 1 Null

[pkriens]

I think this is probably caused by always including util/integer. The optimization was removed because it was often wreaking havoc when you used seq and some other cases.

I'd prefer to keep this an error because I think it is weird that you suddenly get such an error if somewhere suddenly ints are included. If this is not acceptable then we could reinstate the 'use' of int check but now taking into account seq and any other cases. However, I find that quite error prone if you see Int as a standard type. (Which I learned isn't in Alloy.)

It would be nice if we would have a real reference for the language. This feels a uncannily fuzzy for a formal specification tool :-)

[emina]

Yes, this is definitely something for the community to clarify :)

To help us get there, let me make an argument for not automatically importing util/integer---and, more generally, for minimizing implicit features / behaviors in Alloy.

As a user of any language, I expect to be able to freely use all well-formed identifiers that aren't reserved keywords and that don't clash with the names I imported. In this case, the list module should be able to freely use the identifier next because it doesn't clash with anything that is directly imported, and next is not a keyword in Alloy. So, it seems odd / confusing to get a type error that is saying (in a roundabout way) the name next is ambiguous.

That said, I (vaguely) recall the subtleties of the interaction between ints and seq's, so if this is the only way to make everything work, I'll live with it :)

[pkriens]

Yes, I think the seq implies Int. And yes, these clashes are annoying.

I am not sure how much 'integer' we need to include when you only use seq? I think it would be ok if you required to explicitly import util/integer when you start to use integers in anger. This should not be required for equality (e.g. #Foo = 12). Not having next could maybe work then?

I notice during debugging that the sigs automatically contain some seq's? No idea where they come from. In itself, seq is not part of Daniel's book and I do think they need some work.

It is kind of ironic that we have a formal language with a nice tool but no specification ... :-)

[aleksandarmilicevic]

While I wholeheartedly agree with Emina, Peter's persistence on insisting that integers should always be included and treated as built-ins (which implies that all symbols from util/integer must always be imported, essentially making them keywords) has prevailed.

[pkriens]

I am not sure that was my position? I think that # not working because you forget to include integer is a very bad thing to happen. The seq not working correctly, the same. Maybe a solution is to have a base integer type that does not pollute the namespace but still would allow the builtin keywords and operators to function correctly?