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