-- 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}'
I should have added that Data.HList exposes the more specific instances instance HEq HZero HZero HTrue instance HNat n => HEq HZero (HSucc n) HFalse instance HNat n => HEq (HSucc n) HZero HFalse instance (HNat n, HNat n', HEq n n' b ) => HEq (HSucc n) (HSucc n') b That's why I think ghc tries to resolve the wrong instance first: summary: class TypeToNat a b | a -> b class HEq a b c | a b -> c instance ( TypeToNat a elNr -- (1) , TypeToNat b elNr' -- (2) , HEq elNr elNr' r) => HEq a b r -- (3) putStrLn (show (undefined :: (HEq Id_A Id_A a) => a )) When ghc tries to resolve HEq it starts with TypeToNat ( TypeToNat Id_A <unkown type elNr> , TypeToNat Id_A <unkown type elNr'> , HEq <unkown type elNr> <unkown type elNr'> <unkown type r> ) Now ghc can try to resolve (1),(2),(3) in arbitrary order.. What happens if ghc starts with (3)? It tries to find an instance for not known types.. Damn. There is even a matching instance.. , the same one. This time it starts even with HEq <unkown> <unkown> <unkown> which is even more bad! after the second recursion it already knows that won't find a solution, because it will try to resolve HEq <unkown> <unkown> <unkown> again and again.. What happens if ghc starts with (1 or 2)? It happily finds an instance *and* it can even resolve elNr and elNr' Those can then be used to find an instance for (3) easily So I think the behaviour of ghc should be changed to prefer resolving class constraints which reduce the amount of unkown types first I even consider this beeing a bug ? So maybe this thread should be moved to glasgow-haskell-users ? Sincerly Marc Weber