[Haskell-cafe] HEq and Context reduction stack overflow

27 Aug 2008

      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