[GHC] #10125: Inproper evaluation of type families
GHC
ghc-devs at haskell.org
Sun Mar 1 16:06:50 UTC 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
More information about the ghc-tickets
mailing list