[Haskell-cafe] HEq and Context reduction stack overflow

[Marc Weber]

On Mon, Aug 25, 2008 at 09:17:19PM -0400, jeff p wrote:
>   The HList paper (http://homepages.cwi.nl/~ralf/HList/) presents a

Thanks Jeff


        -- packages: HList
        {-# OPTIONS_GHC -fallow-undecidable-instances -XEmptyDataDecls -XMultiParamTypeClasses #-}
        module Main where
        import Data.HList
        import HAppS.Data
        import System.Environment
         
         
        class TypeToNat typE nr | typE -> nr
        instance ( TypeToNat a elNr
                 , TypeToNat b elNr'
                 , HEq elNr elNr' r) => HEq a b r
         
        data Id_A
        instance TypeToNat Id_A HZero
        data Root_T
        instance TypeToNat Id_A nr => TypeToNat Root_T (HSucc nr)
         
        main = do 
          putStrLn (show (undefined :: (HEq Id_A Id_A a) => a ))
 
 
|| [1 of 1] Compiling Main             ( test.hs, test.o )
|| 
test.hs|19 error| 
||     Context reduction stack overflow; size = 20
||     Use -fcontext-stack=N to increase stack size to N
||         `$dHEq :: {HEq elNr elNr' a}'
||           arising from instantiating a type signature at test.hs:20:18-52
||         `$dHEq :: {HEq elNr elNr' a}'



However adding a dummy type T works fine:

        -- packages: HList
        {-# OPTIONS_GHC -XEmptyDataDecls -XMultiParamTypeClasses -fallow-undecidable-instances #-}
        module Main where
        import Data.HList
        import HAppS.Data
        import System.Environment
         
        data T a
         
        class TypeToNat typE nr | typE -> nr
        instance ( TypeToNat a elNr
                 , TypeToNat b elNr'
                 , HEq elNr elNr' r) => HEq (T a) (T b) r
         
        data Id_A
        instance TypeToNat Id_A HZero
        data Root_T
        instance TypeToNat Id_A nr => TypeToNat Root_T (HSucc nr)
         
        main = do 
          putStrLn (show (undefined :: (HEq (T Id_A) (T Id_A) a) => a ))

I don't see what's wrong with the first version.. Can you help me
understand this implicationa ?

Sincerly Marc Weber