Using a polymorphic type annotation on a record field, as in {id : forall a. a -> a = std.function.id} would unexpectedly fail with a failure to unify forall a. a -> a with a -> a, which indicates that the type annotation wasn't properly instantiated before being used to check the value of the field.
It turns out the typechecking of the field per se is fine, but the issue comes from the recursive environment: in a recursive record, we need to build an environment with the types of all record fields before we can start to actually typecheck each field. When the field isn't annotated, we use a fresh unification variable. When typechecking the corresponding field, we unify what's in the type environment (the unification variable, but which might have been unified with another type at this point) with the type inferred for the field. Doing so, we reject things like {a = true, b = a + 1} : _.
However, when the field has a type annotation, we use this annotation for the recursive environment instead (which is important e.g. to keep polymorphic types...polymorphic). In this case, the additional unification step described above would unify a polymorphic type with the inferred type, which is the place that was missing the instantiation.
One possibility is to just add the missing instantiation, but in fact this unification is useless when there is a type annotation, as the typechecking of the field with a polymorphic annotation will perform the same work anyway (infer a type and check that it's a subtype of the instantiated annotation). We thus rather remember which fields are annotated and we entirely skip the unification in this case.
Closes #1690
Using a polymorphic type annotation on a record field, as in
{id : forall a. a -> a = std.function.id}would unexpectedly fail with a failure to unifyforall a. a -> awitha -> a, which indicates that the type annotation wasn't properly instantiated before being used to check the value of the field.It turns out the typechecking of the field per se is fine, but the issue comes from the recursive environment: in a recursive record, we need to build an environment with the types of all record fields before we can start to actually typecheck each field. When the field isn't annotated, we use a fresh unification variable. When typechecking the corresponding field, we unify what's in the type environment (the unification variable, but which might have been unified with another type at this point) with the type inferred for the field. Doing so, we reject things like
{a = true, b = a + 1} : _.However, when the field has a type annotation, we use this annotation for the recursive environment instead (which is important e.g. to keep polymorphic types...polymorphic). In this case, the additional unification step described above would unify a polymorphic type with the inferred type, which is the place that was missing the instantiation.
One possibility is to just add the missing instantiation, but in fact this unification is useless when there is a type annotation, as the typechecking of the field with a polymorphic annotation will perform the same work anyway (infer a type and check that it's a subtype of the instantiated annotation). We thus rather remember which fields are annotated and we entirely skip the unification in this case.