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 Changed 4 years ago by jstolarek

Owner: jstolarek deleted

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.

comment:2 in reply to:  1 Changed 4 years ago by goldfire

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 thomie

Keywords: TypeFamilies added

comment:4 Changed 3 years ago by jstolarek

comment:5 Changed 3 years ago by ezyang

Summary: Use injective type families when dealing with givensUse injective type families (decomposition) when dealing with givens

comment:6 Changed 3 years ago by simonpj

Keywords: InjectiveFamilies added

comment:7 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:8 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:9 Changed 2 years ago by nfrisby

Cc: nfrisby added

comment:10 Changed 2 years ago 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.

Version 0, edited 2 years ago by nfrisby (next)

comment:11 Changed 2 years ago by goldfire

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 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:

{-# 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 simonpj

Implementing this requires changing Core.

A good step would be to write down exactly the changes required.

Note: See TracTickets for help on using tickets.