Application Error with matching domain

[NeuralCoder3]

I get an error that an application can not be constructed ("cannot pass argument") although the type of the argument matches the domain exactly:

  '(0:(.Idx 4294967296), _6524550, 1:(.Idx 4294967296), _6524522, forOut_0, _6524540)' of type 
  '[.Idx 4294967296, .Idx 4294967296, .Idx 4294967296, [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)], .Cn [.Idx 4294967296, [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)], .Cn [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)]], .Cn [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)]]' to 
  '%affine.For (4294967296, 2, (%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)))' of domain 
  '[.Idx 4294967296, .Idx 4294967296, .Idx 4294967296, [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)], .Cn [.Idx 4294967296, [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)], .Cn [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)]], .Cn [%mem.M, %matrix.Mat (2, (__6522473#1:(.Idx 2), __6522473#0:(.Idx 2)), T_6522475)]]'

Fork: NeuralCoder3
Branch: ad_ptr_merge
Commit: ee33da0
Command: ./build/bin/thorin -d matrix -d affine -d direct -d clos -d math -d autodiff lit/autodiff/matrix/prod.thorin -o - -VVVV
Situation: In the matrix medium level lowering pass.

[leissa]

Looks to me that sth in alpha-equiv is broken. I hope to finally have #153 ready this week. As this contains a major overhaul of this code, I don't want to touch it in master. Let's first merge #153, then I will investigate if the problem still persists.

[NeuralCoder3]

Possibly related:

Nested calls like

.con print_m2d [mem:%mem.M] = {
    print_double_matrix_wrap (mem, l, n, m2d, return_cont)
};
.con print_m1d [mem:%mem.M] = {
    print_double_matrix_wrap (mem, k, l, m1d, print_m2d)
};
print_double_matrix_wrap (mem, k, n, m, print_m1d)

(or the inlined version

print_double_matrix_wrap (mem, k, n, m  , .cn [mem: %mem.M] = {
print_double_matrix_wrap (mem, k, l, m1d, .cn [mem: %mem.M] = {
print_double_matrix_wrap (mem, l, n, m2d, return_cont)
})

)
lead to application errors involving proxies:

lit/autodiff/matrix/prod.thorin:33:15-33:94: error: cannot pass argument 
  '.proxy#8#0 print_double_matrix_wrap_6406994, 3' of type 
  '%matrix.Mat (2, (k_6407046, l_6407048), %math.F (52, 11))' to 
  '%core.bitcast (%matrix.Mat (2, ‹2; ⊤:.Nat›, %math.F (52, 11)), %matrix.Mat (2, (.proxy#8#0 print_double_matrix_wrap_6406994, 1, .proxy#8#0 print_double_matrix_wrap_6406994, 2), %math.F (52, 11)))' of domain 
  '%matrix.Mat (2, (.proxy#8#0 print_double_matrix_wrap_6406994, 1, .proxy#8#0 print_double_matrix_wrap_6406994, 2), %math.F (52, 11))

The error does not occur with a single print call.

Fork: NeuralCoder3
Branch: ad_ptr_merge
Commit: 04c5f38
Command: ./build/bin/thorin -d autodiff lit/autodiff/matrix/prod.thorin -d affine -d matrix -d direct -d clos -d math -o - -VVVV --output-ll T.ll

Note: This branch temporarily jumps the other alpha equiv problem using string comparisons (on the printed expressions).

[leissa]

Good thing: In my recent PR, I changed the alpha-equiv magic to always work optimistically. I.e. if you invoke checker().alpha_equiv(a, b), a and b must be alpha-equiv or there is a type error. This makes the logic a bit simpler and I can revert it how it used to work a few months ago.

[leissa]

#180 :
I've just fixed a problem in the matrix/product.thorin.disabled. Is this a different test case?
Now, I get:

../build/bin/thorin matrix/product.thorin.disabled
thorin: /home/roland/neural/dialects/matrix/passes/lower_matrix_mediumlevel.cpp:275: thorin::matrix::LowerMatrixMediumLevel::rewrite_(const thorin::Def*)::<lambda(thorin::u64)>: Assertion `idx == i && "output indices must be consecutive 0..n-1"' failed.

[NeuralCoder3]

#180 : I've just fixed a problem in the matrix/product.thorin.disabled. Is this a different test case? Now, I get:

../build/bin/thorin matrix/product.thorin.disabled
thorin: /home/roland/neural/dialects/matrix/passes/lower_matrix_mediumlevel.cpp:275: thorin::matrix::LowerMatrixMediumLevel::rewrite_(const thorin::Def*)::<lambda(thorin::u64)>: Assertion `idx == i && "output indices must be consecutive 0..n-1"' failed.

The index issue was temporarily from switching the map to the absl one.
At one point I assumed an order which coincidentally was created by the std::map (and by absl in verbose mode).
This should be fixed by e147add.

[leissa]

Can you check with #219?

[NeuralCoder3]

Can you check with #219?

I will test it. But it will take time to resolve all the merge conflicts.