search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Int and Bool #285

Closed zilinc closed 4 years ago

zilinc commented 5 years ago

Occasionally an integer can be typed as Bool.

For example:

c : Bool
c = 1

typechecks.

I think the root cause is in == and /=, which are polymorphic. The constraint generated is integral alpha, where alpha is the type of the operands.

ajaysusarla commented 5 years ago

But isn't that the way we've actually implemented it? Unlike other types, I always see Bool not represented as a tagged union. I thought it was deliberate.

zilinc commented 5 years ago

It doesn't matter how Bool is implemented. An Int shouldn't be allowed to be typed Bool. It's a bug in the typechecker.