Add data type variance to type checking #5960
Conversation
At the moment, no type declarations are variance checked. However, basic variance information is available for lists an immutable arrays. There is a procedure for inferring variance, and the type checking method should work for whatever variance information is provided. Most types will simply have no information available currently, meaning they are treated as invariant.
- Freshen variables in declarations before solving. This avoids accidentally conflating variables from separate separate declarations based on name. - Adjust some defaulting behavior for unknown variables (assume invariant for safety, because the phantom case should be ensured for valid variables via other means).
pchiusano
left a comment
There was a problem hiding this comment.
Nice!!
I think phantom we may want to keep as invariant, unless I am misunderstanding. The reason is we just don't know what the user's intent was.
Like if you exchange a value for a Hashed Nat (a phantom-typed hash), you don't want that to be cast to a Hashed Text automatically. You want to have to take explicit action there.
Ideally we could just have kind annotations but in the absence of that I'm thinking phantom type parameters are treated as invariant. WDYT?
|
Yeah, I was wondering about that myself. As you say, there are uses of phantom types where you don't actually want anything to vary. I can just make phantom things behave as invariant, or map phantoms to invariants for now. |
@dolio yup sounds good to me. |
Use it to fix some compilation errors in new places.
|
I don't really understand the ormolu problem. It seems to be dying on |
I believe this should have already been removed via a merge with trunk, but something about the merge kept it around.
This PR introduces more variance tracking into the type checker. As far as type checking goes, this isn't a huge change. The type checker can be given a collection of variance info for types, and it will be used in the right spot when checking.
The rest is mostly the variance inference for data types, and the plumbing necessary to perform that inference and get the information into the type checker. The inference classifies each parameter of a data type in one of four ways:
T A ~ T Bfor allAandB)T A <= T BwhenA <= B)T A <= T BwhenA >= B)T A = T BwhenA = B)The inference starts with some basic information about wired-in types (like lists), and builds up the information by checking groups of mutually defined data types in dependency order.
The new subtyping possibilities changed how some errors present, so I tried to tweak the error reporting to maintain relatively good messages.