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 |