[Haskell-cafe] HEq and Context reduction stack overflow, non optimal ghc behaviour ?

[Marc Weber]

>         -- 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