Fe type/trait system

[Y-Nak]

• [x] Remove unnecessary Visitor
• [x] Improve error message
• [x] Allow partial application in type alias
• [x] Reports an error for unused type params This is not necessary; need to summarize the reasoning instead.
• [x] Doc work

NOTE: This PR doesn't contain dependent types and function types implementation, please refer to #940

Fe type/trait system

This PR contains Fe v2 type/trait system implementations, which includes

• Internal type/trait representations
• General HKT support
• Trait satisfiability solver

Overview from high-level perspective

Recursive type

We don't allow recursive types if the recursion forms "direct" dependency since it leads to infinite-sized types in our type system. e.g.,

struct Foo {
    // Error!
     f: Foo
}

But this restriction is mitigated by using "indirect" wrapper type, e.g., pointer or reference(NOTE: reference is not implemented in this PR). e.g.,

struct Foo {
    // Ok
    f: *Foo 
}

Generics

struct, enum, function, and trait can be generic, meaning they can have type parameters; also, type parameters can have trait bounds in both a type parameter list and where clause. e.g.,

// NOTE: E and T are intentionally inverted(please consider `Functor` implementation on `Result`).
enum Result<E, T>
where E: Error
{
   Err(E)
   Ok(T)
}

struct S<T: Error> {
    t: T
}

trait Error {}

Higher Kinded Types

In fe v2, we support HKT, which means we can abstract over a type that also abstracts over some type. To specify a HKT, users need to annotate the type parameter with an explicit kind. The type parameter is considered a * type if there is no explicit kind bound. e.g.,

struct I32PtrFamily<P: * -> *> {
   ptr: P<i32>,
}

struct MyPtr<T> {
   t: T
}

struct I32PtrUser {
   ptr: I32PtrFamily<MyPtr>,
}

NOTE: all terms need to be typed to * kind type, e.g.,

struct PtrFamily<P: * -> *> {
    // Error!
    p: P
}

Trait

The trait system in fe is similar to rust, but we don't support associated types yet.

On the contrary, Fe allows for a trait to specify the kind of its type parameters and self type(the type that implements the trait) in addition to a normal trait bound. NOTE: Self appearing in a trait is treated just as a type parameter. e.g.,

trait Add<Rhs, Output> {
     fn add(self, rhs: Rhs) -> Output
}

trait Applicative 
where Self: * -> *
{
     fn pure<T>(t: T) -> Self<T>  
}

Also, it's possible to specify a super trait in the trait definition(NOTE: This is just a syntax sugar for Self: SuperTrait.

trait SubTrait: SuperTrait {}
trait SuperTrait {}

but cyclic trait relationship is not allowed. e.g.,

// Error!
trait Trait1: Trait2 {}
trait Trait2: Trait1 {}

Trait impl

It's the same with the Rust. NOTE: You can implement a trait on a generic type. e.g.,

trait Trait {}
impl<T> Trait for T {}

pub struct S<T: Trait> {
    t: T
}
pub struct S2 {
    // Ok: `Trait` is implemented by `impl<T> Trait for T {}`
    s: S<i32>
}

Trait impl conflict

Conflict happens iff

1. Trait reference in two implementors can be unified
2. Types in two implementors can be unified

e.g.,

pub trait Foo<T> {}

impl Foo<i32> for i32 {}
// No conflict occurs. 
impl Foo<u256> for i32 {}

// Error! Conflict with `impl Foo<i32> for i32 {}`.
// NOTE: this impl doesn't conflict with `impl Foo<u256> for i32 {}`. 
impl<T> Foo<T> for T {}

We don't consider trait bounds in the impl conflict check, so the example below is considered an error.

pub trait Foo<T> {}
impl<T, U> Foo<T> for U 
where 
    T: Clone
    U: Clone
{}
impl<T> Foo<T> for T
{}

Trait Bound Satisfiability

Trait-bound satisfiability check is performed for both type and trait instances.

1. Trait-bound satisfiability for type

   
   trait Trait {}
   impl Trait for i32 {}

pub struct S { t: T }

pub struct S2 { // Ok f: S, // Error! f2: S, }

2. Trait-bound satisfiability for trait instances
```rust
trait Trait<T: Trait2> {}
trait Trait2 {}
impl Trait2 for i32 {}

pub struct S<T>
where T: Trait<i32> + Trait<u256> // Error! `u256` doesn't implement `Trait2`
{}

NOTE: Trait sat solver can use a super trait relationship, so the below example works fine.

pub trait SubTrait: SuperTrait {}
pub trait SuperTrait {}

pub struct S1<T: SuperTrait> {
    t: T
}

pub struct S2<T: SubTrait> {
    t: S1<T> // Ok. the solver can use`SubTrait: SuperTrait`.
}

Type Alias

Type aliases are NOT in the Fe type system, i.e., They are a kind of macro and expanded at the call site. As a result, All generic parameters of a type aliases must be given at the use site. e.g.,

pub enum Result<E, T> {
    Err(E)
    Ok(T)
}

type ErrorCode = u32
type MyResult<T> = Result<ErrorCode, T>
struct Foo {
    res1: MyResult<i32> // Ok
    res2: MyResult // Error!
}

Also, specifying kind bounds is allowed at the type alias definition, but trait bounds are not allowed.

struct S<T: * -> *, U> {
    t: T<U>
}
trait Trait  {}

type Alias<T: * -> *> = S<T, i32> // Ok
type Alias2<T: * -> * +  Trait> = S<T, i32> // Error

Alias to a type that has a higher kind is allowed.

struct S<T> {
    t: T
}
struct Option<T> {}

type Alias = S //  alias to * -> * 

Implementation Note

The design of this PR is greatly inspired by Typing Haskell in Haskell. The main difference is that the PR extended this paper to allow multiple trait parameters.

Type Definitions

All type-related definitions are implemented in hir_analysis::ty::ty_def.

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum TyData {
    TyVar(TyVar),

    TyParam(TyParam),

    TyApp(TyId, TyId),

    TyCon(TyConcrete),

    Invalid(InvalidCause),
}

TyVar represents a free type variable primarily used for type inference and type generalization. For example, when we have a Result<T, E>, generalization lifts it to Result<TyVar<0>, TyVar<1>>. It's important to note that TyParam is not a free type variable. That is, there is no essential difference between TyParam and i32, both are strictly different types, and unification will always fail.

TyCon represents concrete type like i32 or Result.

TyApp represents type application. if you see Result<i32, Option<i32>, then the internal representation for the type is TyApp(TyApp(Result, i32), TyApp(Option, i32)).

Unification

Unification-related types are implemented in hir_analysis::ty::unify. Even though we haven't implemented a type inference, unification plays an important role both for the trait bound satisfiability solver and a trait impl conflict check.

(TBW).

Trait Impl conflict check

Two trait implementation(impl Trait1 for Ty1 and impl Trait1 for Ty2) is considered conflict iff

1. Trait1 and Trait2 can be unified.
2. Ty1 and Ty2 can be unified. NOTE: Before the unifiability check, we need to generalize two impls.

When we check conflicts for 1.impl Trait<i32> for u32

2. impl Trait<T> for T then generalized implementation would be 1'. impl Trait<i32> for u32 2'. impl Trait<TyVar(0)> for TyVar(0)

In the trait unification phase, TyVar(0) is unified to i32. Then, this will lead to a unification error in the implementor type unification phase. As a result, the two implementations do NOT conflict.

(TBW).

Known Issues

HKT-specific SAT problem

It's known that HKT makes it difficult to check trait-bound satisfiability. e.g.,

trait Trait {}
struct S1<T: Trait> {
    t: T
}

struct S2<T: * -> *> {
     t: T<u32>
}

struct S3 {
    t: S2<S1>
}

In this example, the compiler doesn't emit any error. To address this, we need to perform a satisfiability check after monomorphization. But it's impractical. After all, we have two options to address this,

1. Disallow ADT type to specify trait bound
2. Leave it as is

Even if option 2. is selected, safety will not be jeopardized. This is because, either way, it is impossible to create a value with this unsatisfiable (unsat) type. Practically speaking, to create an instance of S2, some constraints on T should be required. For example, T: Applicative like the below one:

impl<T> S2<T> 
where T: * -> * + Applicative
{
    fn new(val: i32) -> Self {
        Self {
            t: T::pure(val)
        }
    }
}

Since S1 cannot implement Applicative due to trait bound limitations on S1, a value of S2<S1> can't exist. But this could become a problem if unsafe cast is allowed in Fe. This is something we need to discuss.

A syntax for type arguments

Since we decided to support HKT, the <> argument list is not perfectly suitable, especially with type aliases. e.g.,

pub struct S1<T, U, V> {
   ...
}

type Foo<T> = S1<T, T>;

pub struct S2 {
    s: Foo<i32, i256>, // This is valid, and resolved to `S1<i32, i32, i256>`.
}

The problem is s: Foo<i32, i256> seems somewhat unnatural. This could be mitigated to a certain extent by allowing to writeFoo<i32><i256>.

MISC

In the current implementation, unused generic parameters are allowed. The context about why rust disallows unused type parameters is described here

I think this might be problematic when we start implementing the borrow checker; either way, we need to decide how to handle this.

[sbillig]

I concur, this is great. I've been writing some fe code and checking out the error messages, and they're pretty nice.

error[6-0003]: trait method type parameter number mismatch
   ┌─ v2.fe:22:8
   │
22 │     fn map<A, B, F: Fn<A, B>>(self: Self<A>, _ f: F) -> Result<E, B> {
   │        ^^^ expected 2 type parameters here, but 3 given

error[6-0006]: given argument label doesn't match the expected label required by trait
   ┌─ v2.fe:22:46
   │
 9 │    fn map<A, B, F: Fn<A, B>>(self: Self<A>, f: F) -> Self<B>
   │                                             ---- argument label is defined here
   ·
22 │     fn map<A, B, F: Fn<A, B>>(self: Self<A>, _ f: F) -> Result<E, B> {
   │                                              ^^^^^^ expected `f` label, but the given label is `_`

[sbillig]

Foo<i32><i256>

I think this syntax would be fine.

What do you think about a "type hole" syntax, for example:

enum Result<T, E> {
    Ok(T)
    Err(E)
}
impl<E> Functor for Result<*, E> { // or Result<_, E> maybe?
    fn map<A, B, F: Fn<A, B>>(self: Self<A>, _ f: F) -> Self<B> {
        match self {
            Result::Ok(a) => {
                return Result::Ok(f(a))
            }
            Result::Err(e) => {
                return Result::Err(e)
            }
        }
    }
}