[BUG] invalid:mat-lam on valid program using SUP enumeration

[Lorenzobattistela]

First reported by @developedby on commit e3b5492b5bbc8f4fcc90944cdd93699381539ed3 when trying to run programs like book/enum_primes.hvml . I tried running other examples from book and basically all enum ones are failing with this bug where we get invalid:mat-lam in a valid program. I've reached a minimal reproducible example with:

data Bin { #O{pred} #I{pred} #E }

@all1(s) = ~s{
  0: #E
  p: !&1{p0 p1}=p &1{ #O{@all1(p0)} #I{@all1(p1)} }
}

// Bin Equality
@eq(a b) = ~a !b {
  #E: ~b {
    #O{bp}: 0
    #I{bp}: 0
    #E: 1
  }
  #O{ap}: ~b{
    #O{bp}: @eq(ap bp)
    #I{bp}: 0
    #E: 0
  }
  #I{ap}: ~b{
    #O{bp}: 0
    #I{bp}: @eq(ap bp)
    #E: 0
  }
}

@some_bin  = #O{#I{#E}}
@some_bin2 = #I{#E}

@X = @all1(2)

@main = @eq(@X @some_bin)

Note that here, if I use the length of bitstring as 1 (and change some bin to have length 1), everything works as expected. Debug mode fails and prints a string forever (another bug to report). So, I changed Runtime.c and printed the reduce calls:

❯ hvml run book/test2.hvml -C
reduce_let term_new(LET,0x000000,0x000000025)
reduce_mat_w32 term_new(MAT,0x000002,0x000000027)
reduce_app_lam term_new(APP,0x000000,0x000000033)
reduce_mat_sup term_new(MAT,0x000003,0x000000003)
reduce_app_sup term_new(APP,0x000000,0x000000022)
reduce_mat_ctr term_new(MAT,0x000003,0x000000003)
reduce_dup_lam term_new(DP0,0x000001,0x000000039)
reduce_app_lam term_new(APP,0x000000,0x000000043)
reduce_dup_lam term_new(DP0,0x000001,0x000000045)
reduce_app_lam term_new(APP,0x000000,0x000000022)
reduce_mat_sup term_new(MAT,0x000003,0x000000009)
reduce_mat_ctr term_new(MAT,0x000003,0x000000035)
reduce_dup_lam term_new(DP1,0x000001,0x00000003b)
reduce_app_lam term_new(APP,0x000000,0x00000005b)
reduce_dup_lam term_new(DP1,0x000001,0x00000005d)
reduce_app_lam term_new(APP,0x000000,0x000000041)
reduce_mat_sup term_new(MAT,0x000003,0x000000013)
reduce_dup_sup 1 1 | 0 term_new(DP1,0x000001,0x000000063) term_new(SUP,0x000001,0x000000067)
reduce_dup_ctr term_new(DP1,0x000001,0x00000003f)
reduce_mat_ctr term_new(MAT,0x000003,0x000000069)
reduce_dup_lam term_new(DP1,0x000001,0x00000006d)
reduce_app_lam term_new(APP,0x000000,0x000000078)
reduce_dup_w32 term_new(DP1,0x000001,0x00000007a)
0
reduce_mat_ctr term_new(MAT,0x000003,0x000000009)
reduce_dup_lam term_new(DP0,0x000001,0x000000055)
reduce_app_lam term_new(APP,0x000000,0x000000080)
reduce_mat_sup term_new(MAT,0x000003,0x000000088)
reduce_app_sup term_new(APP,0x000000,0x0000000a7)
reduce_mat_ctr term_new(MAT,0x000003,0x000000009)
reduce_app_lam term_new(APP,0x000000,0x0000000b7)
reduce_dup_ctr term_new(DP1,0x000001,0x00000004b)
reduce_mat_ctr term_new(MAT,0x000003,0x000000051)
reduce_dup_lam term_new(DP1,0x000001,0x000000057)
reduce_app_lam term_new(APP,0x000000,0x0000000bc)
reduce_dup_w32 term_new(DP1,0x000001,0x0000000be)
0
reduce_let term_new(LET,0x000000,0x0000000c4)
reduce_dup_w32 term_new(DP0,0x000001,0x00000002b)
reduce_mat_w32 term_new(MAT,0x000002,0x0000000c6)
reduce_app_lam term_new(APP,0x000000,0x0000000d2)
reduce_mat_sup term_new(MAT,0x000003,0x000000088)
reduce_app_sup term_new(APP,0x000000,0x0000000a7)
reduce_mat_lam term_new(MAT,0x000003,0x0000000a9)
invalid:mat-lam%                      

Which gives 2 results (0, false) before failing with invalid mat-lam.
Still investigating why and how to fix.

[Lorenzobattistela]

Another interesting thing: when running an old commit where this invalid mat lam was not happening, i got 3 results instead of 4. With the same snippet, if we print @x, we get:

#0{#0{#2{}}}
#0{#1{#2{}}}
#1{#0{#2{}}}
#1{#1{#2{}}}

Which are the 4 possible bitstrings. But when running the equality test, i get 3 results:

0
0
1

(this is where the current commit fails) but sill, one of the results is missing.
This also happens in the current version if I use bitstring length as 1

[Lorenzobattistela]

Possibly related:
The same program, when ran through debug mode, generates an infinite recursion of MAT, which also causes the debug to crash. I think it is possible that it is related to the invalid mat-lam case as well.

The thing is that even a term that correctly reduces (e.g the first case) crashes the debug, which means the infinite recursion of matches is still being generated but possibly not used.

Starting to investigate where this infinite recursion comes from

[Lorenzobattistela]

The commit that breaks it is 8868bbffee5fe16ed658be883658eb7b5edd6fe0 , which is removing the type annotations. In this commit, trying to print @all1(1) already infinitely recurses.

[Lorenzobattistela]

Printing the reduction steps of simply @all(1) leads me to this step, which is causing the infinite recursion:

---------------- ROOT: 
(~a {#{}:#2{} #{}:λb &1{#0{! c = d
(~d {#{}:#2{} #{}:λf &1{#0{@all1(g)} #1{@all1(h)}}})} #1{@all1(e)}}})
! &1{d e} = &1{#0{! c = d
(~d {#{}:#2{} #{}:λf &1{#0{@all1(g)} #1{@all1(h)}}})} #1{@all1(e)}}
! &1{g h} = &1{#0{@all1(g)} #1{@all1(h)}}

reduce_let term_new(LET,0x000000,0x000000010)
reduce: term_new(MAT,0x000002,0x000000012)
---------------- ROOT: 
(~a {#{}:#2{} #{}:λb &1{#0{(~c {#{}:#2{} #{}:λe &1{#0{@all1(f)} #1{@all1(g)}}})} #1{@all1(d)}}})
! &1{c d} = &1{#0{(~c {#{}:#2{} #{}:λe &1{#0{@all1(f)} #1{@all1(g)}}})} #1{@all1(d)}}
! &1{f g} = &1{#0{@all1(f)} #1{@all1(g)}}

Note that after the last reduce_let, on reduce: term_new(MAT...)

we get the following:

! &1{c d} = &1{#0{(~c {#{}:#2{} #{}:λe &1{#0{@all1(f)} #1{@all1(g)}}})} #1{@all1(d)}}

Where c is referencing itself, so when we match this arm, it will keep reaching #0 and matching c again and so on. But why?