Funny type.

[Tom Pledger]

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