fir-lang / fir

MIT License
24 stars 3 forks source link

Super trait bounds are not checked #26

Open osa1 opened 3 hours ago

osa1 commented 3 hours ago
prim type U32

prim type Str

prim fn printStr(s: Str)

trait A[T1]:
    fn a(self)

trait B[T2]:
    fn b(self)

type Box[T3]:
    thing: T3

impl[T4: A] B for Box[T4]:
    fn b(self) = printStr("In b")

fn main() =
    Box(thing = 123u32).b()

# args: --typecheck --no-prelude --no-backtrace

In this test, the Box[T].b call should check T: A, but current it doesn't.

The problem is when calling Scheme::subst in select_method: https://github.com/fir-lang/fir/blob/aba5e9178422c8607f2c766282bae71c0838f649/src/type_checker/ty.rs#L306-L326

to substitute quantified types of the method's type with instantiation types we ignore the bounds on the substituted quantified vars.

Fixing this is a bit involved because this is the first time we need to reduce a predicate of syntax <Type> : <Bound> to a set of normal predicates of syntax <Variable> : <Bound>.

osa1 commented 3 hours ago

A common case where this issue will cause problems is in for loops, which require the iterated expression to implement Iterator:

type A:
    x: U32

fn main() =
    for x in range(A(x = 1), A(x = 2)):         # should be type error
        printStr("")

where range is defined as:

fn range[T](start: T, end: T): RangeIterator[T] =
    RangeIterator(current = start, end = end)

type RangeIterator[T]:
    ...

impl[T: Step + Ord] Iterator for RangeIterator[T]:
    ...

Currently we don't check the T: Step + Ord bound and this type checks, and causes a crash in monomorphiser.