[GHC] #10833: Use injective type families when dealing with givens
#10833: Use injective type families when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #6018 Differential Revisions: | -------------------------------------+------------------------------------- Consider this code: {{{#!hs type family Id a = r | r -> a id :: (Id a ~ Id b) => a -> b id x = x }}} GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * owner: jstolarek => Comment: In the "Injective Type Families for Haskell" we did not present a full proof of soundness of injective type families. It might be the case that the proof requires solving [[http://www.win.tue.nl/rtaloop/problems/79.html|RTA #79]]. But we don't know for sure. Richard argues that for this reason we should not make these changes to Core - if our conjecture that our proof holds turns out to be incorrect Core will become inconsistent. So for the time being I am abandoning further work on this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I don't think this relates to [[http://www.win.tue.nl/rtaloop/problems/79.html|RTA #79]]. (The soundness of type families + `UndecidableInstances` + non-linear patterns does.) Perhaps more sweat on the proof would yield fruit. But somehow it failed to succumb, and so I'm wary of putting it in Core. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: #6018 => #6018, #11511, #12199 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies => TypeFamilies, InjectiveFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by nfrisby): * cc: nfrisby (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by nfrisby): This scenario seems like an excellent use-case for a typechecker plugin: so that power users could opt-in to the soundness conjecture. Do we have an estimate of if that's possible give current TC plugin API and how complicated it would be to implement? Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I don't see why it wouldn't be possible as a plugin. Shouldn't be all that hard (as plugins go). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by infinity0): Just ran into this trying to implement a type-level fmap over a GADT-based HList, mniip on IRC helped to explain that the error was another variant of this bug: {{{#!haskell {-# LANGUAGE DataKinds , GADTs , ScopedTypeVariables , TypeFamilies , TypeFamilyDependencies , TypeOperators #-} data HList xs where HNil :: HList '[] (:::) :: a -> HList as -> HList (a ': as) infixr 6 ::: type family FMapLoad r (m :: * -> *) (xs :: [*]) = (xs' :: [*]) | xs' -> xs where FMapLoad r m '[] = '[] FMapLoad r m (x ': xs) = (r -> m x) ': FMapLoad r m xs sequenceLoad :: forall r m hlist. Monad m => HList (FMapLoad r m hlist) -> [r] -> m (HList hlist) sequenceLoad fs rs = case (fs, rs) of (HNil, []) -> return HNil (HNil, _ ) -> error "xxx" (_, []) -> error "xxx" (f:::fs, r:rs) -> do a <- f r (a :::) <$> sequenceLoad fs rs main :: IO () main = do return () }}} gives for example the error: {{{ • Could not deduce: hlist ~ '[] from the context: FMapLoad r m hlist ~ '[] bound by a pattern with constructor: HNil :: HList '[], }}} even though `FMapLoad` is injective. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10833: Use injective type families (decomposition) when dealing with givens -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018, #11511, | Differential Rev(s): #12199 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Implementing this requires changing Core.
A good step would be to write down exactly the changes required. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10833#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC