Skip to content

Data families seem not to be "surely apart" from anything

The following code is not compiling (GHC 7.10.2), it looks as if data families are not considered "surely apart" from any type, despite being injective.

{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}

type family Equals x y where
    Equals x x = True
    Equals x y = False

data Booly b where
    Truey :: Booly True
    Falsey :: Booly False

data family ID a

data instance ID Bool = IB

test :: Booly (Equals (ID Bool) Int)
test = Falsey

This gives the error

Test.hs:16:8: Warning:
    Couldn't match type ‘Equals (ID Bool) Int’ with ‘'False’
    Expected type: Booly (Equals (ID Bool) Int)
      Actual type: Booly 'False
    In the expression: Falsey
    In an equation for ‘test’: test = Falsey

This gives no error with an ordinary type instead of a data family.

(Inspired and simplified from http://stackoverflow.com/questions/32733368/type-inequalities-in-the-presence-of-data-families#32733368.)

Edited by oerjan@nvg.ntnu.no
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information