typeck should safe-guard against types with un-substituted formals

[pnkfelix]

Spawned off of #5121.

Part of the bug underlying #5121 lay dormant for quite a while because some of the type-checking machinery is not as aggressive as it could be about ensuring that the types it is checking actually correspond to concrete types.

In particular, in a concrete function type, the bound-type/lifetimes (i.e. the "formals" in P.L. speak) from the function's signature have been replaced with other concrete types (i.e. the "actuals").

Currently, the ty represetnation does not really distinguish between formals and actuals except for lifetimes. But nonetheless, we can at least safe-guard against this problem in that case (and presumably if we later change ty to between distinguish between formal/actual for type variables as well, then similar checks would go into the same place, probably).

[nikomatsakis]

The way I had planned to solve this is to use distinct types for "types that may contain inference values" and "types that do not". I actually had a branch of rustc a couple of years back building that did precisely this. The basic idea is to parameter ty::sty with a type parameter that is the type for "reference to another type". Then we pull out all the inference types into a distinct enum that wraps the base enum:

enum sty<T> { ty_tup(~[T]), ... } 
struct normal_type { ... sty<normal_type> ... }
struct inference_type { ... sty<inference_type> ... }

This way, the types of an ast item are distinct from those used during inference. You can write folders and so on generically over T (in fact, lacking default methods, this was INCREDIBLY PAINFUL which is part of the reason I never tried to land the branch, but it should be easier now).

You can see some of the groundwork from this branch still:

• function contexts have their own distinct tables for types
• the core folder is written as a trait with default methods

But one of the challenges I remember was having to find the right canonicalization scheme. I just didn't canonicalize during inference but instead allocated fresh @ty everywhere. This was slow. I suspect using an arena per function would be the right answer here.

[reem]

Triage: I'm not familiar with the relevant internals here and #5121 is closed, so I'm not sure what is still left to do here.

[nikomatsakis]

Nothing has really changed. Still a sort of "nice to have" refactoring though I think, most likely, we'd want to just roll this into whatever "next generation" design we come up with for type checking.

[steveklabnik]

Triage: no idea if this has changed in the last year.

[brson]

@pnkfelix @nikomatsakis is this valuable to have open?

[nikomatsakis]

I think we can close this.