Yes, I know that UndecidableInstances
can be bad. I really tried hard to design my module so that it doesn't need it however I have something like this:
instance Foo x (C x y) => Bar (C x y) where
...
and changing it would make the API substantially uglier. I never derive Foo
out of Bar
so there is no way to make a loop.
On the other hand enabling UndecidableInstances
makes silly mistakes easy to overlook. For example I could write by mistake something like:
instance Foo x (C x z) => Bar (C x y) where
...
where z
never appears on the right side.
Question: Is it possible to use UndecidableInstances
locally in a module, i.e. explicitly mark places where the usual termination rules are lifted?
Of course it won't help with termination, but it will make the decision to use this extension more informed.
Question 2: Is there something weaker than UndecidableInstances
that still wouldn't guarantee termination, but would forbid some more border-line cases like the second code snippet?
So far, language pragmas are per-module, so the answer to the first question is no. As for the second question, I'm not quite sure, but I know of no other extension than UndecidableInstances that would allow the instance.
However, UndecidableInstances isn't that bad, it just allows the type checker to attempt to resolve instances where it can't prove termination. The context-stack prevents it from actually looping forever, though.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With