You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If a data type mentions a non-existent type, then rather than throwing an error, or even timing-out, the elaborator seems to get stuck in an infinite loop.
data Foo α where
| A : NonExistent α → Foo α
The text was updated successfully, but these errors were encountered:
alexkeizer
changed the title
Infinite loop when referring to a non-existent type
Bug: Infinite loop when referring to a non-existent type
May 17, 2024
If a data type mentions a non-existent type, then rather than throwing an error, or even timing-out, the elaborator seems to get stuck in an infinite loop.
The text was updated successfully, but these errors were encountered: