Opened 4 years ago
Last modified 15 months ago
#10833 new feature request
Use injective type families (decomposition) when dealing with givens
Reported by: | jstolarek | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.10.2 |
Keywords: | TypeFamilies, InjectiveFamilies | Cc: | RyanGlScott, Iceland_jack, nfrisby |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #6018, #11511, #12199 | Differential Rev(s): | |
Wiki Page: |
Description
Consider this code:
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.
Change History (13)
comment:1 follow-up: 2 Changed 4 years ago by
Owner: | jstolarek deleted |
---|
comment:2 Changed 4 years ago by
I don't think this relates to 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.
comment:3 Changed 4 years ago by
Keywords: | TypeFamilies added |
---|
comment:4 Changed 3 years ago by
Related Tickets: | #6018 → #6018, #11511, #12199 |
---|
comment:5 Changed 3 years ago by
Summary: | Use injective type families when dealing with givens → Use injective type families (decomposition) when dealing with givens |
---|
comment:6 Changed 3 years ago by
Keywords: | InjectiveFamilies added |
---|
comment:7 Changed 3 years ago by
Cc: | RyanGlScott added |
---|
comment:8 Changed 3 years ago by
Cc: | Iceland_jack added |
---|
comment:9 Changed 2 years ago by
Cc: | nfrisby added |
---|
comment:10 Changed 2 years ago by
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.
comment:11 Changed 2 years ago by
I don't see why it wouldn't be possible as a plugin. Shouldn't be all that hard (as plugins go).
comment:12 Changed 15 months ago by
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:
{-# 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.
comment:13 Changed 15 months ago by
Implementing this requires changing Core.
A good step would be to write down exactly the changes required.
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 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.