[GHC] #14164: GHC hangs on type family dependency

[GHC]

#14164: GHC hangs on type family dependency
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language TypeOperators, DataKinds, PolyKinds, KindSignatures,
 TypeInType, GADTs, TypeFamilyDependencies #-}

 import Data.Kind

 type Cat a = a -> a -> Type

 data SubList :: Cat [a] where
   SubNil :: SubList '[] '[]
   Keep   :: SubList xs ys -> SubList (x:xs) (x:ys)
   Drop   :: SubList xs ys -> SubList xs     (x:ys)

 type family
   UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res
 -> pf ys' xs where
   UpdateWith '[]    '[]    SubNil      = '[]
   UpdateWith (y:ys) '[]    SubNil      = y:ys
   -- UpdateWith '[]    (_:_)  (Keep _)    = '[]
   UpdateWith (y:ys) (_:xs) (Keep rest) = y:UpdateWith ys xs rest
   -- UpdateWith ys     (x:xs) (Drop rest) = x:UpdateWith ys xs rest
 }}}

 seems to loop forever on the "`Renamer/typechecker`"

 {{{
 $ ghci -ignore-dot-ghci -v /tmp/u.hs
 GHCi, version 8.3.20170605: http://www.haskell.org/ghc/  :? for help
 Glasgow Haskell Compiler, Version 8.3.20170605, stage 2 booted by GHC
 version 8.0.2

 [...]

 *** Parser [Main]:
 !!! Parser [Main]: finished in 1.31 milliseconds, allocated 0.651
 megabytes
 *** Renamer/typechecker [Main]:

 [hangs]
 }}}

 while

 {{{#!hs
 type family
   UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res
 -> pf ys' xs where
   UpdateWith '[]    '[]    SubNil      = '[]
   UpdateWith (y:ys) '[]    SubNil      = y:ys
   UpdateWith '[]    (_:_)  (Keep _)    = '[]
 }}}

 immediately gives

 {{{
 $ ghc -ignore-dot-ghci /tmp/u.hs
 [1 of 1] Compiling Main             ( /tmp/u.hs, /tmp/u.o )

 /tmp/u.hs:14:3: error:
     • Type family equations violate injectivity annotation:
         UpdateWith '[] '[] 'SubNil = '[] -- Defined at /tmp/u.hs:14:3
         forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).
           UpdateWith '[] (_2 : _1) ('Keep _3) = '[]
             -- Defined at /tmp/u.hs:16:3
     • In the equations for closed type family ‘UpdateWith’
       In the type family declaration for ‘UpdateWith’
    |
 14 |   UpdateWith '[]    '[]    SubNil      = '[]
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 /tmp/u.hs:16:3: error:
     • Type family equation violates injectivity annotation.
       Type and kind variables ‘_2’, ‘_1’, ‘xs’, ‘_3’
       cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
         forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).
           UpdateWith '[] (_2 : _1) ('Keep _3) = '[]
             -- Defined at /tmp/u.hs:16:3
     • In the equations for closed type family ‘UpdateWith’
       In the type family declaration for ‘UpdateWith’
    |
 16 |   UpdateWith '[]    (_:_)  (Keep _)    = '[]
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14164>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler