Improper evaluation of type families
Hello! I've got here a small piece of code:
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.TypeLevel.Bool where
import Prelude hiding (Eq)
import qualified Prelude as P
import Data.Typeable
import GHC.TypeLits
type family Eq (a :: k) (b :: k) where
Eq a a = True
Eq a b = False
type family If (cond :: Bool) (a :: k) (b :: k) where
If True a b = a
If False a b = b
type family CmpBy (f :: k -> k -> Ordering) (a :: [k]) (b :: [k]) :: Ordering where
CmpBy f '[] '[] = EQ
CmpBy f (a ': as) (b ': bs) = If (Eq (f a b) EQ) (CmpBy f as bs) (f a b)
type family TCompare (a :: [Nat]) (b :: [Nat]) :: Ordering where
TCompare '[] '[] = EQ
TCompare (a ': as) (b ': bs) = If (Eq a b) (TCompare as bs) (CmpNat a b)
type N1 = '[1,2,3,5]
type N2 = '[1,2,3,4]
main = do
print $ (Proxy :: Proxy GT) == (Proxy :: Proxy (TCompare N1 N2))
print $ (Proxy :: Proxy GT) == (Proxy :: Proxy (CmpBy CmpNat N1 N2))
It does NOT compile, while it should. The type-level functions TCompare
and CmpBy CmpNat
should work exactly the same way. Right now the former one always returns EQ
, so the program does not compile with an error:
Bool.hs:49:41:
Couldn't match type ‘'EQ’ with ‘'GT’
Expected type: Proxy (CmpBy CmpNat N1 N2)
Actual type: Proxy 'GT
In the second argument of ‘(==)’, namely
‘(Proxy :: Proxy (CmpBy CmpNat N1 N2))’
In the second argument of ‘($)’, namely
‘(Proxy :: Proxy GT) == (Proxy :: Proxy (CmpBy CmpNat N1 N2))’
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |