#12199: GHC is oblivious to injectivity when a type family is used in a GADT type -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple Injective | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- [https://www.reddit.com/r/haskell/comments/4oeidw/type_family_dependencies_an... A reddit post] points out a limitation of injective type families: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilyDependencies #-} type family Foo a = b | b -> a where Foo Int = Bool data Bar :: * -> * where Bar :: a -> Bar (Foo a) oink :: Bar Bool -> Int oink (Bar x) = x -- type error }}} Compiling this fails with: {{{ Could not deduce: a ~ Int from the context: Bool ~ Foo a }}} Which seems odd, given that `Bool ~ Foo a` should imply `a ~ Int` by injectivity. Even if you change the type signature of `oink` to `Bar (Foo Int) -> Int`, it fails with: {{{ Could not deduce: a ~ Int from the context: Foo Int ~ Foo a }}} which makes it even more apparent that it isn't aware of the fact that `Foo` is injective. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12199 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler