hax Equality constraints meta issue

Equality constraints are sort of hard to encode systematically:

what about mutually recursive classes + eq constraints?
- F* syntactically disallow defining 2+ mutually recursive typeclasses, but using plain records it's possible:
```
[@@FStar.Tactics.Typeclass.tcclass] type foo t = {f : t -> int}
and bar t = {g : t -> int}
```
- but then the constraints are not possible to define (we cannot destruct fields of mutually dependent types, see if it's easy to extend F*, see how this behaves in Coq/Lean)
can we detect casts? that is, when A = B, and x has type A in a position where B is expected, can we insert explicitly cast_using [[A=B]] x?

We also need a bunch of examples.

Nov 03 '23 14:11 W95Psp

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Oct 05 '24 02:10 github-actions[bot]

Still relevant

Oct 07 '24 06:10 W95Psp

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Dec 09 '24 02:12 github-actions[bot]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

May 29 '25 00:05 github-actions[bot]

Still an issue

Jul 17 '25 08:07 W95Psp

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Nov 27 '25 00:11 github-actions[bot]