Pattern Match claims case to be not matchable although it should be #2408

mfelsche · 2017-12-07T21:26:12Z

In the following minimal example the match expression in GenericSum.sum claims that the first case cannot match although the type we match on is correct.

This might have to do with using addc which is not part of the Integer trait and only defined on the concrete Int types. To have a generic function, wrapping addc, that works on all Int types (which all have addc) I had to create the interface SafeOps[T] defining addc and subc in a generic way. I suspect that the issue is here but i cannot pinpoint it yet.

interface SafeOps[T]
  fun addc(t: T): (T, Bool)
  fun subc(t: T): (T, Bool)

class GenericSum[T: (Int & Integer[T] val & SafeOps[T])]
  fun _plus_safe(x: T, y: T): (T, Bool) =>
    x.addc(y)
    
  fun sum(x: T, y: T): T ? =>
    match _plus_safe(x, y)
    | (let res: T, false) => res
    | (_, true) => error
    end
      
actor Main
  new create(env: Env) =>
    try
      env.out.print(GenericSum[U8].sum(1, 2)?.string())
    end

http://playground.ponylang.org/?gist=a2138611ec2c1f4685a243a9d6e71737

Expected output:

Actual output:

0.20.0 [release]
compiled with: llvm 3.9.1 -- cc (Ubuntu 5.4.0-6ubuntu1~16.04.5) 5.4.0 20160609
Error:
main.pony:11:18: this pattern can never match
    | (let res: T, false) => res
                 ^
    Info:
    main.pony:6:33: match type: (T val, Bool val)
      fun _plus_safe(x: T, y: T): (T, Bool) =>
                                    ^
    main.pony:11:18: pattern type: (T val, Bool val)
        | (let res: T, false) => res
                     ^
Error:
main.pony:10:5: function body isn't the result type
    match _plus_safe(x, y)
    ^
    Info:
    main.pony:9:24: function return type: T val
      fun sum(x: T, y: T): T ? =>
                           ^
    main.pony:11:17: function body type: (T val ^ | None val^)
        | (let res: T, false) => res
                    ^
    packages/builtin/none.pony:1:1: None val^ is not a subtype of T val: the type parameter has no lower bounds
    primitive None is Stringable
    ^
    packages/builtin/none.pony:1:1: not every element of (T val ^ | None val^) is a subtype of T val
    primitive None is Stringable
    ^

The text was updated successfully, but these errors were encountered:

mfelsche · 2017-12-07T21:46:23Z

I found out why this might not work as expected: U128 and I128 do not implement addc or subc. That's why the code above is plain wrong. What still puzzles me is the bad error message.

jemc · 2017-12-13T20:55:37Z

Next step for debugging would be to run in lldb, breakpoint the "this pattern can never match" error message, and take a look at what ast_print shows for the match type and for the pattern type.

From that we could figure out what the issue is and how to proceed.

mfelsche · 2017-12-15T08:40:37Z

The whole match expr has the following AST:

(match:scope
  (seq
    (call
      (funref
        (this
          [->
            thistype
            (nominal
              (id $1)
              (id GenericSum)
              (typeargs (typeparamref (id T) val x))
              ref
              x
              x
            )
          ]
        )
        (id _plus_safe)
        [funtype
          box
          x
          (params
            (param (id x) (typeparamref (id T) val x) x)
            (param (id y) (typeparamref (id T) val x) x)
          )
          (tupletype
            (typeparamref (id T) val x)
            (nominal (id $0) (id Bool) x val x x)
          )
        ]
      )
      (positionalargs
        (seq
          (paramref (id x) [typeparamref (id T) val x])
          [typeparamref (id T) val x]
        )
        (seq
          (paramref (id y) [typeparamref (id T) val x])
          [typeparamref (id T) val x]
        )
      )
      x
      x
      [tupletype
        (typeparamref (id T) val x)
        (nominal (id $0) (id Bool) x val x x)
      ]
    )
    [tupletype
      (typeparamref (id T) val x)
      (nominal (id $0) (id Bool) x val x x)
    ]
  )
  (cases:scope
    (case:scope
      (tuple
        (seq
          ($let
            ((id res) [typeparamref (id T) val x])
            (typeparamref (id T) val x)
            [typeparamref (id T) val x]
          )
          [typeparamref (id T) val x]
        )
        (seq
          (false [nominal (id $0) (id Bool) x val x x])
          [nominal (id $0) (id Bool) x val x x]
        )
        [tupletype
          (typeparamref (id T) val x)
          (nominal (id $0) (id Bool) x val x x)
        ]
      )
      x
      (seq
        (letref (id res) [typeparamref (id T) val ^])
        [typeparamref (id T) val ^]
      )
      [tupletype
        (typeparamref (id T) val x)
        (nominal (id $0) (id Bool) x val x x)
      ]
    )
    (case:scope
      (tuple (seq (dontcareref (id _))) (seq true))
      x
      (seq (error x))
    )
  )
  x
)

The types of the first case and the match expression are indeed identical.

When determining if the pattern can match, it is failing when comparing the following operand and pattern in is_x_match_x(...):

operand:

(&
  (uniontype
    (nominal (id $0) (id I8) x val x x)
    (nominal (id $0) (id I16) x val x x)
    (nominal (id $0) (id I32) x val x x)
    (nominal (id $0) (id I64) x val x x)
    (nominal (id $0) (id I128) x val x x)
    (nominal (id $0) (id ILong) x val x x)
    (nominal (id $0) (id ISize) x val x x)
    (nominal (id $0) (id U8) x val x x)
    (nominal (id $0) (id U16) x val x x)
    (nominal (id $0) (id U32) x val x x)
    (nominal (id $0) (id U64) x val x x)
    (nominal (id $0) (id U128) x val x x)
    (nominal (id $0) (id ULong) x val x x)
    (nominal (id $0) (id USize) x val x x)
  )
  (nominal (id $0) (id Integer) (typeargs (typeparamref (id T) val x)) val x x)
  (nominal (id $1) (id SafeOps) (typeargs (typeparamref (id T) val x)) val x x)
)

which is the result of typeparam_upper called on (typeparamref (id T) val x)

pattern:
(nominal (id $0) (id I8) x val x x)

This comparison basically tells me that I8 is not matching (Int & Integer[T] val & SafeOps[T]) though it is a valid instantiation of the typeparam T. (e.g. I128 isn't, which is expected)

jemc · 2018-01-10T21:37:26Z

@sylvanc said he could get it to compile if he did two things:

Remove Int from the type intersection.
Add an else branch to the match.

On the sync call we determined that it was stopping at I8 because it was in the middle of is_isect_sub_x, and was stopping on the first element of the intersection comparison. I'd be interested to see a full backtrace of where this is_x_match_x failed comparison is called from.

We're keeping the label on so we can discuss this on next week's sync, because we ran out of time.

mfelsche · 2018-01-12T21:40:56Z

I am really sorry to have missed the Sync call, I really liked following along your thinking and digging.

To make things clear, the above code sample and the type definition are not wrong because U128 and I128 do not implement addc and subc. They would just not be captured by the type param T: (Int & Integer[T] & SafeOps[T]) which is fine for this example.

While the actual issue was worked around long ago and the fixes mentioned by @sylcanc are fixing the code sample above, the remaining problem is the bad error report.

I am trying to find a proper backtrace and the actual flaw in the is_subtype call chain.

mfelsche · 2018-01-17T20:26:29Z

The comparison that fails and leads to the match being rejected is the comparison of I16 and I8 where I16 stems from the Int union and I8 is also from the union. My best guess up to now is that we handle something wrong with descending down the different intersect and union types, but i need to investigate further.

Here is some output from lldb at the point it actually fails:

* thread #1: tid = 18371, 0x00000000004d9de1 ponyc`is_nominal_match_nominal(operand=0x00007ffff283ff80, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 91 at matchtype.c:330, name = 'ponyc', stop reason = step over
  * frame #0: 0x00000000004d9de1 ponyc`is_nominal_match_nominal(operand=0x00007ffff283ff80, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 91 at matchtype.c:330
    frame #1: 0x00000000004d9fc0 ponyc`is_x_match_nominal(operand=0x00007ffff283ff80, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 185 at matchtype.c:389
    frame #2: 0x00000000004da1c0 ponyc`is_x_match_x(operand=0x00007ffff283ff80, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 235 at matchtype.c:456
    frame #3: 0x00000000004d93d4 ponyc`is_union_match_x(operand=0x00007ffff2840380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 68 at matchtype.c:21
    frame #4: 0x00000000004d9f84 ponyc`is_x_match_nominal(operand=0x00007ffff2840380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 125 at matchtype.c:380
    frame #5: 0x00000000004da1c0 ponyc`is_x_match_x(operand=0x00007ffff2840380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 235 at matchtype.c:456
    frame #6: 0x00000000004d9456 ponyc`is_isect_match_x(operand=0x00007ffff2840300, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 68 at matchtype.c:51
    frame #7: 0x00000000004d9fa0 ponyc`is_x_match_nominal(operand=0x00007ffff2840300, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 153 at matchtype.c:383
    frame #8: 0x00000000004da1c0 ponyc`is_x_match_x(operand=0x00007ffff2840300, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 235 at matchtype.c:456
    frame #9: 0x00000000004d96b3 ponyc`is_typeparam_match_x(operand=0x00007ffff2847380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 73 at matchtype.c:175
    frame #10: 0x00000000004d9fd9 ponyc`is_x_match_nominal(operand=0x00007ffff2847380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 210 at matchtype.c:392
    frame #11: 0x00000000004da1c0 ponyc`is_x_match_x(operand=0x00007ffff2847380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 235 at matchtype.c:456
    frame #12: 0x00000000004d94d8 ponyc`is_x_match_union(operand=0x00007ffff2847380, pattern=0x00007ffff284a4c0, opt=0x00007fffffffd880) + 68 at matchtype.c:81
    frame #13: 0x00000000004da16f ponyc`is_x_match_x(operand=0x00007ffff2847380, pattern=0x00007ffff284a4c0, opt=0x00007fffffffd880) + 154 at matchtype.c:447
    frame #14: 0x00000000004d955a ponyc`is_x_match_isect(operand=0x00007ffff2847380, pattern=0x00007ffff284a540, opt=0x00007fffffffd880) + 68 at matchtype.c:111
    frame #15: 0x00000000004da18b ponyc`is_x_match_x(operand=0x00007ffff2847380, pattern=0x00007ffff284a540, opt=0x00007fffffffd880) + 182 at matchtype.c:450
    frame #16: 0x00000000004da064 ponyc`is_x_match_typeparam(operand=0x00007ffff2847380, pattern=0x00007ffff28468c0, opt=0x00007fffffffd880) + 73 at matchtype.c:417
    frame #17: 0x00000000004da1d9 ponyc`is_x_match_x(operand=0x00007ffff2847380, pattern=0x00007ffff28468c0, opt=0x00007fffffffd880) + 260 at matchtype.c:459
    frame #18: 0x00000000004d9617 ponyc`is_tuple_match_tuple(operand=0x00007ffff2846d80, pattern=0x00007ffff2846f40, opt=0x00007fffffffd880) + 127 at matchtype.c:145
    frame #19: 0x00000000004d9768 ponyc`is_x_match_tuple(operand=0x00007ffff2846d80, pattern=0x00007ffff2846f40, opt=0x00007fffffffd880) + 161 at matchtype.c:192
    frame #20: 0x00000000004da1a7 ponyc`is_x_match_x(operand=0x00007ffff2846d80, pattern=0x00007ffff2846f40, opt=0x00007fffffffd880) + 210 at matchtype.c:453
    frame #21: 0x00000000004da246 ponyc`is_matchtype(operand=0x00007ffff2846d80, pattern=0x00007ffff2846f40, opt=0x00007fffffffd880) + 43 at matchtype.c:476
    frame #22: 0x00000000004b76f9 ponyc`expr_case(opt=0x00007fffffffd880, ast=0x00007ffff3079840) + 603 at match.c:512
    frame #23: 0x0000000000477ac6 ponyc`pass_expr(astp=0x00007fffffffd348, options=0x00007fffffffd880) + 763 at expr.c:531
    frame #24: 0x0000000000475555 ponyc`ast_visit(ast=0x00007fffffffd348, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 615 at pass.c:412
    frame #25: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd3b8, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #26: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd428, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #27: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd498, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #28: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd508, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #29: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd578, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #30: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd5e8, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #31: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd658, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #32: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd6c8, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #33: 0x00000000004754a7 ponyc`ast_visit(ast=0x00007fffffffd788, pre=(ponyc`pass_pre_expr at expr.c:470), post=(ponyc`pass_expr at expr.c:487), options=0x00007fffffffd880, pass=PASS_EXPR) + 441 at pass.c:383
    frame #34: 0x0000000000474bad ponyc`visit_pass(astp=0x00007fffffffd788, options=0x00007fffffffd880, last_pass=PASS_ALL, out_r=0x00007fffffffd767, pass=PASS_EXPR, pre_fn=(ponyc`pass_pre_expr at expr.c:470), post_fn=(ponyc`pass_expr at expr.c:487)) + 139 at pass.c:171
    frame #35: 0x0000000000474f5b ponyc`ast_passes(astp=0x00007fffffffd788, options=0x00007fffffffd880, last=PASS_ALL) + 679 at pass.c:239
    frame #36: 0x00000000004750d9 ponyc`ast_passes_program(ast=0x00007ffff36bfd00, options=0x00007fffffffd880) + 40 at pass.c:273
    frame #37: 0x00000000004476ff ponyc`program_load(path=".", opt=0x00007fffffffd880) + 191 at package.c:933
    frame #38: 0x0000000000444ed0 ponyc`compile_package(path=".", opt=0x00007fffffffd880, print_program_ast=false, print_package_ast=false) + 44 at main.c:56
    frame #39: 0x00000000004450fc ponyc`main(argc=2, argv=0x00007fffffffda28) + 407 at main.c:118
    frame #40: 0x00007ffff41b8830 libc.so.6`__libc_start_main(main=(ponyc`main at main.c:73), argc=2, argv=0x00007fffffffda28, init=<unavailable>, fini=<unavailable>, rtld_fini=<unavailable>, stack_end=0x00007fffffffda18) + 240 at libc-start.c:291
    frame #41: 0x0000000000444d59 ponyc`_start + 41
(lldb) p ast_print(operand, 80)
(nominal (id $0) (id I16) x val x x)

(lldb) p ast_print(pattern, 80)
(nominal (id $0) (id I8) x val x x)

(lldb) frame select 1
frame #1: 0x00000000004d9fc0 ponyc`is_x_match_nominal(operand=0x00007ffff283ff80, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 185 at matchtype.c:389
   386 	      return MATCHTYPE_REJECT;
   387 	
   388 	    case TK_NOMINAL:
-> 389 	      return is_nominal_match_nominal(operand, pattern, opt);
   390 	
   391 	    case TK_TYPEPARAMREF:
   392 	      return is_typeparam_match_x(operand, pattern, opt);
(lldb) p ast_print(operand, 80)
(nominal (id $0) (id I16) x val x x)

(lldb) p ast_print(pattern, 80)
(nominal (id $0) (id I8) x val x x)

(lldb) frame select 2
frame #2: 0x00000000004da1c0 ponyc`is_x_match_x(operand=0x00007ffff283ff80, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 235 at matchtype.c:456
   453 	      return is_x_match_tuple(operand, pattern, opt);
   454 	
   455 	    case TK_NOMINAL:
-> 456 	      return is_x_match_nominal(operand, pattern, opt);
   457 	
   458 	    case TK_TYPEPARAMREF:
   459 	      return is_x_match_typeparam(operand, pattern, opt);
(lldb) p ast_print(operand, 80)
(nominal (id $0) (id I16) x val x x)

(lldb) p ast_print(pattern, 80)
(nominal (id $0) (id I8) x val x x)

(lldb) frame select 3
frame #3: 0x00000000004d93d4 ponyc`is_union_match_x(operand=0x00007ffff2840380, pattern=0x00007ffff284a940, opt=0x00007fffffffd880) + 68 at matchtype.c:21
   18  	    child != NULL;
   19  	    child = ast_sibling(child))
   20  	  {
-> 21  	    switch(is_x_match_x(child, pattern, opt))
   22  	    {
   23  	      case MATCHTYPE_ACCEPT:
   24  	        // If any type in the operand union accepts a match, then the entire
(lldb)  p ast_print(operand, 80)  
(uniontype
  (nominal (id $0) (id I8) x val x x)
  (nominal (id $0) (id I16) x val x x)
  (nominal (id $0) (id I32) x val x x)
  (nominal (id $0) (id I64) x val x x)
  (nominal (id $0) (id I128) x val x x)
  (nominal (id $0) (id ILong) x val x x)
  (nominal (id $0) (id ISize) x val x x)
  (nominal (id $0) (id U8) x val x x)
  (nominal (id $0) (id U16) x val x x)
  (nominal (id $0) (id U32) x val x x)
  (nominal (id $0) (id U64) x val x x)
  (nominal (id $0) (id U128) x val x x)
  (nominal (id $0) (id ULong) x val x x)
  (nominal (id $0) (id USize) x val x x)
)

(lldb) p ast_print(pattern, 80)
(nominal (id $0) (id I8) x val x x)

(lldb)

mfelsche · 2019-02-24T20:31:04Z

This seems to have been fixed with ponyc 0.26.0.
I am not sure, though what exactly caused this to work now.
Maybe:

https://github.com/ponylang/ponyc/pull/2660/files

I dunno if we should close it, though. Maybe we still have some corpses in the basement? But hopefully any work on: #2982 will fix whatever is still hid.

jemc · 2019-02-25T22:09:06Z

Maybe the remaining scope of this issue ticket would be to create a regression test to prevent it from being accidentally broken by future work?

SeanTAllen · 2022-01-27T05:13:51Z

This compiles now when an else is added to the match:

interface SafeOps[T]
  fun addc(t: T): (T, Bool)
  fun subc(t: T): (T, Bool)

class GenericSum[T: (Int & Integer[T] val & SafeOps[T])]
  fun _plus_safe(x: T, y: T): (T, Bool) =>
    x.addc(y)
    
  fun sum(x: T, y: T): T ? =>
    match _plus_safe(x, y)
    | (let res: T, false) => res
    | (_, true) => error
    else
      error
    end
      
actor Main
  new create(env: Env) =>
    try
      env.out.print(GenericSum[U8].sum(1, 2)?.string())
    end

But otherwise there is a compilation error. When @mfelsche said that this was working as of 0.26.0, did he mean with the else or as originally reported.

If it's with the else, we can easily add a regression test for this and close this out.

Fixes #2408.

mfelsche · 2022-03-05T19:20:37Z

Yes, this one works with the else. It needs this because ponyc doesn't detect the exhaustive match. The actual mismatch that led to this issue is fixed with current ponyc. Regression test is being added.

Fixes #2408.

mfelsche added the project error message label Dec 7, 2017

jemc added the needs discussion during sync label Dec 8, 2017

mfelsche mentioned this issue Dec 8, 2017

addc and subc functions not implemented for U128 and I128 #2409

Closed

SeanTAllen added bug: 1 - needs investigation help wanted Extra attention is needed and removed needs discussion during sync labels Dec 13, 2017

jemc added the needs discussion during sync label Dec 15, 2017

jemc removed the needs discussion during sync label Aug 8, 2018

SeanTAllen added needs investigation This needs to be looked into before its "ready for work" bug Something isn't working and removed project error message labels May 12, 2020

SeanTAllen added the discuss during sync Should be discussed during an upcoming sync label Feb 1, 2022

mfelsche added a commit that referenced this issue Mar 5, 2022

Add regression test for issue 2408.

6ce4fd0

Fixes #2408.

mfelsche mentioned this issue Mar 5, 2022

Add regression test for issue 2408. #4050

Merged

SeanTAllen closed this as completed in #4050 Mar 6, 2022

SeanTAllen pushed a commit that referenced this issue Mar 6, 2022

Add regression test for issue 2408. (#4050)

eaf6dda

Fixes #2408.

ponylang-main removed the discuss during sync Should be discussed during an upcoming sync label Mar 6, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pattern Match claims case to be not matchable although it should be #2408

Pattern Match claims case to be not matchable although it should be #2408

mfelsche commented Dec 7, 2017

mfelsche commented Dec 7, 2017

jemc commented Dec 13, 2017

mfelsche commented Dec 15, 2017

jemc commented Jan 10, 2018

mfelsche commented Jan 12, 2018

mfelsche commented Jan 17, 2018

mfelsche commented Feb 24, 2019

jemc commented Feb 25, 2019

SeanTAllen commented Jan 27, 2022

mfelsche commented Mar 5, 2022

Pattern Match claims case to be not matchable although it should be #2408

Pattern Match claims case to be not matchable although it should be #2408

Comments

mfelsche commented Dec 7, 2017

mfelsche commented Dec 7, 2017

jemc commented Dec 13, 2017

mfelsche commented Dec 15, 2017

jemc commented Jan 10, 2018

mfelsche commented Jan 12, 2018

mfelsche commented Jan 17, 2018

mfelsche commented Feb 24, 2019

jemc commented Feb 25, 2019

SeanTAllen commented Jan 27, 2022

mfelsche commented Mar 5, 2022