anoma / geb

A Categorical View of Computation

https://anoma.github.io/geb/

GNU General Public License v3.0

28 stars 10 forks source link

Possibly-incorrect type error where Geb expects a product type #58

Closed rokopt closed 1 year ago

rokopt commented 1 year ago

See this comment to #47. I'm not immediately sure whether this is supposed to produce a type error or not, but I will investigate it and fix it if it's supposed to typecheck. I'm not sure whether there's any relationship with #57 not being implemented yet or not.

rokopt commented 1 year ago

I think I've made a test case out of the term that originally produced this error:

https://github.com/anoma/geb/commit/f1baf142302084a8abd30c874029fa330a51ad60

It doesn't run into the "not a product type" problem documented in the comment , though. I'm not specifically aware of anything having changed since that might have fixed it, but I might be missing something. Does the problem still occur with the Juvix-generated code?

rokopt commented 1 year ago

...Apparently all I needed to do was post that, and suddenly my test has started reproducing the "not a product type" error, without my making further changes. Some Lisp test infrastructure caching bug or something? I have no idea.

rokopt commented 1 year ago

This might be the bug:

https://github.com/anoma/geb/commit/6f28b5b4385c87093c7521cd2b2072c8e9e01193

rokopt commented 1 year ago

70 includes what I think might be a fix for this.

rokopt commented 1 year ago

I believe this has been fixed by https://github.com/anoma/geb/commit/c356c6cd7a4687b623651686ba39186a5266e06d (borrowed from the fix in #70).