GHC hangs on type family dependency

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

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 _)    = '[]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture