Unsound matches with unconstrainted type parameters of different caps.

[ta3ta1]

Compiler crash on following code:

trait T
interface I
class C

actor Main
  fun f[A, B](x: (A | B)): (A | B) =>
    match x
    | let a: A => a
    | let b: B => b
    end

  new create(env: Env) =>
    f[I32, I](1) // NG
    // f[I32, T](1) // OK
    // f[I32, C](1) // OK

    // f[ReadSeq[I32], I](Array[I32]) // NG
    // f[ReadSeq[I32], T](Array[I32]) // NG
    // f[ReadSeq[I32], C](Array[I32]) // OK

Backtrace(lldb):

Building builtin -> /home/ta3ta1/Code/ponyc/packages/builtin
Building /home/ta3ta1/Code/issue/ -> /home/ta3ta1/Code/issue
Generating
 Reachability
 Selector painting
 Data prototypes
 Data types
 Function prototypes
 Functions
Process 1671 stopped
* thread ponylang/ponyc#1: tid = 1671, 0x00007ffff58e4230 libLLVM-3.9.so.1`llvm::BasicBlock::getContext() const, name = 'ponyc', stop reason = signal SIGSEGV: invalid address (fault address: 0x8)
    frame #0: 0x00007ffff58e4230 libLLVM-3.9.so.1`llvm::BasicBlock::getContext() const
libLLVM-3.9.so.1`llvm::BasicBlock::getContext:
->  0x7ffff58e4230 <+0>: movq   0x8(%rdi), %rax
    0x7ffff58e4234 <+4>: movq   (%rax), %rax
    0x7ffff58e4237 <+7>: retq   
    0x7ffff58e4238:      nopl   (%rax,%rax)
(lldb) bt
* thread ponylang/ponyc#1: tid = 1671, 0x00007ffff58e4230 libLLVM-3.9.so.1`llvm::BasicBlock::getContext() const, name = 'ponyc', stop reason = signal SIGSEGV: invalid address (fault address: 0x8)
  * frame #0: 0x00007ffff58e4230 libLLVM-3.9.so.1`llvm::BasicBlock::getContext() const
    frame ponylang/ponyc#1: 0x00007ffff595758f libLLVM-3.9.so.1`llvm::BranchInst::BranchInst(llvm::BasicBlock*, llvm::Instruction*) + 31
    frame ponylang/ponyc#2: 0x00007ffff590ae07 libLLVM-3.9.so.1`LLVMBuildBr + 55
    frame ponylang/ponyc#3: 0x00005555555fa174 ponyc`gen_match(c=0x00007fffffffdc30, ast=0x00007ffff00c5980) + 837 at genmatch.c:816
    frame ponylang/ponyc#4: 0x00005555555ecdb9 ponyc`gen_expr(c=0x00007fffffffdc30, ast=0x00007ffff00c5980) + 485 at genexpr.c:86
    frame ponylang/ponyc#5: 0x00005555555fa404 ponyc`gen_seq(c=0x00007fffffffdc30, ast=0x00007ffff00c5e00) + 78 at gencontrol.c:22
    frame ponylang/ponyc#6: 0x00005555555ecc5c ponyc`gen_expr(c=0x00007fffffffdc30, ast=0x00007ffff00c5e00) + 136 at genexpr.c:26
    frame ponylang/ponyc#7: 0x0000555555624daa ponyc`genfun_fun(c=0x00007fffffffdc30, t=0x00007ffff2a65800, m=0x00007ffff00a5e80) + 424 at genfun.c:436
    frame ponylang/ponyc#8: 0x00005555556261f6 ponyc`genfun_method_bodies(c=0x00007fffffffdc30, t=0x00007ffff2a65800) + 340 at genfun.c:895
    frame ponylang/ponyc#9: 0x00005555555f0ae8 ponyc`gentypes(c=0x00007fffffffdc30) + 1084 at gentype.c:884
    frame ponylang/ponyc#10: 0x000055555560b7f0 ponyc`genexe(c=0x00007fffffffdc30, program=0x00007ffff304dd00) + 559 at genexe.c:409
    frame ponylang/ponyc#11: 0x00005555555e9f5c ponyc`codegen(program=0x00007ffff304dd00, opt=0x00007fffffffe0d0) + 298 at codegen.c:1043
    frame ponylang/ponyc#12: 0x000055555559c8c2 ponyc`generate_passes(program=0x00007ffff304dd00, options=0x00007fffffffe0d0) + 53 at pass.c:301
    frame ponylang/ponyc#13: 0x000055555559b8f9 ponyc`compile_package(path="/home/ta3ta1/Code/issue/", opt=0x00007fffffffe0d0, print_program_ast=false, print_package_ast=false) + 147 at main.c:255
    frame ponylang/ponyc#14: 0x000055555559bdc6 ponyc`main(argc=2, argv=0x00007fffffffe248) + 1208 at main.c:398
    frame ponylang/ponyc#15: 0x00007ffff390d2b1 libc.so.6`__libc_start_main + 241
    frame ponylang/ponyc#16: 0x000055555559b6ba ponyc`_start + 42
(lldb) fr sel 3
frame ponylang/ponyc#3: 0x00005555555fa174 ponyc`gen_match(c=0x00007fffffffdc30, ast=0x00007ffff00c5980) + 837 at genmatch.c:816
   813 	    if(is_matchtype(match_type, pattern_type, c->opt) != MATCHTYPE_ACCEPT)
   814 	    {
   815 	      // If there's no possible match, jump directly to the next block.
-> 816 	      LLVMBuildBr(c->builder, next_block);
   817 	    } else {
   818 	      // Check the pattern.
   819 	      ok = static_match(c, match_value, match_type, pattern, next_block);
(lldb) fr va
(compile_t *) c = 0x00007fffffffdc30
(ast_t *) ast = 0x00007ffff00c5980
(bool) needed = true
(ast_t *) type = 0x00007ffff00c36c0
(ast_ptr_t) match_expr = 0x00007ffff00c4d80
(ast_ptr_t) cases = 0x00007ffff00c8280
(ast_ptr_t) else_expr = 0x00007ffff00c6b40
(LLVMTypeRef) phi_type = 0x0000555555929f30
(ast_t *) match_type = 0x00007fffefdd3980
(LLVMValueRef) match_value = 0x000055555594f170
(LLVMBasicBlockRef) pattern_block = 0x00005555559b75b0
(LLVMBasicBlockRef) else_block = 0x0000000000000000
(LLVMBasicBlockRef) post_block = 0x00005555559b74b0
(LLVMBasicBlockRef) next_block = 0x0000000000000000
(LLVMValueRef) phi = 0x00005555559b7538
(ast_t *) the_case = 0x00007ffff00ca940
(ast_t *) next_case = 0x0000000000000000
(ast_ptr_t) pattern = 0x00007ffff00c9040
(ast_ptr_t) guard = 0x00007ffff00c9380
(ast_ptr_t) body = 0x00007ffff00cb5c0
(ast_t *) pattern_type = 0x00007ffff00ca480
(bool) ok = true

NG patterns give same crash.

Compiler version:

0.18.0-96e96187 [debug]
compiled with: llvm 3.9.1 -- cc (Debian 6.3.0-18) 6.3.0 20170516

[jemc]

This is related to exhaustive match. When a match is exhaustive, the next_block will be NULL (as it is here). In those cases, we're never supposed to jump to the next_block (as we do here).

We need to step through this and figure out how to properly handle this case without jumping to the next_block (because there is no next_block).

[sylvanc]

@jemc 's diagnosis is right. @Praetonus says we should set the next_block to a block with an unreachable block terminator, as that branch should never be taken.

[jemc]

Sounds right to me 👍.

[Praetonus]

Hm no, the unreachable solution doesn't seem correct. I'll investigate more.

[Praetonus]

Since an equivalent code without generic types results in a compilation error, I think this match should either result in a compilation error or be considered non-exhaustive. I'm not sure which one is correct.

[jemc]

@Praetonus - it's definitely an exhaustive match, so it probably needs to be a compilation error.

Note that the error message you get when removing the indirection of the type parameters/arguments is:

Error:
main.pony:10:7: this capture violates capabilities, because the match would need to differentiate by capability at runtime instead of matching on type alone
    | let a: I32 => a
      ^
    Info:
    main.pony:8:13: the match type allows for more than one possibility with the same type as pattern type, but different capabilities. match type: (I32 val | I ref)
      fun f(x: (I32 | I)): (I32 | I) =>
                ^
    main.pony:10:7: pattern type: I32 val
        | let a: I32 => a
          ^
Error:
main.pony:11:7: this capture violates capabilities, because the match would need to differentiate by capability at runtime instead of matching on type alone
    | let b: I => b
      ^
    Info:
    main.pony:8:13: the match type allows for more than one possibility with the same type as pattern type, but different capabilities. match type: (I32 val | I ref)
      fun f(x: (I32 | I)): (I32 | I) =>
                ^
    main.pony:11:7: pattern type: I ref
        | let b: I => b
          ^

Note that I here is effectively the same as Any - an empty interface that is a supertype of everything. So the main issue is that I32 <: I, but they are different caps (val/ref), which means that you're matching on capability at runtime, which isn't allowed. The error goes away if you change interface I to interface val I.

So, exhaustive match doesn't really have anything to do with that problem - it would be the same problem for a non-exhaustive match.

---

This is an interesting case, because the only way to make this match safe would be to prove that either A and B are disjoint types, or that they have the same cap. It's interesting, because I don't know of a way to express either one of those conditions with type parameter constraints. So we end up with a situation where this very useful snippet (matching object type at runtime, from one of two type parameters) is seemingly impossible to write, even though there are many reifications of it that should be allowable.

Perhaps what we need are some new possibilities for expressing constraints? I'm not really sure what that should look like.

[SeanTAllen]

Sync consensus is that we want to remove crashing aspect of this (the bug) without disallowing valid code.

[jemc]

This was discussed on the 2017-09-06 sync call.

It's important to mention that this wouldn't be a problem if capabilities were present at runtime, rather than being a zero-cost abstraction that falls away at compile time. @sylvanc brought up that if we could still make them trivially cheap at runtime, this could be a good option, though we'd have to weigh it carefully because the zero-cost-abstraction part of capabilities that we have right now is really nice.

---

In the absence of that, we have to come up with a solution that disallows the unsafe case, even if it may also disallow some safe cases.

Our possible solutions are constrained by two requirements that we agreed on:

• We want the compiler to issue a typechecking error for this unsafe case.
• We don't want the compiler to have to know the type arguments when typechecking the body of a type-parameterized method (as this would allow the possibility of creating generic types that compile for some type arguments, and don't compile for others, which would quickly our poor programmers into the fiery pits of compiler hell)

With these in mind, we agreed our best choice for action was to modify the is_matchtype function (or rather, the static functions that implement it), which currently allows an unconstrained type parameter to be considered to potentially match anything. There are two places where this happens (one for the left side, and one for the right side of a match):

https://github.com/ponylang/ponyc/blob/021e3d4bf00e38a1d7c31e82926b339ee5626f9c/src/libponyc/type/matchtype.c#L407-L414

https://github.com/ponylang/ponyc/blob/021e3d4bf00e38a1d7c31e82926b339ee5626f9c/src/libponyc/type/matchtype.c#L165-L172

After we explored a lot of options, the only feasible one we came up with was to change the compiler to assume that an unconstrained type param cannot be guaranteed to match any type, because we have no clue what the type argument is, and for any given type on the other side of the match, there are examples of type arguments that will be a match that "violates capabilities" in the way described in my previous comment. In other words, we should return MATCHTYPE_DENY instead of MATCHTYPE_ACCEPT.

---

I'm marking this as an "easy" task, since now that it has been fully discussed, the solution is quite simple.

[Theodus]

Marking as needs discussion because this change has implications for the collections/List implementation. Specifically, ListNode.apply fails to compile: https://github.com/ponylang/ponyc/blob/master/packages/collections/list_node.pony#L16

We should consider a possible special case for as expressions

[Theodus]

During the last sync meeting we found that the failure to compile ListNode.apply was actually an example of a bug in the current compiler.

[jemc]

Right, and just to follow that up, it spurred me to add #105.

[jemc]

Found another case where the compiler was allowing matching on capability only, due to an unconstrained type param: https://github.com/ponylang/ponyc/pull/2289/files#diff-35e468e76bf0c02622ffcf7465e7cf82L411

[Praetonus]

I'm not sure the implementation solution described by @jemc above is correct, since it would forbid matching from a type parameter to the same type parameter (e.g. if the match type is a union containing the type parameter.)

I think a better solution would be to allow the match if the operand and pattern refer to the same type parameter with compatible caps, and to match on Any #any otherwise.

[shelby3]

@jemc wrote:

Note that I here is effectively the same as Any - an empty interface that is a supertype of everything.

That’s a problem with structural interfaces. With (nominally or structurally selected) type classes which in my opinion would be preferable to interfaces and traits, AFAICT you wouldn’t have this problem.

If I remember correctly, it was @keean who taught me that (in his opinion) Any shouldn’t even be in a statically type programming language. You may need top and bottom types for the type checker but no actual type created by the programmer should ever equate to Any. So if you need Any, then I think it indicates there’s likely some fundamental design flaw in the language?

This is an interesting case, because the only way to make this match safe would be to prove that either A and B are disjoint types, or that they have the same cap. It's interesting, because I don't know of a way to express either one of those conditions with type parameter constraints. So we end up with a situation where this very useful snippet (matching object type at runtime, from one of two type parameters) is seemingly impossible to write, even though there are many reifications of it that should be allowable.

Are y’all familiar with Stephen Dolan’s MLsub thesis? He points out that type systems that have unions and intersections and that don’t put the unions and intersections (all types) in the ground types have an unwieldy algebra that is very difficult if not impossible to prove sound. Perhaps §2.1.5 Distributivity and subtyping on pg. 21 is also applicable.

I’ll quote:

^{Despite the succinctness of this definition, these types have a remarkably complicated and unwieldy algebra. Pottier gave the following example illustrating the incompleteness of a particular subtyping algorithm…}

So if all types are in the ground types, then there’s a distributive lattice and I think the disjointness you need is guaranteed? I need to reread that MLsub paper to be sure about this.

If the above is correct about your design being fundamentally unsound, then more cases will be discovered as more Pony code is written. And special case “fixes” would proliferate. In that case, perhaps it would be wise to bite the bullet now and scrap current design for a design that would be sound? Especially if the replacement would provide superior functionality and expression for the programmer.

EDIT: I posted that at 3am my time. After thinking about this more, nominal subtyping (e.g. traits) also prevents the needed disjoint invariant of the types (e.g. A is an Animal and B is a Cat, so is A also a Cat?). Without disjoint invariant of types in the union and intersection types, I imagine the reasoning about the type system has corner cases. The plan I had been formulating for a type system would only have subtyping from the anonymous, structural union types and no nominal subtyping. And no structural interfaces. The type classes would replace everything you currently use classes, interfaces, and traits for. And I think I would opt for nominal instead of Haskell’s structural type classes.

Also anonymous, structural (i.e. not nominal) intersection types seem to cause problems in a type system. If there’s no traits nor interfaces, then I don’t think they’re needed (not accessible to the Pony programmer) except perhaps only in the type checker as the dual to anonymous, structural union types. @keean had demonstrated to me that intersections of first-class functions can cause unification to be undecidable. We see another example of unsoundness due to intersections in §2.6.4 Modelling Challenges of the recent paper by George Steed about improving Pony.

FYI: this post of mine might subsume the Subtyping exclusion RFC.

EDIT#2: some additional thoughts.

Note that to exclude the vacuous reasoning, I posit not only would need to exclude traits and interfaces (i.e. subtyping other than for anonymous, structural unions) from the programming language, but would also need to exclude anonymous, structural unions from type parametrised cases that can cause undecidable cases such as the example of this thread. I think that could be accomplished by only applying type class bound operations on anonymous, structural unions, which effectively removes any overlapping non-disjoint portions of any union of said unions because the type class instances are resolved at compile-time and can’t be overlapping.¹ Understanding my posited point may be aided by reading this.

¹ _{Haskell does have an optional extension for overlapping instances but presuming not enabling overlapping instances.}