
Jay Cox writes: | One day I was playing around with types and I came across this type: | | >data S m a = Nil | Cons a (m (S m a)) : | >instance (Show a, Show (m (S m a))) => Show (S m a) where | > show Nil = "Nil" | > show (Cons x y) = "Cons " ++ show x ++ " " ++ show y | | which boggles my mind. But hugs +98 and ghci | -fallow-undecidable-instances both allow it to compile but when i try | | >show s | | on | | >s = Cons 3 [Cons 4 [], Cons 5 [Cons 2 [],Cons 3 []]] | | (btw yes we are "nesting" an arbitrary lists here! however structurally | it really isnt much different from any tree datatype) | | we get | | | ERROR - | *** The type checker has reached the cutoff limit while trying to | *** determine whether: | *** Show (S [] Integer) | *** can be deduced from: | *** () | *** This may indicate that the problem is undecidable. However, | *** you may still try to increase the cutoff limit using the -c | *** option and then try again. (The current setting is -c998) | | | funny thing is apparently if you set -c to an odd number (on hugs) | it gives | | | *** The type checker has reached the cutoff limit while trying to | *** determine whether: | *** Show Integer | *** can be deduced from: | *** () | | why would it try to deduce Show integer? It's the first subgoal of Show (S [] Integer). If the cutoff were greater by 1, presumably it's achieved, and then that last memory cell is reused for the second subgoal Show [S [] Integer], which in turn has a subgoal Show (S [] Integer), which overflows... as Dylan's just pointed out, so I'll stop now. - Tom