= ... return ...
I know this is basically a rewording of a previous e-mail, but I realized this is the question I *really* wanted to ask. We have this language extension UndecidableInstances (not to mention OverlappingInstances), which seem to divide the Haskell camp into two factions: * Hey, GHC said to turn on this flag. Ok! * Undecidables are the devil! I get the feeling the truth lies in the middle. As I understand it (please correct me if I am wrong), the problem with undecidables is that they can create non-terminating instances. However, for certain cases the programmer should be able to prove to him/herself that the instances will terminate. My question is: how can you make such a proof? I've had to cases in particular that made me want undecidables. Both of them, IMO, could be solved by creating new extensions to GHC which would not require undecidables. Nonetheless, for now we only have undecidables at our disposal. The examples are: * Context synonyms (eg, MonadFailure = Monad + Failure). * Subclass function defaulting For an example of the second, a nifty definition of Monad would be: class Applicative m => Monad m where pure = return (<*>) = ap fmap = liftM Of course, neither of these is possible in Haskell, so we can use undecidables. How can a programmer prove that a set of instances is, in fact, safe? And if they make a mistake and right a bad set of undecidable/overlapping instances, what's the worst case scenario? Is it a compile-time or run-time error*? Michael * Yes, I mean error.