Super trait bounds are not checked

[osa1]

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:

fir/src/type_checker/ty.rs

Lines 306 to 326 in aba5e91

	/// Substitute `ty` for quantified `var` in `self`.
	pub(super) fn subst(&self, var: &Id, ty: &Ty, _loc: &ast::Loc) -> Scheme {
	// TODO: This is a bit hacky.. In top-level functions `var` should be in `quantified_vars`,
	// but in associated functions and trait methods it can also be a type parameter of the
	// trait/type. For now we use the same subst method for both.
	debug_assert!(self
	.quantified_vars
	.iter()
	.any(|(var_, _bounds)| var_ == var));
	Scheme {
	quantified_vars: self
	.quantified_vars
	.iter()
	.filter(|(var_, _bounds)| var_ != var)
	.cloned()
	.collect(),
	ty: self.ty.subst(var, ty),
	loc: self.loc.clone(),
	}
	}

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]

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.

[osa1]

Currently if I have a quantified varible like

fn id[T](a: T): T = a

When checking the function body, I represent T as a type constructor with no constructors.

(The bounds are collected in a "context" that we don't use when type checking the body. The context is only used when resolving the predicates collected while checking the body.)

I think this is mostly fine, but I'm wondering if it's better in any way to represent these quantified variables as their own variant.

More concretely, in #26 we will have to "reduce" predicates of form <Type> : <Bound> to a set of predicates of form <Var> : <Bound>.

In this reduction, if we see a bound like T : MyTrait, we may want to check whether T is a type constructor or a type parameter.

• If type parameter: then the bound needs to be in the context.

  (We currently don't pass context around when checking bodies, we probably should.)

• If type constructor: the type should be implementing the trait, which we can check by looking at the implementing types of the trait in PgmTypes.

  (Note: current we don't allow a polymorphic type to implement a trait multiple times with different type parameters, so this is easy.)

If we treat both the same, and starting passing context around, then for a type like T we have to check both the context and global type state to see if satisfy the bounds.

It's fine as long as we check the context first and then the global type state, but if we had two different variants we would look one or the other depending on the variant.

[osa1]

If we treat both the same, and starting passing context around, then for a type like T we have to check both the context and global type state to see if satisfy the bounds.

It's fine as long as we check the context first and then the global type state, but if we had two different variants we would look one or the other depending on the variant.

To clarify, the reason why we need to pass conetxt around is that the predicate set type (PredSet) only allows adding predicates to unification variables.

So I can't add predicates to T in fn a[T](t: T) = <HERE> and then check that the predicates hold in check_fun or similar.