[GHC] #12199: GHC is oblivious to injectivity when a type family is used in a GADT type
#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
#12199: GHC is oblivious to injectivity when solving an equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): [https://www.reddit.com/r/haskell/comments/4oeidw/type_family_dependencies_an... gelisam points out] an even simpler failing example that doesn't involve GADTs. Even worse, it's cited as an example that should typecheck from section 5.3 of the [http://ics.p.lodz.pl/%7Estolarek/_media/pl:research :stolarek_peyton-jones_eisenberg_injectivity_extended.pdf original injective type families paper]! {{{#!hs {-# LANGUAGE TypeFamilyDependencies #-} type family F a = b | b -> a fid :: (F a ~ F b) => a -> b fid x = x }}} {{{ Could not deduce: a ~ b from the context: F a ~ F b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12199#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12199: GHC is oblivious to injectivity when solving an equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10833 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: => #10833 Comment: Example in #comment:1 should not compile '''yet''' - see #10833 for details. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12199#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12199: GHC is oblivious to injectivity when solving an equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10833 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies, Injective => TypeFamilies, InjectiveFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12199#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12199: GHC is oblivious to injectivity when solving an equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10833 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by nfrisby): * cc: nfrisby (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12199#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12199: GHC is oblivious to injectivity when solving an equality constraint -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeFamilies, Resolution: duplicate | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10833 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate Comment: This is really a duplicate of #10833. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12199#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC