Change the Array/Slice subtyping relationship to a unification-based one

[jfecher]

Problem

When creating a slice users have to explicitly narrow the type to a slice type:

let array = [1, 2, 3];

let slice: [Field] = [1, 2, 3];

This is due to slices being a subtype of arrays and all array literals having an array type.

Happy Case

If we made an array literal's size parameter polymorphic over whether it is a slice or not we would no longer need an explicit type annotation. For review, the current representation is:

type Type {
    ...
    Array { elements: Box<Type>, size: Type }, // size is expected to be a Type::Constant or generic
    Slice { elements: Box<Type> }
}

The proposal is to merge these two cases to something resembling:

type Type {
    ArrayOrSlice { elements: Box<Type>, size: Type }, // expected to be a Type::Constant, MaybeConstant, or generic
    MaybeConstant(u64, TypeVariable),
}

In this scheme an array literal [1, 2] would have the type:

Type::ArrayOrSlice {
    elements: Box::new(Type::Field),
    size: Type::MaybeConstant(2, TypeVariable::Unbound)
}

Then if the array is later used somewhere an array is expected, e.g. fn foo(array: [Field; 2]){ ... }, it will be narrowed to

Type::ArrayOrSlice {
    elements: Box::new(Type::Field),
    size: Type::MaybeConstant(2, TypeVariable::Bound { Type::Constant(2) })
}

Through normal unification. Likewise, if the type is narrowed to a slice, e.g. from foo = foo.push_back(3), the type would instead be narrowed to:

Type::ArrayOrSlice {
    elements: Box::new(Type::Field),
    size: Type::MaybeConstant(2, TypeVariable::Bound { Type::SliceSize }) // where SliceSize is some arbitrary sentinel value
}

Alternatives Considered

Alternatively, we could separate the syntax of arrays and slices. For example, arrays could keep the [1, 2, 3] syntax, and we could give slices a dedicated &[1, 2, 3] syntax where the & is part of the literal.

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response