7 commits

Author	SHA1	Message	Date
Ayaz Hafiz	49a92e5ef1	Support fixpoint-fixing under recursion variables ... Sometimes, we might need to fixpoint-fix a unification like [ Bar [ Bar <a>, Foo ], Foo ] as <a> 🛠️ [ Bar <b>, Foo ] as <b> where we hit a comparison between <a> and <b>. In this case, follow each recursion point independently and see if we can find the chain to the needle we were searching for. Closes #5476	2023-06-13 17:15:11 -05:00
Ayaz Hafiz	1c93727822	Add a notion of "openness" tag extensions suitable only for size-polymorphism	2023-01-16 10:52:23 -06:00
Ayaz Hafiz	bef9b54124	Avoid parsing doc comments as code	2022-11-16 14:05:53 -06:00
Ayaz Hafiz	2cba520839	Document fixpoint fixing algorithm	2022-11-16 14:05:51 -06:00
Ayaz Hafiz	8414c8e2de	Remove unneeded comments	2022-11-16 14:05:51 -06:00
Ayaz Hafiz	5a92947326	Use fixpoint-fixing in unification	2022-11-16 14:05:51 -06:00
Ayaz Hafiz	3c968b581d	Check in fixpoint-fixing algorithm	2022-11-16 14:05:51 -06:00