#10910: Data families seem not to be "surely apart" from anything -------------------------------------+------------------------------------- Reporter: oerjan | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: | Keywords: data | families, closed type families Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by oerjan: Old description:

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.

{{{#!hs {-# 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 }}}

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

New description: 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. {{{#!hs {-# 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.) -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10910#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10910: Data families seem not to be "surely apart" from anything -------------------------------------+------------------------------------- Reporter: oerjan | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: data Resolution: | families, closed type families Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * component: Compiler => Compiler (Type checker) Comment: Compiles fine with HEAD (ghc-7.11.20150909). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10910#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler