search

titzer / virgil

A fast and lightweight native programming language
1.2k stars 42 forks source link

Add failing tests for ADT type inference #134

Closed k-sareen closed 1 year ago

k-sareen commented 1 year ago

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).

titzer commented 1 year ago

I'll tinker with these tests a bit.

titzer commented 1 year ago

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 commented 1 year ago

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.