search

AshleyYakeley / Truth

Changes and Pinafore projects. Pull requests not accepted.
https://pinafore.info/
GNU General Public License v2.0
32 stars 0 forks source link

Solver apparently cannot solve long-ish recursive types #237

Closed AshleyYakeley closed 11 months ago

AshleyYakeley commented 1 year ago 
(rec g, b | Maybe. (rec e, g | Maybe. e)) | Maybe. (rec e, (rec g, b | Maybe. (rec e, g | Maybe. e)) | Maybe. e)
<:
rec d, (rec f, (rec h, (rec i, b & Maybe. (rec d, (rec f, (rec h, i & Maybe. (rec d, (rec f, h & Maybe. (rec d, f & Maybe. d)) & Maybe. d)) & Maybe. (rec d, f & Maybe. d)) & Maybe. d)) & Maybe. (rec d, (rec f, h & Maybe. (rec d, f & Maybe. d)) & Maybe. d)) & Maybe. (rec d, f & Maybe. d)) & Maybe. d

Makes progress but uses up all available memory.

AshleyYakeley commented 1 year ago

Simpler case (note b is free in both):

rec r, b | Maybe r
<:
rec d, (rec f, (rec h, (rec i, b & Maybe. (rec d, (rec f, (rec h, i & Maybe. (rec d, (rec f, h & Maybe. (rec d, f & Maybe. d)) & Maybe. d)) & Maybe. (rec d, f & Maybe. d)) & Maybe. d)) & Maybe. (rec d, (rec f, h & Maybe. (rec d, f & Maybe. d)) & Maybe. d)) & Maybe. (rec d, f & Maybe. d)) & Maybe. d
AshleyYakeley commented 1 year ago

Will be fixed by fixing #234.

AshleyYakeley commented 11 months ago

Fixed.