thorin2 icon indicating copy to clipboard operation
thorin2 copied to clipboard

Function used as a type but is in fact a term

Open NeuralCoder3 opened this issue 2 years ago • 2 comments

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.

NeuralCoder3 avatar Oct 04 '22 13:10 NeuralCoder3

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.

leissa avatar Oct 12 '22 23:10 leissa

Marked as enhancement as the only remaining real problem is the type inference that is not yet properly implemented.

leissa avatar Oct 12 '22 23:10 leissa