Support for rigid type variables

[xxdavid]

Hi!

I had almost no time to work on the local type inference (#553) in the past months, but I finally found some time last week. After thinking about the implementation, I've decided that a good first step towards LTI would be to add the missing support for rigid type variables. This way we can check bodies of polymorphic functions. And here's a PR just for that.

Rigid type variables are usually treated as type you know nothing about. You cannot assume anything about them and almost no subtyping rules apply to them (except for reflexivity, top, bottom, and any()). When typechecking a function, all of the type variables mentioned in its spec should be considered as rigid, because they can be anything (it is up to the caller what they are instantiated to (in rank-1 polymorphism)).

With this, we can discover type errors like this one:

-spec id(A) -> A.
id(_X) -> 42.

The implementation in this PR tells us that in this case:

The integer on line 2 at column 11 is expected to have type A but it has type 42

When implementing rigid type variables, we have to somehow distinguish between flexible and rigid type variables. I came up with three possible ways of doing so:

1. Adding a new type() shape: {rigid_type, anno(), atom()}
2. Adding a new anno() shape: {is_rigid, boolean()}
3. Keeping the kind (flexible/rigid) of type variables in the current scope in Env

I turned down option number two, as we could not use pattern matching or guards to distinguish between flexible and rigid type variables. Option three could come with a macro guard is_flexible(Var, Env) (which is nice) but would require us to use it in every place where type variables are used in typechecking. This seems quite fragile to me, and thus I went for the option number one. A good thing about this approach is that it required no changes to the typechecking core (subtype, type_check_expr, etc.), only a few utility functions were enriched with a new clause for rigid_var. The only hassle was that erl_pp doesn't expect rigid_var and prints INVALID-FORM in that case, so we have to transform every type before printing it, but this seems okay to me.

I added tests for rigid type variables and I think it works really well. I also moved poly_2 test functions with explanation in the commit message, feel free to react to that as well.

What do you think about it? @erszcz @zuiderkwast

[xxdavid]

Thank you for the review! 🙂

[xxdavid]

Hey guys, could we please move this forward? 🙂 Is there anything left you want to change or comment on?

I've just fixed the authorship of the commits (there was a wrong email address used in them; otherwise the commits are the same) and force-pushed them. I also added one small fixup commit (a103f65).

[xxdavid]

@zuiderkwast I get it. Thank you for merging the PR.

Okay, I'll add a chapter related to Polymorphism to the wiki. I think it can cover both directions: checking the polymorphic functions itself (this involves the rigid type variables) and checking calls to such polymorphic functions (this will hopefully use the LTI approach I described in #553, I will make a PR for that soon). But I am afraid I don't have an edit permission to the wiki.

[zuiderkwast]

@josefs, do you want to give write permissions to @xxdavid in this repo?

He is currently the most active person in this project.

Alternatively, allow everyone to edit the wiki pages by unchecking "Restrict editing to collaborators only" under settings:

Thanks.

[josefs]

@josefs, do you want to give write permissions to @xxdavid in this repo?

Done

[xxdavid]

Thanks!