Simpler region types

[melsman]

Investigate the possibility of not associating type variables with region variables in types.

There are three aspects of the MLKit type system that, when combined, seem to lead to unsoundness.

1. Region variables of type RT-bot
2. Lack of quantification of secondary region and effect variables
3. Unification of auxiliary region and effect variables for datatypes

(See the relevant papers on the region-inference algorithm for an introduction of the above concepts)

The problem is illuminated by issue .

Instead of fixing the problem by making the type system even more complicated (e.g., distinguishing different region variables of type RT-bot), we seek a simpler solution, namely to alter the definition of region types as follows:

tau ::= 'a 
      | ([taus]t, r)              -- t boxed
      | [taus]t                   -- t unboxed
      | (<taus>-e.phi-><taus'>, r)
      | ((taus), r)               -- len taus>1
      | (taus)                    -- len taus<2
taus ::= tau1,...,taun
phi  ::= {ae1,...,aen}
ae   ::= put r | get r | e

(here e denote an effect variable and r denote a region variable)

This change has several consequences:

• Region types become much simpler to explain as they are not cluttered with region variables that have no real runtime consequence. Notice that region variables associated with type variables will never occur in effects, except when gc is enabled and we want to ensure that closures do not contain dangling pointers...
• The change may speed up region inference and the associated representation analyses significantly (e.g., multiplicity inference, physical-size inference, storage-mode analysis) as there are fewer region variables around.
• The region type of a region variable is now known at the time a region variable is created (during spreading).
• Region types RT-bot and RT-word can be eliminated.
• The partial order on region types can be simplified; perhaps we should rename RT-top to RT-other to emphasise that objects are properly categorised according to region types.
• Quite a lot of code will need to change.