Crystal: Error combining `if var` with proc declaration

[chocolateboy]

Crystal: 0.22.0 (2017-04-22) LLVM 4.0.0
OS: Linux (Arch)

The following code prints out the expected types and value:

test1.cr

def get_value
  ["Foo", nil][0]
end

value = get_value
puts typeof(value)

if value
  puts typeof(value)
  puts value.size # OK: 3
end

Output

(String | Nil)
String
3

However, if a proc which closes over the type-narrowed value is declared in the then branch, it breaks the type narrowing:

test2.cr

def get_value
  ["Foo", nil][0]
end

value = get_value
puts typeof(value)

if value
  puts typeof(value)
  puts value.size # OK: 3
  proc = ->() { puts value.size }
  proc.call
end

Error

Error in test.cr:10: undefined method 'size' for Nil (compile-time type is (String | Nil))

  puts value.size # OK: 3
             ^~~~

It works fine if the value is removed from the proc:

test3.cr

def get_value
  ["Foo", nil][0]
end

value = get_value
puts typeof(value) #=> (String | Nil)

if value
  puts typeof(value) #=> String
  puts value.size # OK: 3
  proc = ->() { puts 42 }
  proc.call
end

Output

(String | Nil)
String
3
42

It also works if the proc declaration is moved out of the then branch:

test4.cr

def get_value
  ["Foo", nil][0]
end

def get_proc(value)
  ->() { puts value.size }
end

value = get_value
puts typeof(value)

if value
  puts typeof(value)
  puts value.size # OK: 3
  proc = get_proc(value)
  proc.call
end

Output

(String | Nil)
String
3
3

[mverzilli]

Nice catch! Thanks

[bcardiff]

In the test4.cr I was expecting to see something like

def get_value
  ["Foo", nil][0]
end

value = get_value
proc = ->{ puts value.size }
puts typeof(value)

if value
  puts typeof(value)
  puts value.size # OK: 3
  proc.call
end

Which also complains

... undefined method 'size' for Nil (compile-time type is (String | Nil))

proc = ->{ puts value.size }

The reason is that if a variable is captured in a proc (leading to a closure), it's value could be changed from the proc. So we can't guarantee the type filter will hold, because the proc could be called in any moment. In your examples the code is linear and for a human is trivial. But the compiler does not track when a proc can be called. It's just the existence of a closure over a variable that abort the type filter logic. The compiler is not even tracking if the closure writes or just reads the variable.

All the examples have the same effect whether ->{ puts value.size }, ->{ puts value }, proc = ->{ puts value; value = "Bar" }. (NB: Actually your test4.cr don't because the closure is over the argument and not the variable, hence my expectation of test4.cr).

The workaround in your case, if you are expecting just to read the value could be to closure a copy of value:

value = get_value
puts typeof(value)

if value # or false or true or nil...
  copy = value
  puts typeof(value)
  puts value.size # OK: 3
  proc = ->{ puts copy }
  proc.call
end

So, I think is mainly a wontfix. At most it could be a low-prio enhancement for closures over read only values, but some details need to be analyzed first.

[mverzilli]

If it is a wontfix, we need to think how to document it in such a way that less people gets surprised by this or at least when they bring it up we can provide a link to an internally coherent explanation. So let's keep it open :).

[RX14]

Would it be possible to only undo the type filtering after the variable is closed on?

[bcardiff]

@RX14 No in the general case. It requires tracking the lifetime of the proc. Is one of those cases that the simple examples are doable, but a complete solution is not posible. And changing the semantic whether we can analyze or not a lifetime of an object it will be to obscure for the user.

[RX14]

I agree that tracking when a proc is called is impossible, but tracking when a proc is created doesn't seem (to me, with no compler knowledge) harder than tracking assignments (another thing which can widen a type).

[bcardiff]

In non linear code you can't. If the proc is created in a loop, or kept in an ivar i think the effect is hard to explain, and then to use.

[RX14]

Surely the effect of creating a closure on the variable is the same as assigning with a RHS of all the possible types. You can assign a new type to a variable in a loop, it just makes the same type for the whole loop. Ivars don't matter, because you don't need to track the closure once it's been created, you don't need to know where it's assigned, just that it was created.

I'm not saying it's worth doing, just that it's possible.

[bcardiff]

@RX14 I don't think it is. If the proc is assigned to an ivar, and you are in a multithread, or at least you generate a fiber switch, the proc could change the variable it is been closured. And all that could happen inside a branch where you would expect the type restriction to hold. If the variable leak out of the scope of the method, then you can't guarantee it's value/actual type remains the same.

[ozra]

If the proc is ever called can in some cases never be deduced but that it _cannot_ have been called at a certain time _can be deduced_. And so it should. Likewise, whether it has been modified / narrowed when it can be deduced the proc is called. And when it is/or is not known: it should be known, that the function is "pure" with regard to the certain closured variable. Of course it's a lot of work to improve inference, but imo one should continually strive to offload the user everything that is possible to deduce from available information "mechanically" - that's what compilers are for!

[RX14]

@bcardiff Sure, after the variable has been closured the variable cannot ever be type restricted again. But that's already the case. Why is it so difficult to make that happen only after the proc is assigned as opposed to before that in the code.

Why does this work but not this? What's the difference? This is surely a bug.

[asterite]

Duplicate of https://github.com/crystal-lang/crystal/issues/3093

[RX14]

@asterite solving that bug would solve this one, but isn't there another bug highlighted by my comment. Both of those examples capture the block but one restricts the type before the block and one does not.