Type variable quantification for record functions (and record constructors?)

[AshleyYakeley]

• split off from Existential types in record constructors #172

Record Functions

Should be able to identify certain type variables in record functions. For example:

# implicit type form (matching var from sig) (disallow?)
f1: Maybe t of
    m: a -> (a *: t);
    end = ...;

# explicit type form (quantified)
f1: Maybe t of
    type t;
    m: a -> (a *: t);
    end = ...;

# explicit type form
f2: Integer -> Text -> Text of
    type t;
    m: Text -> t -> (t *: Text);
    end = ...;

# no quantified type
f3: Integer -> Text -> Text of
    m: Text -> t -> (t *: Text);
    end = ...;

Equivalent types:

• fn m => f1 : forall t. (forall a. a -> (a *: t)) -> Maybe t
• fn m => f2 : forall t. (Text -> t -> (t *: Text)) -> Integer -> Text -> Text
• fn m => f3 : (forall t. Text -> t -> (t *: Text)) -> Integer -> Text -> Text

Record Constructors

# implicit type form (already, matching var from sig)
datatype R1 +t of
    Mk of
        m: a -> (a *: t);
    end;
end;

# explicit type form (disallow?)
datatype R1 +t of
    Mk of
        type t;
        m: a -> (a *: t);
    end;
end;

# explicit type form
datatype R2 of
    Mk of
        type t;
        m: Text -> t -> (t *: Text);
    end;
end;

# no quantified type
datatype R3 of
    Mk of
        m: Text -> t -> (t *: Text);
    end;
end;

Equivalent types:

• fn m => Mk.R1 : forall t. (forall a. a -> (a *: t)) -> R1 t
• fn m => Mk.R2 : forall t. (Text -> t -> (t *: Text)) -> R2
• fn m => Mk.R3 : (forall t. Text -> t -> (t *: Text)) -> R3

Matching:

• fn Mk.R1 => m : forall t. R1 t -> (forall a. a -> (a *: t))
• fn Mk.R2 => m bad, type escape
• fn Mk.R3 => m : R3 -> (forall t. Text -> t -> (t *: Text))

[AshleyYakeley]

To do:

• record functions: move sig before of..end
• record functions: connect type variable to sig (already done for record constructors)
• record functions: add type
• record constructors: add type, check for type escape when matching