[GHC] #10125: Inproper evaluation of type families

1 Mar 2015

      #10125: Inproper evaluation of type families
-------------------------------------+-------------------------------------
              Reporter:  danilo2     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.8.4
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Hello! I've got here a small piece of code:

 {{{#!haskell
 {-# 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))’
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10125
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler