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