Opened 5 years ago

Closed 5 years ago

#10125 closed bug (invalid)

Improper evaluation of type families

Reported by: danilo2 Owned by:
Priority: high Milestone:
Component: Compiler Version: 7.8.4
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (3)

comment:1 Changed 5 years ago by danilo2

Summary: Inproper evaluation of type familiesImproper evaluation of type families

comment:2 Changed 5 years ago by danilo2

Priority: normalhigh

comment:3 Changed 5 years ago by simonpj

Resolution: invalid
Status: newclosed

It's a bug in GHC 7.8. The program should be rejected because you have an un-saturated application of CmpNat on the last line. I'm afraid that GHC's type inference machinery is only capable of dealing with saturated applications of type families. Sorry. HEAD and 7.10 reject it with a decent message.

I'll close as invalid because GHC doesn't claim to support it. Many people would like to do higher order type-family programming in this way, but it's an open question how to do so with predicable type inference.

Simon

Note: See TracTickets for help on using tickets.