thorin2
thorin2 copied to clipboard
Function used as a type but is in fact a term
Observed in lit/direct/ds2cps_ax_cps2ds_dependent_short.thorin
Command line: ./build/bin/thorin -d direct -d tool ./lit/direct/ds2cps_ax_cps2ds_dependent_short.thorin --output-thorin -
Issue:
:4294967295: error: 'Π n_167425: .Nat → .infer (<nullptr>)' used as a type but is in fact a term
High-level description:
We constructed a wrapper around .Idx
Suspected problem: Idx has problems with the duality of fundamental integer and being applied as a function.
Suffers also from #106.
- changing the literal to
0:.Idx n
and - adding a return type to
lam_idx
fixes the test case.
see also #103:
Work is underway to add type inference.
Marked as enhancement as the only remaining real problem is the type inference that is not yet properly implemented.