Skip to content

Add failing tests for ADT type inference #134

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

Merged
merged 3 commits into from
Feb 20, 2023

Conversation

k-sareen
Copy link
Contributor

No description provided.

@k-sareen
Copy link
Contributor Author

k-sareen commented Feb 18, 2023

As discussed in #131. Some explanations for my reasoning these are type inference bugs:

  1. I would argue that adt_type_infer01.v3 is a type inference bug instead of a syntax bug as it should easily be able to infer that a is of type A<u4> so it should not be complaining about MatchError: match on type A<u4> requires unqualified case. This would also allow deconstructing the case expression like with other ADTs.
  2. adt_type_infer02.v3 complains about TypeError: type "A" expects 1 type arguments and found 0 and MatchError: key of type A<u4> can never match type A.B<?> among other things. Again, it should be able to infer that a is of type A<u4> inside the match statement.
  3. adt_type_infer03.v3 is the closest to what we have to do currently to match an ADT with a type parameter, but it can't infer that A<T>.C and A<U>.C are the same types.
  4. The adt_type_infer04.v3 test is just a combination of adt_type_infer01.v3 and adt_type_infer02.v3.

adt_type_infer0{2,3,4} use the return value from g() in the way we have to do currently. Just added it for sanity that we are using the return value from g() and as a test that this kind of matching should be allowed as well (I also didn't want to generate more errors than required).

@k-sareen k-sareen force-pushed the seman-type-parameter-tests branch from 5809e5d to c9dc595 Compare February 18, 2023 02:40
@titzer titzer merged commit 738aa63 into titzer:master Feb 20, 2023
@titzer
Copy link
Owner

titzer commented Feb 20, 2023

I'll tinker with these tests a bit.

@titzer
Copy link
Owner

titzer commented Feb 20, 2023

As discussed in #131. Some explanations for my reasoning these are type inference bugs:

  1. I would argue that adt_type_infer01.v3 is a type inference bug instead of a syntax bug as it should easily be able to infer that a is of type A<u4> so it should not be complaining about MatchError: match on type A<u4> requires unqualified case. This would also allow deconstructing the case expression like with other ADTs.

The rule is that matching on an ADT either deconstructs, in which case you don't qualify the cases, or it is a type-case, in which you need to write full types. It doesn't currently do unification on the target type of a type-case, maybe it should.

  1. adt_type_infer02.v3 complains about TypeError: type "A" expects 1 type arguments and found 0 and MatchError: key of type A<u4> can never match type A.B<?> among other things. Again, it should be able to infer that a is of type A<u4> inside the match statement.

This is the unification thing above, it can't figure out the type argument. This test had other bugs; the C case cannot be arbitrarily re-used across different instantiations of A.

  1. adt_type_infer03.v3 is the closest to what we have to do currently to match an ADT with a type parameter, but it can't infer that A<T>.C and A<U>.C are the same types.

They aren't the same types. A<T>.C and A<U>.C might be represented completely differently, even if the C case doesn't mention the type parameter.

  1. The adt_type_infer04.v3 test is just a combination of adt_type_infer01.v3 and adt_type_infer02.v3.

adt_type_infer0{2,3,4} use the return value from g() in the way we have to do currently. Just added it for sanity that we are using the return value from g() and as a test that this kind of matching should be allowed as well (I also didn't want to generate more errors than required).

@k-sareen
Copy link
Contributor Author

The rule is that matching on an ADT either deconstructs, in which case you don't qualify the cases, or it is a type-case, in which you need to write full types. It doesn't currently do unification on the target type of a type-case, maybe it should.

I mean it would make it less verbose, so definitely better for developer UX.

This is the unification thing above, it can't figure out the type argument. This test had other bugs; the C case cannot be arbitrarily re-used across different instantiations of A.

Ah right. Interesting. Variants don't get passed by reference, I forgot.

They aren't the same types. A<T>.C and A<U>.C might be represented completely differently, even if the C case doesn't mention the type parameter.

That's fair. I checked with Rust and yeah I must have been misremembering because an equivalent program does not compile in Rust as well.

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