Should type checker reject this or not?

[PaulKlint]

The type checker rejects the following (based on a test for the recently added function concat):

module experiments::Compiler::Examples::Tst2

// Recently introduced in List.rsc
public list[&T] concat(list[list[&T]] xxs) =
  ([] | it + xs | xs <- xxs);

 value main(list[value] args) = concat([]);

with the following message:

error("Could not instantiate type variables in type fun list[&T \<: value](list[list[&T \<: value]]) with argument types (list[void])",|rascal:///experiments/Compiler/Examples/Tst2.rsc|(189,10,<7,32>,<7,42>))

The interpreter accepts this. I am in favor of following the type checker's choice (and remove this particular test) but just want to have other opinions on this.

[mahills]

Good question. I know why it rejects this -- it definitely can't instantiate &T so it can't figure out the return type -- but logically it should allow an empty list, and returning value would allow any returned type to work. I'm in favor of disallowing this since it can only happen with an explicit empty list being passed (even [ [] ] would work, from what I can tell), but others, like @jurgenvinju. may disagree.

[mahills]

@jurgenvinju that was a big hint to jump into the discussion :)

[jurgenvinju]

Hi @mahills I missed this one while traveling I guess. I'll have a look now.

[jurgenvinju]

@mahills @PaulKlint I need more context to understand why &T can not be bound at the call site. What is the call site? If it's the test in lang::rascal::tests::basic::List which calls accidentally the concat with another type parameter with the same name &T, it should just instantiate the one &T with the other &T right? What am I missing here?

The interpreter does this lazily, so you will see the right instantiation eventually with a concrete void or value depending on the actual contents of the provided lists by the random test value generator.

[PaulKlint]

@jurgenvinju there is a full example at the top of this issue: that is the complete context that exists. The call site is the call([]) occurring in main.

[jurgenvinju]

As for directly answering the question: should the type checker reject this? I think not, because the function is type correct in itself, namely understanding two possible cases:

• it could return list[void] and void is a sub-type of any &T (even if &T would be bound with void)
• it may return elements from list[&T], which are &T, then wrapped in a list again, so the return type list[&T] is exactly fine.

But I see no reason for &T to be bound while checking the body of the function. So there is my confusion with the question. On the call site its another story. See previous comment, where it could be either the random value generator throwing us off because it is pretending to generate static types, or the fact that the type parameters have the same name on the call site and the definition site is messing things up?

[mahills]

Actually, rethinking this, I should add support for this and similar cases. The real reason this doesn't work is simply because the structures don't line up -- you are supposed to pass a list of lists, but are just passing in [], so the type instantiation code can't find how to bind &T. Basically, the only time this will happen is if someone explicitly passes [] to this function.

[jurgenvinju]

@mahills aha, I see. Yes this can only happen in case of empty lists and sets and maps, but it may happen in a nested fashion, like with parametrized data types or something. In this case binding the parameters for which no witness can be found with void should be ok right?

[mahills]

@jurgenvinju right, that's what I'm going to do (hopefully later today)

[jurgenvinju]

@PaulKlint thanks for pointing out the main. That is what I missed and what Mark discussed. Since there is no nesting in the example it is hard to bind the &T. void should be a safe binding in this case though.

[jurgenvinju]

thanks @mahills ! Love it when a plan comes together 👍

[PaulKlint]

Works fine now.