GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:59:48Zhttps://gitlab.haskell.org/ghc/ghc//issues/4259Relax restrictions on type family instance overlap20190707T18:59:48ZlilacRelax restrictions on type family instance overlapThe following reduced fragment of some real code is rejected, but could be accepted, by GHC:
```
{# LANGUAGE TypeFamilies, EmptyDataDecls #}
data True
type family LessEq a b :: *
type instance LessEq a a = True
type instance LessEq (f a) (f b) = LessEq a b
```
GHC says:
```
Conflicting family instance declarations:
type instance LessEq a a
 Defined at /home/richards/.random/tf.hs:5:1419
type instance LessEq (f a) (f b)
 Defined at /home/richards/.random/tf.hs:6:1419
```
This is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.
In particular (absent XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.
In order to retain soundness in the presence of XUndecidableInstances, any pair of type instances, where either instance could not be compiled without XUndecidableInstances, would continue to use the current syntactic equality rule.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  6.12.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family instance conflict checks could be smarter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The following reduced fragment of some real code is rejected, but could be accepted, by GHC:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies, EmptyDataDecls #}\r\ndata True\r\n\r\ntype family LessEq a b :: *\r\ntype instance LessEq a a = True\r\ntype instance LessEq (f a) (f b) = LessEq a b\r\n}}}\r\n\r\nGHC says:\r\n\r\n{{{\r\n Conflicting family instance declarations:\r\n type instance LessEq a a\r\n  Defined at /home/richards/.random/tf.hs:5:1419\r\n type instance LessEq (f a) (f b)\r\n  Defined at /home/richards/.random/tf.hs:6:1419\r\n}}}\r\n\r\nThis is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.\r\n\r\nIn particular (absent XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.\r\n\r\nIn order to retain soundness in the presence of XUndecidableInstances, any pair of type instances, where either instance could not be compiled without XUndecidableInstances, would continue to use the current syntactic equality rule.","type_of_failure":"OtherFailure","blocking":[]} >The following reduced fragment of some real code is rejected, but could be accepted, by GHC:
```
{# LANGUAGE TypeFamilies, EmptyDataDecls #}
data True
type family LessEq a b :: *
type instance LessEq a a = True
type instance LessEq (f a) (f b) = LessEq a b
```
GHC says:
```
Conflicting family instance declarations:
type instance LessEq a a
 Defined at /home/richards/.random/tf.hs:5:1419
type instance LessEq (f a) (f b)
 Defined at /home/richards/.random/tf.hs:6:1419
```
This is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.
In particular (absent XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.
In order to retain soundness in the presence of XUndecidableInstances, any pair of type instances, where either instance could not be compiled without XUndecidableInstances, would continue to use the current syntactic equality rule.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  6.12.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family instance conflict checks could be smarter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The following reduced fragment of some real code is rejected, but could be accepted, by GHC:\r\n\r\n{{{\r\n{# LANGUAGE TypeFamilies, EmptyDataDecls #}\r\ndata True\r\n\r\ntype family LessEq a b :: *\r\ntype instance LessEq a a = True\r\ntype instance LessEq (f a) (f b) = LessEq a b\r\n}}}\r\n\r\nGHC says:\r\n\r\n{{{\r\n Conflicting family instance declarations:\r\n type instance LessEq a a\r\n  Defined at /home/richards/.random/tf.hs:5:1419\r\n type instance LessEq (f a) (f b)\r\n  Defined at /home/richards/.random/tf.hs:6:1419\r\n}}}\r\n\r\nThis is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.\r\n\r\nIn particular (absent XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.\r\n\r\nIn order to retain soundness in the presence of XUndecidableInstances, any pair of type instances, where either instance could not be compiled without XUndecidableInstances, would continue to use the current syntactic equality rule.","type_of_failure":"OtherFailure","blocking":[]} >8.0.1https://gitlab.haskell.org/ghc/ghc//issues/10227Type checker cannot deduce type20190707T18:37:00Zlennart@augustsson.netType checker cannot deduce typeWhen using closed type families the type checker does not use all the information that the closedness condition implies.
In the following module the type checker fails to deduce the type for `f`.
But lets start with `descrIn` since it has the same problem. The deduced type is `(D d Bool ~ Bool, D d Double ~ Bool, D d (Maybe String) ~ Bool) => Descr d`. But it is (to quote Simon PJ) plain as a pikestaff that `D d Double ~ Bool` can only hold if `d ~ In`, since there are only two equations and it cannot be the second.
Similar reasoning can be used to deduce all the commented out type signatures.
```hs
{# LANGUAGE RecordWildCards, TypeFamilies, DataKinds, NoMonomorphismRestriction, FlexibleContexts #}
module Main(main) where
import Data.Maybe
data InOut = In  Out
type family D (d :: InOut) a where
D 'In a = Bool
D 'Out a = a
data Descr d = Descr {
abc :: D d Bool,
def :: D d Double,
ghi :: D d (Maybe String)
}
descrIn :: Descr 'In
descrIn = Descr { abc = False, def = True, ghi = True }
f :: Descr 'Out > Double
f Descr{..} = def + read (fromMaybe "0" ghi)
g :: Descr 'In > Descr 'Out
g d = Descr { abc = if abc d then True else False,
def = if def d then 1234 else 0,
ghi = if ghi d then Just "3008" else Nothing }
main :: IO ()
main = do
print $ f $ g descrIn
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type checker cannot deduce type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When using closed type families the type checker does not use all the information that the closedness condition implies.\r\n\r\nIn the following module the type checker fails to deduce the type for `f`.\r\n\r\nBut lets start with `descrIn` since it has the same problem. The deduced type is `(D d Bool ~ Bool, D d Double ~ Bool, D d (Maybe String) ~ Bool) => Descr d`. But it is (to quote Simon PJ) plain as a pikestaff that `D d Double ~ Bool` can only hold if `d ~ In`, since there are only two equations and it cannot be the second.\r\n\r\nSimilar reasoning can be used to deduce all the commented out type signatures.\r\n\r\n{{{#!hs\r\n{# LANGUAGE RecordWildCards, TypeFamilies, DataKinds, NoMonomorphismRestriction, FlexibleContexts #}\r\nmodule Main(main) where\r\nimport Data.Maybe\r\n\r\ndata InOut = In  Out\r\n\r\ntype family D (d :: InOut) a where\r\n D 'In a = Bool\r\n D 'Out a = a\r\n\r\ndata Descr d = Descr {\r\n abc :: D d Bool,\r\n def :: D d Double,\r\n ghi :: D d (Maybe String)\r\n }\r\n\r\ndescrIn :: Descr 'In\r\ndescrIn = Descr { abc = False, def = True, ghi = True }\r\n\r\nf :: Descr 'Out > Double\r\nf Descr{..} = def + read (fromMaybe \"0\" ghi)\r\n\r\ng :: Descr 'In > Descr 'Out\r\ng d = Descr { abc = if abc d then True else False,\r\n def = if def d then 1234 else 0,\r\n ghi = if ghi d then Just \"3008\" else Nothing }\r\n\r\nmain :: IO ()\r\nmain = do\r\n print $ f $ g descrIn\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >When using closed type families the type checker does not use all the information that the closedness condition implies.
In the following module the type checker fails to deduce the type for `f`.
But lets start with `descrIn` since it has the same problem. The deduced type is `(D d Bool ~ Bool, D d Double ~ Bool, D d (Maybe String) ~ Bool) => Descr d`. But it is (to quote Simon PJ) plain as a pikestaff that `D d Double ~ Bool` can only hold if `d ~ In`, since there are only two equations and it cannot be the second.
Similar reasoning can be used to deduce all the commented out type signatures.
```hs
{# LANGUAGE RecordWildCards, TypeFamilies, DataKinds, NoMonomorphismRestriction, FlexibleContexts #}
module Main(main) where
import Data.Maybe
data InOut = In  Out
type family D (d :: InOut) a where
D 'In a = Bool
D 'Out a = a
data Descr d = Descr {
abc :: D d Bool,
def :: D d Double,
ghi :: D d (Maybe String)
}
descrIn :: Descr 'In
descrIn = Descr { abc = False, def = True, ghi = True }
f :: Descr 'Out > Double
f Descr{..} = def + read (fromMaybe "0" ghi)
g :: Descr 'In > Descr 'Out
g d = Descr { abc = if abc d then True else False,
def = if def d then 1234 else 0,
ghi = if ghi d then Just "3008" else Nothing }
main :: IO ()
main = do
print $ f $ g descrIn
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type checker cannot deduce type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When using closed type families the type checker does not use all the information that the closedness condition implies.\r\n\r\nIn the following module the type checker fails to deduce the type for `f`.\r\n\r\nBut lets start with `descrIn` since it has the same problem. The deduced type is `(D d Bool ~ Bool, D d Double ~ Bool, D d (Maybe String) ~ Bool) => Descr d`. But it is (to quote Simon PJ) plain as a pikestaff that `D d Double ~ Bool` can only hold if `d ~ In`, since there are only two equations and it cannot be the second.\r\n\r\nSimilar reasoning can be used to deduce all the commented out type signatures.\r\n\r\n{{{#!hs\r\n{# LANGUAGE RecordWildCards, TypeFamilies, DataKinds, NoMonomorphismRestriction, FlexibleContexts #}\r\nmodule Main(main) where\r\nimport Data.Maybe\r\n\r\ndata InOut = In  Out\r\n\r\ntype family D (d :: InOut) a where\r\n D 'In a = Bool\r\n D 'Out a = a\r\n\r\ndata Descr d = Descr {\r\n abc :: D d Bool,\r\n def :: D d Double,\r\n ghi :: D d (Maybe String)\r\n }\r\n\r\ndescrIn :: Descr 'In\r\ndescrIn = Descr { abc = False, def = True, ghi = True }\r\n\r\nf :: Descr 'Out > Double\r\nf Descr{..} = def + read (fromMaybe \"0\" ghi)\r\n\r\ng :: Descr 'In > Descr 'Out\r\ng d = Descr { abc = if abc d then True else False,\r\n def = if def d then 1234 else 0,\r\n ghi = if ghi d then Just \"3008\" else Nothing }\r\n\r\nmain :: IO ()\r\nmain = do\r\n print $ f $ g descrIn\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/10832Generalize injective type families20201209T23:11:31ZJan Stolarekjan.stolarek@ed.ac.ukGeneralize injective type familiesWith injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero  Succ a
class Add a b r  a b > r, r a > b
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r)
```
Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:
```hs
type family AddTF a b = r  r a > b where
AddTF Zero b = b
AddTF (Succ a) b = Succ (AddTF a b)
```
But we want to be able to say that.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.11 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Generalize injective type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:\r\n\r\n{{{#!hs\r\ndata Nat = Zero  Succ a\r\n\r\nclass Add a b r  a b > r, r a > b\r\ninstance Add Zero b b\r\ninstance (Add a b r) => Add (Succ a) b (Succ r)\r\n}}}\r\nHere we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:\r\n\r\n{{{#!hs\r\ntype family AddTF a b = r  r a > b where\r\n AddTF Zero b = b\r\n AddTF (Succ a) b = Succ (AddTF a b)\r\n}}}\r\nBut we want to be able to say that.","type_of_failure":"OtherFailure","blocking":[]} >With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero  Succ a
class Add a b r  a b > r, r a > b
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r)
```
Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:
```hs
type family AddTF a b = r  r a > b where
AddTF Zero b = b
AddTF (Succ a) b = Succ (AddTF a b)
```
But we want to be able to say that.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.11 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Generalize injective type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:\r\n\r\n{{{#!hs\r\ndata Nat = Zero  Succ a\r\n\r\nclass Add a b r  a b > r, r a > b\r\ninstance Add Zero b b\r\ninstance (Add a b r) => Add (Succ a) b (Succ r)\r\n}}}\r\nHere we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:\r\n\r\n{{{#!hs\r\ntype family AddTF a b = r  r a > b where\r\n AddTF Zero b = b\r\n AddTF (Succ a) b = Succ (AddTF a b)\r\n}}}\r\nBut we want to be able to say that.","type_of_failure":"OtherFailure","blocking":[]} >Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc//issues/10833Use injective type families (decomposition) when dealing with givens20200317T22:24:40ZJan Stolarekjan.stolarek@ed.ac.ukUse injective type families (decomposition) when dealing with givensConsider this code:
```hs
type family Id a = r  r > a
id :: (Id a ~ Id b) => a > b
id x = x
```
GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.2 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #6018 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Use injective type families when dealing with givens","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[6018],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\ntype family Id a = r  r > a\r\n\r\nid :: (Id a ~ Id b) => a > b\r\nid x = x\r\n}}}\r\nGHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code:
```hs
type family Id a = r  r > a
id :: (Id a ~ Id b) => a > b
id x = x
```
GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.2 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #6018 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Use injective type families when dealing with givens","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[6018],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\ntype family Id a = r  r > a\r\n\r\nid :: (Id a ~ Id b) => a > b\r\nid x = x\r\n}}}\r\nGHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core.","type_of_failure":"OtherFailure","blocking":[]} >Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc//issues/11511Type family producing infinite type accepted as injective20190707T18:30:07ZJan Stolarekjan.stolarek@ed.ac.ukType family producing infinite type accepted as injectiveA question came up during discussion at University of Wrocław:
```hs
type family F a = r  r > a where
F a = [F a]
```
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.
This is not an implementation problem  this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family producing infinite type accepted as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Injective","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"Bug","description":"A question came up during discussion at University of Wrocław:\r\n\r\n\r\n{{{#!hs\r\ntype family F a = r  r > a where\r\n F a = [F a]\r\n}}}\r\n\r\nShould this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.\r\n\r\nThis is not an implementation problem  this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.","type_of_failure":"OtherFailure","blocking":[]} >A question came up during discussion at University of Wrocław:
```hs
type family F a = r  r > a where
F a = [F a]
```
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.
This is not an implementation problem  this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family producing infinite type accepted as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Injective","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"Bug","description":"A question came up during discussion at University of Wrocław:\r\n\r\n\r\n{{{#!hs\r\ntype family F a = r  r > a where\r\n F a = [F a]\r\n}}}\r\n\r\nShould this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.\r\n\r\nThis is not an implementation problem  this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/13621Problems with injective type families20190707T18:20:54ZIcelandjackProblems with injective type families```hs
{# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilyDependencies #}
import Data.Kind
type family
IB a = res  res > a where
IB Int = Bool
IB Bool = Int
type Cat k = k > k > Type
data F :: Cat Type where
F :: (a > IB a) > F a (IB a)
data Exp :: Type > Type where
I :: Int > Exp Int
B :: Bool > Exp Bool
fmap' :: F a b > (Exp a > Exp b)
fmap' (F f) = \case
B b > I (f b)
I i > B (f i)
```
I would have thought this should work as well, given that `IB` is injective:
```hs
data F :: Cat Type where
F :: (IB a > a) > F (IB a) a
```
but it gives
```hs
fmap' :: F a b > (Exp a > Exp b)
fmap' (F f) = \case
B b > I (f b)
 c.hs:33:13: error:
 • Could not deduce: b ~ Int
 from the context: a ~ IB b
 bound by a pattern with constructor:
 F :: forall a. (IB a > a) > F (IB a) a,
 in an equation for ‘fmap'’
 at c.hs:32:810
 or from: a ~ Bool
 bound by a pattern with constructor: B :: Bool > Exp Bool,
 in a case alternative
 at c.hs:33:35
 ‘b’ is a rigid type variable bound by
 the type signature for:
 fmap' :: forall a b. F a b > Exp a > Exp b
 at c.hs:31:10
 • In the first argument of ‘I’, namely ‘(f b)’
 In the expression: I (f b)
 In a case alternative: B b > I (f b)
 • Relevant bindings include
 f :: IB b > b (bound at c.hs:32:10)
 fmap' :: F a b > Exp a > Exp b (bound at c.hs:32:1)
 Failed, modules loaded: none.
```
But if we know that `a ~ Bool` (as we do from matching on `B`), and we know that `a ~ IB b` then by injectivity it should figure that `b ~ Int`?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Problems with injective type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilyDependencies #}\r\n\r\nimport Data.Kind\r\n\r\ntype family\r\n IB a = res  res > a where\r\n IB Int = Bool\r\n IB Bool = Int\r\n\r\ntype Cat k = k > k > Type\r\n\r\ndata F :: Cat Type where\r\n F :: (a > IB a) > F a (IB a)\r\n\r\ndata Exp :: Type > Type where\r\n I :: Int > Exp Int\r\n B :: Bool > Exp Bool\r\n\r\nfmap' :: F a b > (Exp a > Exp b)\r\nfmap' (F f) = \\case\r\n B b > I (f b)\r\n I i > B (f i)\r\n}}}\r\n\r\nI would have thought this should work as well, given that `IB` is injective:\r\n\r\n{{{#!hs\r\ndata F :: Cat Type where\r\n F :: (IB a > a) > F (IB a) a\r\n}}}\r\n\r\nbut it gives\r\n\r\n{{{#!hs\r\nfmap' :: F a b > (Exp a > Exp b)\r\nfmap' (F f) = \\case\r\n B b > I (f b)\r\n\r\n c.hs:33:13: error:\r\n • Could not deduce: b ~ Int\r\n from the context: a ~ IB b\r\n bound by a pattern with constructor:\r\n F :: forall a. (IB a > a) > F (IB a) a,\r\n in an equation for ‘fmap'’\r\n at c.hs:32:810\r\n or from: a ~ Bool\r\n bound by a pattern with constructor: B :: Bool > Exp Bool,\r\n in a case alternative\r\n at c.hs:33:35\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n fmap' :: forall a b. F a b > Exp a > Exp b\r\n at c.hs:31:10\r\n • In the first argument of ‘I’, namely ‘(f b)’\r\n In the expression: I (f b)\r\n In a case alternative: B b > I (f b)\r\n • Relevant bindings include\r\n f :: IB b > b (bound at c.hs:32:10)\r\n fmap' :: F a b > Exp a > Exp b (bound at c.hs:32:1)\r\n Failed, modules loaded: none.\r\n}}}\r\n\r\nBut if we know that `a ~ Bool` (as we do from matching on `B`), and we know that `a ~ IB b` then by injectivity it should figure that `b ~ Int`?","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilyDependencies #}
import Data.Kind
type family
IB a = res  res > a where
IB Int = Bool
IB Bool = Int
type Cat k = k > k > Type
data F :: Cat Type where
F :: (a > IB a) > F a (IB a)
data Exp :: Type > Type where
I :: Int > Exp Int
B :: Bool > Exp Bool
fmap' :: F a b > (Exp a > Exp b)
fmap' (F f) = \case
B b > I (f b)
I i > B (f i)
```
I would have thought this should work as well, given that `IB` is injective:
```hs
data F :: Cat Type where
F :: (IB a > a) > F (IB a) a
```
but it gives
```hs
fmap' :: F a b > (Exp a > Exp b)
fmap' (F f) = \case
B b > I (f b)
 c.hs:33:13: error:
 • Could not deduce: b ~ Int
 from the context: a ~ IB b
 bound by a pattern with constructor:
 F :: forall a. (IB a > a) > F (IB a) a,
 in an equation for ‘fmap'’
 at c.hs:32:810
 or from: a ~ Bool
 bound by a pattern with constructor: B :: Bool > Exp Bool,
 in a case alternative
 at c.hs:33:35
 ‘b’ is a rigid type variable bound by
 the type signature for:
 fmap' :: forall a b. F a b > Exp a > Exp b
 at c.hs:31:10
 • In the first argument of ‘I’, namely ‘(f b)’
 In the expression: I (f b)
 In a case alternative: B b > I (f b)
 • Relevant bindings include
 f :: IB b > b (bound at c.hs:32:10)
 fmap' :: F a b > Exp a > Exp b (bound at c.hs:32:1)
 Failed, modules loaded: none.
```
But if we know that `a ~ Bool` (as we do from matching on `B`), and we know that `a ~ IB b` then by injectivity it should figure that `b ~ Int`?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Problems with injective type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilyDependencies #}\r\n\r\nimport Data.Kind\r\n\r\ntype family\r\n IB a = res  res > a where\r\n IB Int = Bool\r\n IB Bool = Int\r\n\r\ntype Cat k = k > k > Type\r\n\r\ndata F :: Cat Type where\r\n F :: (a > IB a) > F a (IB a)\r\n\r\ndata Exp :: Type > Type where\r\n I :: Int > Exp Int\r\n B :: Bool > Exp Bool\r\n\r\nfmap' :: F a b > (Exp a > Exp b)\r\nfmap' (F f) = \\case\r\n B b > I (f b)\r\n I i > B (f i)\r\n}}}\r\n\r\nI would have thought this should work as well, given that `IB` is injective:\r\n\r\n{{{#!hs\r\ndata F :: Cat Type where\r\n F :: (IB a > a) > F (IB a) a\r\n}}}\r\n\r\nbut it gives\r\n\r\n{{{#!hs\r\nfmap' :: F a b > (Exp a > Exp b)\r\nfmap' (F f) = \\case\r\n B b > I (f b)\r\n\r\n c.hs:33:13: error:\r\n • Could not deduce: b ~ Int\r\n from the context: a ~ IB b\r\n bound by a pattern with constructor:\r\n F :: forall a. (IB a > a) > F (IB a) a,\r\n in an equation for ‘fmap'’\r\n at c.hs:32:810\r\n or from: a ~ Bool\r\n bound by a pattern with constructor: B :: Bool > Exp Bool,\r\n in a case alternative\r\n at c.hs:33:35\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n fmap' :: forall a b. F a b > Exp a > Exp b\r\n at c.hs:31:10\r\n • In the first argument of ‘I’, namely ‘(f b)’\r\n In the expression: I (f b)\r\n In a case alternative: B b > I (f b)\r\n • Relevant bindings include\r\n f :: IB b > b (bound at c.hs:32:10)\r\n fmap' :: F a b > Exp a > Exp b (bound at c.hs:32:1)\r\n Failed, modules loaded: none.\r\n}}}\r\n\r\nBut if we know that `a ~ Bool` (as we do from matching on `B`), and we know that `a ~ IB b` then by injectivity it should figure that `b ~ Int`?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/13797Mark negation injective20200317T22:19:50ZIcelandjackMark negation injective```hs
{# Language DataKinds, TypeOperators, TypeFamilyDependencies, UndecidableInstances #}
import GHC.TypeLits
data N = O  S N
type family
U (a :: Nat) = (res :: N)  res > a where
U 0 = O
U n = S (U (n1))
```
gives
```
olates injectivity annotation.
Type variable ‘n’ cannot be inferred from the righthand side.
In the type family equation:
U n = 'S (U (n  1))  Defined at /tmp/a.hs:37:3
• In the equations for closed type family ‘U’
In the type family declaration for ‘U’
Failed, modules loaded: none.
```
I expect this to work, this depends on making `()` injective which depends on ["generalized injectivity"](https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies#Futureplansandideas)?
```hs
type family
(a :: Nat)  (b :: Nat) = (res :: Nat)  a b > res, res a > b, res b > a where
{ built in }
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Mark negation injective","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language DataKinds, TypeOperators, TypeFamilyDependencies, UndecidableInstances #}\r\n\r\nimport GHC.TypeLits\r\n\r\ndata N = O  S N\r\n\r\ntype family\r\n U (a :: Nat) = (res :: N)  res > a where\r\n U 0 = O\r\n U n = S (U (n1))\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\nolates injectivity annotation.\r\n Type variable ‘n’ cannot be inferred from the righthand side.\r\n In the type family equation:\r\n U n = 'S (U (n  1))  Defined at /tmp/a.hs:37:3\r\n • In the equations for closed type family ‘U’\r\n In the type family declaration for ‘U’\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nI expect this to work, this depends on making `()` injective which depends on [https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies#Futureplansandideas \"generalized injectivity\"]?\r\n\r\n{{{#!hs\r\ntype family\r\n (a :: Nat)  (b :: Nat) = (res :: Nat)  a b > res, res a > b, res b > a where\r\n { built in }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language DataKinds, TypeOperators, TypeFamilyDependencies, UndecidableInstances #}
import GHC.TypeLits
data N = O  S N
type family
U (a :: Nat) = (res :: N)  res > a where
U 0 = O
U n = S (U (n1))
```
gives
```
olates injectivity annotation.
Type variable ‘n’ cannot be inferred from the righthand side.
In the type family equation:
U n = 'S (U (n  1))  Defined at /tmp/a.hs:37:3
• In the equations for closed type family ‘U’
In the type family declaration for ‘U’
Failed, modules loaded: none.
```
I expect this to work, this depends on making `()` injective which depends on ["generalized injectivity"](https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies#Futureplansandideas)?
```hs
type family
(a :: Nat)  (b :: Nat) = (res :: Nat)  a b > res, res a > b, res b > a where
{ built in }
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Mark negation injective","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language DataKinds, TypeOperators, TypeFamilyDependencies, UndecidableInstances #}\r\n\r\nimport GHC.TypeLits\r\n\r\ndata N = O  S N\r\n\r\ntype family\r\n U (a :: Nat) = (res :: N)  res > a where\r\n U 0 = O\r\n U n = S (U (n1))\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\nolates injectivity annotation.\r\n Type variable ‘n’ cannot be inferred from the righthand side.\r\n In the type family equation:\r\n U n = 'S (U (n  1))  Defined at /tmp/a.hs:37:3\r\n • In the equations for closed type family ‘U’\r\n In the type family declaration for ‘U’\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nI expect this to work, this depends on making `()` injective which depends on [https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies#Futureplansandideas \"generalized injectivity\"]?\r\n\r\n{{{#!hs\r\ntype family\r\n (a :: Nat)  (b :: Nat) = (res :: Nat)  a b > res, res a > b, res b > a where\r\n { built in }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14164GHC hangs on type family dependency20200123T19:31:02ZIcelandjackGHC hangs on type family dependency```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 _) = '[]
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 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  
</details>
<! {"blocked_by":[],"summary":"GHC hangs on type family dependency","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language TypeOperators, DataKinds, PolyKinds, KindSignatures, TypeInType, GADTs, TypeFamilyDependencies #}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat a = a > a > Type\r\n\r\ndata SubList :: Cat [a] where\r\n SubNil :: SubList '[] '[]\r\n Keep :: SubList xs ys > SubList (x:xs) (x:ys)\r\n Drop :: SubList xs ys > SubList xs (x:ys)\r\n\r\ntype family \r\n UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a])  res > pf ys' xs where\r\n UpdateWith '[] '[] SubNil = '[]\r\n UpdateWith (y:ys) '[] SubNil = y:ys\r\n  UpdateWith '[] (_:_) (Keep _) = '[]\r\n UpdateWith (y:ys) (_:xs) (Keep rest) = y:UpdateWith ys xs rest\r\n  UpdateWith ys (x:xs) (Drop rest) = x:UpdateWith ys xs rest\r\n}}}\r\n\r\nseems to loop forever on the \"`Renamer/typechecker`\"\r\n\r\n{{{\r\n$ ghci ignoredotghci v /tmp/u.hs \r\nGHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help\r\nGlasgow Haskell Compiler, Version 8.3.20170605, stage 2 booted by GHC version 8.0.2\r\n\r\n[...]\r\n\r\n*** Parser [Main]:\r\n!!! Parser [Main]: finished in 1.31 milliseconds, allocated 0.651 megabytes\r\n*** Renamer/typechecker [Main]:\r\n\r\n[hangs]\r\n}}}\r\n\r\nwhile \r\n\r\n{{{#!hs\r\ntype family \r\n UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a])  res > pf ys' xs where\r\n UpdateWith '[] '[] SubNil = '[]\r\n UpdateWith (y:ys) '[] SubNil = y:ys\r\n UpdateWith '[] (_:_) (Keep _) = '[]\r\n}}}\r\n\r\nimmediately gives\r\n\r\n{{{\r\n$ ghc ignoredotghci /tmp/u.hs \r\n[1 of 1] Compiling Main ( /tmp/u.hs, /tmp/u.o )\r\n\r\n/tmp/u.hs:14:3: error:\r\n • Type family equations violate injectivity annotation:\r\n UpdateWith '[] '[] 'SubNil = '[]  Defined at /tmp/u.hs:14:3\r\n forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).\r\n UpdateWith '[] (_2 : _1) ('Keep _3) = '[]\r\n  Defined at /tmp/u.hs:16:3\r\n • In the equations for closed type family ‘UpdateWith’\r\n In the type family declaration for ‘UpdateWith’\r\n \r\n14  UpdateWith '[] '[] SubNil = '[]\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\n/tmp/u.hs:16:3: error:\r\n • Type family equation violates injectivity annotation.\r\n Type and kind variables ‘_2’, ‘_1’, ‘xs’, ‘_3’\r\n cannot be inferred from the righthand side.\r\n Use fprintexplicitkinds to see the kind arguments\r\n In the type family equation:\r\n forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).\r\n UpdateWith '[] (_2 : _1) ('Keep _3) = '[]\r\n  Defined at /tmp/u.hs:16:3\r\n • In the equations for closed type family ‘UpdateWith’\r\n In the type family declaration for ‘UpdateWith’\r\n \r\n16  UpdateWith '[] (_:_) (Keep _) = '[]\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```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 _) = '[]
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 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  
</details>
<! {"blocked_by":[],"summary":"GHC hangs on type family dependency","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language TypeOperators, DataKinds, PolyKinds, KindSignatures, TypeInType, GADTs, TypeFamilyDependencies #}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat a = a > a > Type\r\n\r\ndata SubList :: Cat [a] where\r\n SubNil :: SubList '[] '[]\r\n Keep :: SubList xs ys > SubList (x:xs) (x:ys)\r\n Drop :: SubList xs ys > SubList xs (x:ys)\r\n\r\ntype family \r\n UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a])  res > pf ys' xs where\r\n UpdateWith '[] '[] SubNil = '[]\r\n UpdateWith (y:ys) '[] SubNil = y:ys\r\n  UpdateWith '[] (_:_) (Keep _) = '[]\r\n UpdateWith (y:ys) (_:xs) (Keep rest) = y:UpdateWith ys xs rest\r\n  UpdateWith ys (x:xs) (Drop rest) = x:UpdateWith ys xs rest\r\n}}}\r\n\r\nseems to loop forever on the \"`Renamer/typechecker`\"\r\n\r\n{{{\r\n$ ghci ignoredotghci v /tmp/u.hs \r\nGHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help\r\nGlasgow Haskell Compiler, Version 8.3.20170605, stage 2 booted by GHC version 8.0.2\r\n\r\n[...]\r\n\r\n*** Parser [Main]:\r\n!!! Parser [Main]: finished in 1.31 milliseconds, allocated 0.651 megabytes\r\n*** Renamer/typechecker [Main]:\r\n\r\n[hangs]\r\n}}}\r\n\r\nwhile \r\n\r\n{{{#!hs\r\ntype family \r\n UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a])  res > pf ys' xs where\r\n UpdateWith '[] '[] SubNil = '[]\r\n UpdateWith (y:ys) '[] SubNil = y:ys\r\n UpdateWith '[] (_:_) (Keep _) = '[]\r\n}}}\r\n\r\nimmediately gives\r\n\r\n{{{\r\n$ ghc ignoredotghci /tmp/u.hs \r\n[1 of 1] Compiling Main ( /tmp/u.hs, /tmp/u.o )\r\n\r\n/tmp/u.hs:14:3: error:\r\n • Type family equations violate injectivity annotation:\r\n UpdateWith '[] '[] 'SubNil = '[]  Defined at /tmp/u.hs:14:3\r\n forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).\r\n UpdateWith '[] (_2 : _1) ('Keep _3) = '[]\r\n  Defined at /tmp/u.hs:16:3\r\n • In the equations for closed type family ‘UpdateWith’\r\n In the type family declaration for ‘UpdateWith’\r\n \r\n14  UpdateWith '[] '[] SubNil = '[]\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\n/tmp/u.hs:16:3: error:\r\n • Type family equation violates injectivity annotation.\r\n Type and kind variables ‘_2’, ‘_1’, ‘xs’, ‘_3’\r\n cannot be inferred from the righthand side.\r\n Use fprintexplicitkinds to see the kind arguments\r\n In the type family equation:\r\n forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).\r\n UpdateWith '[] (_2 : _1) ('Keep _3) = '[]\r\n  Defined at /tmp/u.hs:16:3\r\n • In the equations for closed type family ‘UpdateWith’\r\n In the type family declaration for ‘UpdateWith’\r\n \r\n16  UpdateWith '[] (_:_) (Keep _) = '[]\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16436Pattern matching breaks injective type families20191221T17:31:05ZVladislav ZavialovPattern matching breaks injective type families```
{# LANGUAGE TypeFamilyDependencies, TypeOperators, DataKinds, GADTs, TypeApplications #}
data HList xs where
HNil :: HList '[]
HCons :: x > HList xs > HList (x:xs)
type family ListId xs = ys  ys > xs
where
ListId '[] = '[]
ListId (x:xs) = (x : ListId xs)
f :: HList (ListId ts) > ()
f a =
case a of
HNil > ()
 z@(HCons _ _) > f z  uncomment to break
z > f z
```
While `z > f z` works, pattern matching on `HCons` breaks it:
```
A.hs:16:24: error:
• Could not deduce: ListId xs ~ xs1
from the context: ListId ts ~ (x : xs1)
bound by a pattern with constructor:
HCons :: forall x (xs :: [*]). x > HList xs > HList (x : xs),
in a case alternative
at A.hs:16:816
‘xs1’ is a rigid type variable bound by
a pattern with constructor:
HCons :: forall x (xs :: [*]). x > HList xs > HList (x : xs),
in a case alternative
at A.hs:16:816
Expected type: HList (ListId (x : xs))
Actual type: HList (ListId ts)
• In the first argument of ‘f’, namely ‘z’
In the expression: f z
In a case alternative: z@(HCons _ _) > f z

16  z@(HCons _ _) > f z
 ^
``````
{# LANGUAGE TypeFamilyDependencies, TypeOperators, DataKinds, GADTs, TypeApplications #}
data HList xs where
HNil :: HList '[]
HCons :: x > HList xs > HList (x:xs)
type family ListId xs = ys  ys > xs
where
ListId '[] = '[]
ListId (x:xs) = (x : ListId xs)
f :: HList (ListId ts) > ()
f a =
case a of
HNil > ()
 z@(HCons _ _) > f z  uncomment to break
z > f z
```
While `z > f z` works, pattern matching on `HCons` breaks it:
```
A.hs:16:24: error:
• Could not deduce: ListId xs ~ xs1
from the context: ListId ts ~ (x : xs1)
bound by a pattern with constructor:
HCons :: forall x (xs :: [*]). x > HList xs > HList (x : xs),
in a case alternative
at A.hs:16:816
‘xs1’ is a rigid type variable bound by
a pattern with constructor:
HCons :: forall x (xs :: [*]). x > HList xs > HList (x : xs),
in a case alternative
at A.hs:16:816
Expected type: HList (ListId (x : xs))
Actual type: HList (ListId ts)
• In the first argument of ‘f’, namely ‘z’
In the expression: f z
In a case alternative: z@(HCons _ _) > f z

16  z@(HCons _ _) > f z
 ^
```https://gitlab.haskell.org/ghc/ghc//issues/17186Another loop with injective type families20201110T15:28:13ZRichard Eisenbergrae@richarde.devAnother loop with injective type familiesBroken out from #16512, the following program causes GHC to loop:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE TypeOperators, AllowAmbiguousTypes #}
module T16512 where
 This test is significantly abbreviated from what was posted; see
 #16512 for more context.
type family Dim v
type family v `OfDim` (n :: Dim v) = r  r > n
(!*^) :: Dim m `OfDim` j > Dim m `OfDim` i
(!*^) = undefined
```
The fix for #16512 does not fix this.Broken out from #16512, the following program causes GHC to loop:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE TypeOperators, AllowAmbiguousTypes #}
module T16512 where
 This test is significantly abbreviated from what was posted; see
 #16512 for more context.
type family Dim v
type family v `OfDim` (n :: Dim v) = r  r > n
(!*^) :: Dim m `OfDim` j > Dim m `OfDim` i
(!*^) = undefined
```
The fix for #16512 does not fix this.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev