Union-type declaration in :let rejects valid type in constructor

[tonchis]

With the following Mare code I expect to be able to optionally pass a positional argument to Bar.new, by making foo of (Foo | None) type:

:class Foo

:class Bar
  :let some_foo (Foo | None)

  :new (@some_foo = None)

:actor Main
  :new (env)
    foo = Foo.new
    Bar.new(foo)

However, Bar.new(foo) is rejecting foo saying it's not a subtype of None

Compilation Errors:

---

The type of this expression doesn't meet the constraints imposed on it:
from /opt/code/examples/main.mare:11:
    Bar.new(foo)
            ^~~

- it is required here to be a subtype of None:
  from /opt/code/examples/main.mare:6:
  :new (@some_foo = None)
                    ^~~~

- but the type of the local variable was Foo:
  from /opt/code/examples/main.mare:10:
    foo = Foo.new
    ^~~

---

The type of this expression doesn't meet the constraints imposed on it:
from /opt/code/examples/main.mare:10:
    foo = Foo.new
          ^~~~~~~

- it is required here to be a subtype of Foo:
  from /opt/code/examples/main.mare:10:
    foo = Foo.new
    ^~~

- it is required here to be a subtype of None:
  from /opt/code/examples/main.mare:6:
  :new (@some_foo = None)
                    ^~~~

- but the type of the return value was Foo:
  from /opt/code/examples/main.mare:10:
    foo = Foo.new
              ^~~

make: *** [Makefile:56: example-compile.inner] Error 1
make: *** [example-compile] Error 2

[jemc]

I am in the midst of working on a refactor of the type inference system, and I suspect that the new architecture will do a better prevent inference holes like this in the future.

However, in the short term, I'll see how easy it is to patch up this hole in the current infer pass.

[jemc]

I've taken a look at this and found that the work it will take to fix it is not worthwhile at this time while I am actively working to replace that subsystem with a better one.

The new type inference system I'm working on should handle this case well, so I'm going to mark this ticket as blocked by that one, and I'll ensure this bug gets fixed as part of that work.

[jemc]

This is blocked by #76.

[tonchis]

@jemc got it! makes sense. Meanwhile I found another problem that feels similar to this one while working on the packages/spec.

This is the following SpecEventAssert I have:

:class val SpecEventAssert
  :let success Bool
  :let pos SourceCodePosition
  :let assert (Assert | None)

  // TODO: refactor into the line below after #102 is fixed.
  // :new (@success, @pos, @assert = None)
  :new (@success, @pos, assert (Assert | None) = None)
    @assert = assert

And in spec_reporter.savi I'm calling

      if (event.assert <: Assert) (
        event.assert.report(@env)
      |
        @env.err.write("\n")
        @env.err.write(Inspect[event.pos.row + 1])
        @env.err.write(": FAIL: ")
        @env.err.print(event.pos.string)
      )

which fails compilation:

   335 ms : reach
     0 ms : paint
     0 ms : type_check
     0 ms : codegen
     0 ms : binary

Compilation Error:

---

The 'report' function can't be called on this receiver:
from /opt/code/packages/spec/spec_reporter.savi:57:
        event.assert.report(@env)
                     ^~~~~~

- None has no 'report' function:
  from /opt/code/src/prelude/none.savi:1:
:primitive None
           ^~~~

make: *** [Makefile:56: example-compile.inner] Error 1
make: *** [example-compile] Error 2

However, if I change the call site to extract event.assert into a variable, it works just fine:

    assert = event.assert

    if event.success (
      @env.err.write(".")
    |
      if (assert <: Assert) (
        assert.report(@env)
      |
        @env.err.write("\n")
        @env.err.write(Inspect[event.pos.row + 1])
        @env.err.write(": FAIL: ")
        @env.err.print(event.pos.string)
      )
    )

As both call sites are equivalent, I would expect both of them to work.

[jemc]

This last one is actually not a bug. This is actually a rather common limitation of many strongly typed languages.

As both call sites are equivalent, I would expect both of them to work.

They're actually not quite the same! Your first version calls event.assert twice (once in the condition, and once in the body), and the second one only calls it one time (to assign it to the variable).

The key point is that, from the limited perspective of this function scope's view of the world, while event.assert was a certain value/type the first time you checked it, it's not guaranteed to be the same value/type the next time you call it. So the compiler is being defensive and assuming the worst, assuming that a different value/type may be returned.

And again, this is a limitation you'll run into in many strongly typed languages - you often have to do something like the workaround you did of capturing to a variable and then testing the type of the variable. If you look at the compiler source code you'll see me doing the same thing all over the place to deal with the same limitation in Crystal. This works because the variable is locally scoped and the compiler can easily see that the variable is not changed between when you check it and when you use it.

Now, you could pretty convincingly argue that this specific case is pretty easily proved safe. Specifically, we know that the field event.assert is a let field (it cannot be rebound to a new value) and furthermore event is a val, so it is deeply immutable. So we can probably make the compiler smart enough to realize that this particular case is safe as-is. And arguably we should, perhaps!

However, even if we do so for this specific case, you will quickly run into other cases where it's not feasible to prove that the type doesn't change from one site to the next. In many cases it would require very extensive or even whole-program analysis to prove that some other function you're calling doesn't somehow reach back into the original object and change it before your second call. and in some cases it might be impossible to prove it (such as when a trait is blocking the compiler from knowing statically what the implementation of a particular function call is, since a trait hides the concrete type behind a structural interface).

The concern to keep in mind if we go down a road of doing that kind of extended analysis is a phenomenon we sometimes call "spooky action at a distance". Imagine an example where to prove that the type didn't change from one call to the next, the compiler had to traverse a deep tree of hundreds of possible function paths all over other parts of your program. Let's say that it did manage to prove this, and it allowed your code to compile. But then imagine that you're working in one of those other parts of the program and suddenly a change you made in a seemingly unrelated part of the program now makes it not possible for the compiler to prove the sameness of the type and now this error pops up in this distant region of code from the part you're working on, and you're like "what the heck? why is that code suddenly broken?"

That is, sometimes it is nicer for the programmer to have an overly strict rule that is applied consistently, than a very flexible rule that gets applied in a way that is hard to predict.

So we have to draw the line somewhere. At what point is it a reasonable level of analysis, and at what point does it become spooky action at a distance? These are questions we have to answer, and the answers may not be clear-cut.

For now, you'll need to account for this limitation when writing code by adopting a pattern of dealing with it. There's the workaround you did of using a variable, and there's also another approach that I might recommend here - using try and as! instead of if and <:.

I'll write up an example of what I'm suggesting in the code review for your pull request that includes this code.

[jemc]

Here's the example of what I suggest, using try and as!: https://github.com/savi-lang/savi/pull/103#discussion_r671783687

[tonchis]

@jemc Ohh! I got it. Thank you very much for the detailed account. I see how multiple call-sites of seemingly "the same thing" isn't a guarantee of sameness in the compiler's eyes.

It does make me wonder about the advantage of :let, and knowing this limitation, what other errors is :let guarding me from knowing that I still need to treat fields as if they might differ in value from one call to the next.

[jemc]

I think that's a reasonable complaint. Let's open up another ticket to continue this discussion about how let and val might help the compiler prove this case.