Re: [GHC] #10833: Use injective type families (decomposition) when dealing with givens

14 Sep 2018

      #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