Closed christiaanb closed 5 years ago
Given:
[G] x :: KnownNat (a + b) [W] p :: KnownNat a
The plugin tries to solve this by generating:
evidence p = x - q new wanted: [W] q :: KnownNat b
the solver loop does another turn, and we get:
[G] x :: KnownNat (a + b) [W] q :: KnownNat b
which the plugin solves by:
evidence q = x - k new wanted: [W] k :: KnownNat a
and we're back to solving KnownNat a again, thus looking forever if it wasn't for the type checker solver iteration limit. This is https://github.com/clash-lang/clash-compiler/issues/608
KnownNat a
Given:
The plugin tries to solve this by generating:
the solver loop does another turn, and we get:
which the plugin solves by:
and we're back to solving
KnownNat aagain, thus looking forever if it wasn't for the type checker solver iteration limit. This is https://github.com/clash-lang/clash-compiler/issues/608