Restrict usages of type variables in non-generalized contexts

Type variables can only be used on functions (and in number literals as
a carve-out for now). In all other cases, a type variable takes on a
single, concrete type based on later usages. This check emits errors
when this is violated.

The implementation is to check the rank of a variable after it could be
generalized. If the variable is not generalized but annotated as a type
variable, emit an error.
This commit is contained in:
Ayaz Hafiz 2025-01-02 14:26:37 -06:00
parent f5961cbb22
commit a0461679dd
13 changed files with 230 additions and 114 deletions

View file

@ -95,22 +95,6 @@ flags! {
/// Prints all type variables entered for fixpoint-fixing.
ROC_PRINT_FIXPOINT_FIXING
/// Verifies that after let-generalization of a def, any rigid variables in the type annotation
/// of the def are indeed generalized.
///
/// Note that rigids need not always be generalized in a def. For example, they may be
/// constrained by a type from a lower rank, as `b` is in the following def:
///
/// F a : { foo : a }
/// foo = \arg ->
/// x : F b
/// x = arg
/// x.foo
///
/// Instead, this flag is useful for checking that in general, introduction is correct, when
/// chainging how defs are constrained.
ROC_VERIFY_RIGID_LET_GENERALIZED
/// Verifies that an `occurs` check indeed only contains non-recursive types that need to be
/// fixed-up with one new recursion variable.
///