Failure to resolve free variables from a method's block return type

[caspiano]

The compiler should be able to solve free variables from the return type of a block in cases where the type of other variables can only be deduced from the return type of the block.

• Failure to solve block argument-free variable.

class Foo(T)
  def method(&block : U, T -> U) forall U
    yield U.zero, T.zero
  end
end

Foo(Int32).new.method do |zero, foo|
  puts zero, foo
  Float64.zero
end

Output:

In type_error_0.cr:7:16

 7 | Foo(Int32).new.method do |zero, foo|
                    ^-----
Error: instantiating 'Foo(Int32)#method()'


In type_error_0.cr:2:23

 2 | def method(&block : U, T -> U) forall U
                         ^
Error: undefined constant U

* Failure to solve optional method argument free variable that is not explicitly passed at the call site.

def method(a : U? = nil, &block : U -> U) forall U
  yield a if a
end

method do |foo|
  foo + "hello"
end

Output:

In type_error_1.cr:5:1

 5 | method do |foo|
     ^-----
Error: instantiating 'method()'


In type_error_1.cr:1:35

 1 | def method(a : U? = nil, &block : U -> U) forall U
                                       ^
Error: undefined constant U

[HertzDevil]

1. I don't think Float64.zero in the block should be used to infer the zero parameter's type even if it is doable.
2. Probably duplicate of Type inference and generics when dealing with default nil #2456

[caspiano]

One may want to use a class method on a type var before it is solved later by the block, I think it's unexpected that it can't be resolved

[beta-ziliani]

What's sure is that the error can be improved. It's confusing to call a type variable a constant.

[asterite]

The way the compiler works is like this... if you have a block that says &block : T -> U then:

• The compiler will first check what's the type of T
• With that type it will "instantiate" the given block assuming the first argument has type T (which is now known to the compiler)
• With that, the compiler can figure out the type of the block
• Then it assigns that type to U and finally proceeds to type the actual method that has the block argument, because now U is known

For example Enumerable#map is defined like this:

  def map(& : T -> U) : Array(U) forall U
    ary = [] of U
    each { |e| ary << yield e }
    ary
  end

So given [1, 2, 3].map { |x| x.to_s } (well, Array overrides this method, but let's say it doesn't) then:

• T gets the type Int32, from Array(Int32) including Enumerable(Int32)
• So x gets the type Int32
• Then x.to_s has the type String
• So U gets the type String
• And so [] of U is actually typed as [] of String

Now let's see the first snippet in this issue:

class Foo(T)
  def method(&block : U, T -> U) forall U
    yield U.zero, T.zero
  end
end

Foo(Int32).new.method do |zero, foo|
  puts zero, foo
  Float64.zero
end

Let's try to do the same:

• First we'll type U... Oops! We don't know U. Failure.

I... I don't think this can be implemented.

But let's try it. We have to start by typing something, right? Otherwise it's impossible.

Let's try typing the block (do |zero, foo|). Can we type it? Well, we don't know what are the types of zero and foo, so we can't type it.

Let's try typing the method. It says yield U.zero. But we don't know what's the type of U!

I think you are expecting the compiler to somehow only type Float64.zero, skipping the previous puts line, and then to know that that's U. Then with that we can type the method and then the block.

For this to work the logic of how blocks are typed needs to use bindings, like everywhere else... but that's a bit tricky to implement. In fact I think we didn't do that because there was a blocker I can't remember now.

All of this to say: it's not gonna happen soon, and it might never happen.

[caspiano]

I could grok a bit of that from the semantic visit of Call node and your answer has made it crystal clear. Cheers @asterite 🙂

[asterite]

All of this to say: it's not gonna happen soon, and it might never happen.

I think I shouldn't say these things, so I'll never again. What I meant is that I won't do that, but someone might, I don't know.