Description
The to-poly function taking Geb morphisms to the Poly category seems to be faulty. The issue this stems from is #93 and has to do with evaluating the identity function on Bool in STLC - (lamb (coprod so1 so1) (index 0)) - in the empty context.
In particular, the code given by
(to-circuit nil (lamb (coprod so1 so1) (index 0)) :name)
accompanied with the entry code and additional constraint for checking such as name 0 = 0 or name 1 = 1 will fail during the Vamp-IR verification stage.
The interpreters and uncurry allowed to pinpoint that the fault seems to lie in the to-poly compiler step taking Geb morphisms to Poly. In particular, evaluating the object of poly at 0 and 1 gives
(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 0) 1/8
(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 1) 3/8
(note this code is run in geb.trans) while the correct application should give
(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 0) 1/8
(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 1) 3/8
The use of gapply in Geb seems to suggest that the STLC to Geb part of the pipeline works fine, so we need to figure out what is going awry with to-poly and fix it.