Uninforming "typing" error for let-definition instead of an expected "syntax" error

[grayswandyr]

In the following model, I made an intentional mistake, typingS.b instead of S.B.

Alloy emits a clear "syntax" error for p1 (The name "b" cannot be found.). as expected.

But if I comment p1 and uncomment p2, I get a totally uninformative error that just says x cannot be typechecked (in the real model I had, it took mea very long time to spot a typo in a long identifier...).

open util/boolean
sig S { B: one Bool }
run p1 { isTrue[S.b] }
//run p2 { let x = S.b | isTrue[x] }

[alcinocunha]

Some errors in let expressions are being correctly reported, for example, in the following command:

run p3 { let x = B.S | isTrue[x] }

It seems that let expressions are being type checked independently of the context they are being used. If that is the case this issue should be easy to fix.

However, I'm not sure that is what we want because context is important for disambiguating overloaded functions and detect irrelevance types, according to the paper that introduced Alloy's type system. For example, the following model also gives the uninformative error (the error was an ambiguity error due to B being overloaded), but actually there is no error if we replace x by B in expression isTrue[S.x] (hence my conclusion that let expressions are being type checked without taking into account the context where they are being used).

open util/boolean
sig S { B: one Bool }
sig T { B: one Bool }
run { let x = B | isTrue[S.x] }

If we want to keep typing the let expressions not taking into account context, then in this example an ambiguity error should have been reported at expression B, and I believe this issue should be an easy fix that could be scheduled for the next release.

If want to start taking context into account then we need to discuss how to report errors in let expressions, such as in the following command, where one usage of x is erroneous and other isn't.

run { let x = B | isTrue[S.x] or some x}

But then we should also discuss if the type system should be reimplemented to properly use the context to detect irrelevance errors as described in the above paper. For example, command run { some (Bool+S).B } does not raise an error and it should because Bool is an irrelevant expression in this context. Since this is a lot of work, for the next minor release I would just keep typing lets as they are currently and just fix the problem with the uninformative errors.