Type checking with associated types is not right

[osa1]

Consider this for statement:

for x in iter: body

The steps to type check this:

1. Generate fresh variables:
   • A for the element type
   • X for the iterator type
2. Add X: Iterator[Item = A] to the predicates.
3. Type check iter expecting type X.
4. Type check body with x : X in the environment.

After step (3), the predicate becomes something like RangeIterator[U32] : Iterator[Item = X], which is fine.

But that doesn't "normalize" X to U32, using the Item type in the impl:

impl[T: Step + Eq] Iterator for RangeIterator[T]:
    type Item = T
    ...

So in the body when we see a use of x we don't have any information on its type X. It doesn't normalize to U32, and it doesn't have predicates.

I think we should be normalizing it to U32 somehow..

[osa1]

Small repro:

fn main() =
    let iter = range(0u32, 10)
    expectU32Item(iter)

fn expectU32Item[X: Iterator[Item = U32]](x: X) = ()

This type checks today because there seems to be some other issue in the type checker, we don't check associated types properly. The following should fail:

fn main() =
    let iter = range(0u32, 10)
    expectI32Item(iter)

fn expectI32Item[X: Iterator[Item = I32]](x: X) = ()

Currently both type check.

[osa1]

Another example:

fn main() = expectI32Elem(123i32)

prim type I32

prim type Str

impl I32:
    prim fn toStr(self): Str

trait Test[T]:
    type Elem

    fn getElem(self): Elem

impl Test for I32:
    type Elem = Str

    fn getElem(self): Str = self.toStr()

fn expectI32Elem[X: Test[Elem = I32]](x: X) = expectStr(x.getElem())

fn expectStr(x: Str) = ()

This can be tested with --typecheck.

[osa1]

One of the issues (among many) here is that the scheme we generate for I32.getElem has Str or Elem return type depending on how we write it.

impl Test for I32:
    type Elem = Str
    fn getElem(self): Str = ...         # return type is `Con(Str)` in the env

impl Test for I32:
    type Elem = Str
    fn getElem(self): Elem = ...         # return type is `Con(Elem)` in the env

In both cases the return type should refer to Self.Elem using the AssocTySelect. We don't have a Self variant in Ty yet, but perhaps we can use the self type in the impl block and represent it as I32.Elem.

In both cases, I think we will also need to restrict associated types to one per implementing type. So with this impl we can't implement another type with an associated type with the same name. It's probably OK for now.

[osa1]

Sigh.. It's still not quite right. New repro:

fn main() = expectU32Item(RangeIterator(current = 0u32, end = 10u32))

fn expectU32Item[I: Iterator[Item = U32]](iter: I) = ()

prim type U32

type Option[T]:
    None
    Some(T)

trait Iterator[T]:
    type Item

    fn next(self): Option[Item]

type RangeIterator[T]:
    current: T
    end: T

impl[T] Iterator for RangeIterator[T]:
    type Item = T

    fn next(self): Option[T] = None

(Run with --no-prelude)

Type error:

tests/AssocTys3.fir:3:1: Associated type RangeIterator[_1].Item ('T) is not U32

The type on the left-hand side should be RangeIterator[U32].Item, which should then normalize to 'T.

[osa1]

Making progress.. Unsurprisingly it's still not right. New repro:

fn main() =
    let box = Box(thing = 123u32)
    let item = getItem(box)
    printStr((item + 456).toStr())

trait GetItem[X]:
    type Item
    fn getItem(self): Item

type Box[T]:
    thing: T

impl[T] GetItem for Box[T]:
    type Item = T
    fn getItem(self): T = self.thing

fn getItem[A, X: GetItem[Item = A]](x: X): A = x.getItem()

prim fn printStr(s: Str)

prim type Str

[osa1]

I'm actually now sure how to make this work. The steps to type check getItem(box):

• Instantiate getItem as Fn(x: _2): _1 (A = _1, X = _2), add _2: GetItem[Item = _1] to the predicates.
• Unify argument types, in this case just _2 ~ Box[U32].
• Since we don't have an expected type in the context (let doesn't have a type annotation), the return type of the instantiated function type is the value of the expr and hence the binding item, which is _1.

Now we have _2: GetItem[Item = _1] in the predicates, and _2 ~ Box[U32], but that doesn't make _1 ~ U32 right now.

It looks like when we have a predicate and the type variable of it is "refined" (i.e. unified with antoher type), we need to use the type of the variable to extract associated types somehow? So we solve Box[U32] ~ GetItem[Item = _1] to have _1 ~ U32.

[osa1]

Probably the best way is that every time we unify a variable with a non-variable, we visit the predicates on the variable, and for associated type predicates we try to "extract" the associated types when possible. When we can't, we carry on as usual.

[osa1]

The thing that's causing this problem is we use the predicates to type check method calls (and probably other things too) and don't add predicates when calling trait methods.

So when we have a + b, we expect a to have __add method, but we don't do this by adding type of a to the predicates as _1: Add, instead we expect it to be in the context already, or a's type should be a concrete type with the method.

For this to work we also need to visit context as we unify things to extract associated types.

I think how this would normally go is: we would keep generating predicates and resolve everything in resolve_preds. In the repro above, that would generate:

• _2 ~ Box[U32] where we also have _2: GetItem[Item = _1], as before.
• When type checking item + 456, we desugar it to item.__add(456), which will generate item ~ typeof(456) using the Add trait definition.
  • Note that we may need a type annotation to the int literal here.

Now at the end of the function we have an empty "givens" (because the function doesn't have a context) and we need to resolve

• _2: GetItem[Item = _1]

where

• _1 ~ U32
• _2 ~ Box[U32]

Which should already work today.

I think this may be the right way to do it, and the reason why I used the predicates when type checking method calls is probably to make some demo/examples work.

I think this should also be more flexible, because a unification done later when checking a list of statements can make a previous statement well-typed, though I can't think of an example right now..

OTOH eagerly resolving predicates might lead to better errors perhaps? (at the cost of rejecting some valid programs)