id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential,wikipage
14164,GHC hangs on type family dependency,Iceland_jack,,"{{{#!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 ignoredotghci 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 ignoredotghci /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 righthand side.
Use fprintexplicitkinds 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 _) = '[]
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
}}}",bug,new,normal,8.10.1,Compiler,8.2.1,,InjectiveFamilies,RyanGlScott,Unknown/Multiple,Unknown/Multiple,None/Unknown,indexedtypes/should_compile/T14164,,,,,