Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor and improve type checking. #28481

Merged
merged 1 commit into from
Jan 7, 2025
Merged

Refactor and improve type checking. #28481

merged 1 commit into from
Jan 7, 2025

Conversation

mikebenfield
Copy link
Collaborator

@mikebenfield mikebenfield commented Dec 19, 2024

Superfluous contants like ADDRESS_TYPE in checker.rs
are removed, along with some of the assert_*_type methods.

TypeChecker's implementation of ExpressionVisitor
has Output = Type rather than Output = Some(Type),
and its methods return Type::Err on errors rather than None.

Many functions in that implementation have a simpler implementation
with fewer levels of nesting.

Introduced new errors for TypeCheckerError:

type_should_be2 is a replacement for type_should_be
with a better message. Also various _mismatch errors
for operators with incorrectly typed operands.

Introduce equal_user for comparing whether two
types are equal as seen by the user - only difference between
the older eq_flat is it takes into account current
program name when comparing composite types

Display CompositeType with program name if present.

Parse CompositeType without program name if it's not present.

Catch type errors previously not caught:

  • transition call after async function call (this should eventually
    be allowed, but it will require changes to codegen)

  • Abs operand type

  • Binary operation operand type

  • Comparing record types with the same name but different programs

  • Ternary conditional operands not being the same type

(Some of these errors were caught before only in the case that their
visitor received an expected type as addtional input.)

@mikebenfield mikebenfield requested a review from d0cd December 19, 2024 00:37
Error [ETYC0372003]: Expected type `an integer of less than 128 bits or a bool` but type `Foo` was found
--> compiler-test:41:47
|
41 | let q: i32 = Pedersen128::hash_to_i32(Foo { a: 1u32, b: 1u32, });
Copy link
Collaborator

@d0cd d0cd Dec 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should work right, because the size of Foo will be less than 128 bits. This particular instance actually may be too large, but some structs may fit. May be an entirely new feature.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I'm not sure any structs will fit. There's a lot of overhead in the bitwise representation of structs. For each member, its name is encoded as a field. I don't think any struct will be encoded as less than 280 bits.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Identifiers are length-prefixed so for small enough structs, you'd be able to get them to fit.

#[test]
    fn test_size_in_bits() {
        let plaintext = Plaintext::<CurrentNetwork>::from_str("{ x: 1u8 }").unwrap();
        let size_in_bits = plaintext.to_bits_le().len();
        assert_eq!(size_in_bits, 76);
    }

A simpler approach could be to allow structs and arrays, but issue a compiler warning that their may be a runtime failure if the struct or array is too big.
Possibly work for a different PR.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see. In that case maybe yeah I'll leave it to a runtime error.

Error [ETYC0372003]: Expected type `an integer of less than 128 bits or a bool` but type `Foo` was found
--> compiler-test:41:47
|
41 | let q: i64 = Pedersen128::hash_to_i64(Foo { a: 1u32, b: 1u32, });
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this case, Foo exceeds the size of a u64, so it should not be allowed.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't follow. It already is being disallowed, isn't it?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oops, meant it as a follow on thought for the previous comment.
That structs and arrays should in general be allowed, but this one is clearly oversized.

@mikebenfield mikebenfield force-pushed the type-refactor branch 2 times, most recently from 476f366 to a7eaf3c Compare December 20, 2024 21:32
Superfluous contants like `ADDRESS_TYPE` in checker.rs
are removed, along with some of the `assert_*_type` methods.

TypeChecker's implementation of ExpressionVisitor
has `Output = Type` rather than `Output = Some(Type)`,
and its methods return `Type::Err` on errors rather than None.

Many functions in that implementation have a simpler implementation
with fewer levels of nesting.

Introduced new errors for TypeCheckerError:

`type_should_be2` is a replacement for `type_should_be`
with a better message. Also various `_mismatch` errors
for operators with incorrectly typed operands.

Introduce `equal_user` for comparing whether two
types are equal as seen by the user - only difference between
the older eq_flat is it takes into account current
program name when comparing composite types

Display CompositeType with program name if present.

Parse CompositeType without program name if it's not present.

Catch type errors previously not caught:

* transition call after async function call (this should eventually
 be allowed, but it will require changes to codegen)

* Abs operand type

* Binary operation operand type

* Comparing record types with the same name but different programs

* Ternary conditional operands not being the same type

(Some of these errors were caught before only in the case that their
visitor received an expected type as addtional input.)
@mikebenfield mikebenfield marked this pull request as ready for review January 6, 2025 23:20
Copy link
Collaborator

@d0cd d0cd left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Could you add a short blurb in the PR describing what it does, just for completeness?

Good to merge after that!

@mikebenfield
Copy link
Collaborator Author

I've copied the commit message to the PR comment.

@mikebenfield mikebenfield merged commit 71ce020 into mainnet Jan 7, 2025
10 checks passed
@mikebenfield mikebenfield deleted the type-refactor branch January 7, 2025 00:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants