GHC issues
https://gitlab.haskell.org/ghc/ghc/-/issues
2019-07-07T18:26:39Z
https://gitlab.haskell.org/ghc/ghc/-/issues/12430
TypeFamilyDependencies accepts invalid injectivity annotation
2019-07-07T18:26:39Z
Alexey Vagarenko
TypeFamilyDependencies accepts invalid injectivity annotation
Consider this code (depends on singletons-2.2):
```hs
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators,
KindSignatures, TypeInType, TypeFamilyDependencies, UndecidableInstances #-}
module Bug where
import Data.Kind (Type...
Consider this code (depends on singletons-2.2):
```hs
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators,
KindSignatures, TypeInType, TypeFamilyDependencies, UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Singletons.Prelude (Map, SndSym0)
import GHC.TypeLits (Nat)
data Payload = A | B
newtype NewType a = NewType Int
type NatList = [(Nat, Payload)]
type StripNatList (natList :: NatList) = Map SndSym0 natList
type family Family (natList :: NatList) = (r :: Type) | r -> natList where
Family '[] = ()
Family xs = NewType (StripNatList xs)
```
Why GHC is okay with injectivity annotation for `Family`: `r -> natList`?
These two types:
```hs
type Foo = Family '[ '(0, 'A), '(1, 'B)]
type Bar = Family '[ '(0, 'A), '(0, 'B)]
```
are obviously map to the same type:
```hs
*Bug Data.Singletons.Prelude> :kind! Foo
Foo :: *
= NewType ('A :$$$ '['B])
*Bug Data.Singletons.Prelude> :kind! Bar
Bar :: *
= NewType ('A :$$$ '['B])
```
----
If inline `StripNatList` inside `Family` definition:
```hs
type family Family (natList :: NatList) = (r :: Type) | r -> natList where
Family '[] = ()
Family xs = NewType (Map SndSym0 xs)
```
or change `StripNatList` definition to type family:
```hs
type family StripNatList (natList :: NatList) where
StripNatList '[] = '[]
StripNatList ('(n, x) ': xs) = x ': StripNatList xs
```
compilation expectedly fails with `Type family equation violates injectivity annotation.`
----
Moreover, if I remove `NewType` from `Family` and change result kind:
```hs
type family Family (natList :: NatList) = (r :: [Payload]) | r -> natList where
Family xs = StripNatList xs
```
it fails with correct error regardless of `StripNatList` definition.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | jstolarek |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeFamilyDependencies accepts invalid injectivity annotation","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["jstolarek"],"type":"Bug","description":"Consider this code (depends on singletons-2.2):\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators,\r\nKindSignatures, TypeInType, TypeFamilyDependencies, UndecidableInstances #-}\r\n\r\nmodule Bug where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Singletons.Prelude (Map, SndSym0)\r\nimport GHC.TypeLits (Nat)\r\n\r\ndata Payload = A | B\r\n\r\nnewtype NewType a = NewType Int\r\n\r\ntype NatList = [(Nat, Payload)]\r\n\r\ntype StripNatList (natList :: NatList) = Map SndSym0 natList\r\n\r\ntype family Family (natList :: NatList) = (r :: Type) | r -> natList where\r\n Family '[] = ()\r\n Family xs = NewType (StripNatList xs) \r\n}}}\r\n\r\nWhy GHC is okay with injectivity annotation for `Family`: `r -> natList`?\r\n\r\nThese two types:\r\n\r\n{{{#!hs\r\ntype Foo = Family '[ '(0, 'A), '(1, 'B)]\r\ntype Bar = Family '[ '(0, 'A), '(0, 'B)]\r\n}}}\r\nare obviously map to the same type:\r\n\r\n{{{#!hs\r\n*Bug Data.Singletons.Prelude> :kind! Foo\r\nFoo :: *\r\n= NewType ('A :$$$ '['B])\r\n*Bug Data.Singletons.Prelude> :kind! Bar\r\nBar :: *\r\n= NewType ('A :$$$ '['B])\r\n}}}\r\n----\r\nIf inline `StripNatList` inside `Family` definition:\r\n{{{#!hs\r\ntype family Family (natList :: NatList) = (r :: Type) | r -> natList where\r\n Family '[] = ()\r\n Family xs = NewType (Map SndSym0 xs)\r\n}}}\r\nor change `StripNatList` definition to type family:\r\n{{{#!hs\r\ntype family StripNatList (natList :: NatList) where\r\n StripNatList '[] = '[]\r\n StripNatList ('(n, x) ': xs) = x ': StripNatList xs\r\n}}}\r\ncompilation expectedly fails with `Type family equation violates injectivity annotation.`\r\n----\r\nMoreover, if I remove `NewType` from `Family` and change result kind:\r\n{{{#!hs\r\ntype family Family (natList :: NatList) = (r :: [Payload]) | r -> natList where\r\n Family xs = StripNatList xs\r\n}}}\r\nit fails with correct error regardless of `StripNatList` definition.","type_of_failure":"OtherFailure","blocking":[]} -->
8.8.1