GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200117T16:43:24Zhttps://gitlab.haskell.org/ghc/ghc//issues/15883GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)20200117T16:43:24ZIcelandjackGHC panic: newtype F rep = F (forall (a :: TYPE rep). a)```hs
{# Language RankNTypes #}
{# Language KindSignatures #}
{# Language PolyKinds #}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64unknownlinux):
isUnliftedType
forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type
isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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 panic: newtype F rep = F (forall (a :: TYPE rep). a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language RankNTypes #}\r\n{# Language KindSignatures #}\r\n{# Language PolyKinds #}\r\n\r\nimport GHC.Exts\r\n\r\nnewtype Foo rep = MkFoo (forall (a :: TYPE rep). a)\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64unknownlinux):\r\n isUnliftedType\r\n forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type\r\n isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language RankNTypes #}
{# Language KindSignatures #}
{# Language PolyKinds #}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64unknownlinux):
isUnliftedType
forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type
isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 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 panic: newtype F rep = F (forall (a :: TYPE rep). a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language RankNTypes #}\r\n{# Language KindSignatures #}\r\n{# Language PolyKinds #}\r\n\r\nimport GHC.Exts\r\n\r\nnewtype Foo rep = MkFoo (forall (a :: TYPE rep). a)\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghcstage2 interactive ignoredotghci /tmp/U.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64unknownlinux):\r\n isUnliftedType\r\n forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type\r\n isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.10.1https://gitlab.haskell.org/ghc/ghc//issues/15870No skolem info panic20190707T18:02:38ZsheafNo skolem info panicI've been toying with some typelevel lenses and running into some issues with kind unification, when I ran into a panic:
```
bug.hs:30:34: error:ghc.exe: panic! (the 'impossible' happened)
(GHC version 8.6.2 for x86_64unknownmingw32):
No skolem info:
[k_a1Hgj]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\utils\Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler\\typecheck\\TcErrors.hs:2891:5 in ghc:TcErrors
```
Here's a boiled down version (with a bit of extraneous code left in for context, as it's so short):
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
data Optic a where
Index :: Nat > Optic a
Name :: Symbol > Optic a
(:.:) :: Optic a > Optic b > Optic a  composition
class Gettable a (optic :: Optic a) where
type Get a (optic :: Optic a)
{
some basic instances, e.g.
instance Gettable (a,b) (Index 0) where
type Get (a,b) (Index 0) = a
...
}
instance forall a b (g1 :: Optic a) (g2 :: Optic b).
( Gettable a g1
, b ~ Get a g1
, Gettable b g2
) => Gettable a (g1 :.: g2) where
type Get a (g1 :.: g2) = Get a g2
```
The program I am actually trying to write has the instance declaration changed to
```hs
instance forall a b (g1 :: Optic a) (g2 :: Optic (Get a g1)).
( Gettable a g1
, b ~ Get a g1
, Gettable b g2
) => Gettable a (g1 :.: g2) where
type Get a (g1 :.: g2) = Get (Get a g1) g2
```
but GHC complains that it can't match kinds:
```
• Expected kind ‘Optic b’, but ‘g2’ has kind ‘Optic (Get a g1)’
• In the second argument of ‘Gettable’, namely ‘g2’
In the instance declaration for ‘Gettable a (g1 :.: g2)’

20  , Gettable b g2

```
I don't know if there is a way around that, and I'd be interested to hear any advice.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 Type  Bug 
 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":"No skolem info panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I've been toying with some typelevel lenses and running into some issues with kind unification, when I ran into a panic:\r\n\r\n\r\n{{{\r\nbug.hs:30:34: error:ghc.exe: panic! (the 'impossible' happened)\r\n (GHC version 8.6.2 for x86_64unknownmingw32):\r\n No skolem info:\r\n [k_a1Hgj]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler\\utils\\Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler\\\\typecheck\\\\TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nHere's a boiled down version (with a bit of extraneous code left in for context, as it's so short):\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\ndata Optic a where\r\n Index :: Nat > Optic a\r\n Name :: Symbol > Optic a\r\n (:.:) :: Optic a > Optic b > Optic a  composition\r\n\r\nclass Gettable a (optic :: Optic a) where\r\n type Get a (optic :: Optic a)\r\n\r\n{\r\nsome basic instances, e.g.\r\ninstance Gettable (a,b) (Index 0) where\r\n type Get (a,b) (Index 0) = a\r\n...\r\n}\r\n\r\ninstance forall a b (g1 :: Optic a) (g2 :: Optic b).\r\n ( Gettable a g1\r\n , b ~ Get a g1\r\n , Gettable b g2\r\n ) => Gettable a (g1 :.: g2) where\r\n type Get a (g1 :.: g2) = Get a g2\r\n}}}\r\n\r\nThe program I am actually trying to write has the instance declaration changed to\r\n{{{#!hs\r\ninstance forall a b (g1 :: Optic a) (g2 :: Optic (Get a g1)).\r\n ( Gettable a g1\r\n , b ~ Get a g1\r\n , Gettable b g2\r\n ) => Gettable a (g1 :.: g2) where\r\n type Get a (g1 :.: g2) = Get (Get a g1) g2\r\n}}}\r\nbut GHC complains that it can't match kinds:\r\n\r\n{{{\r\n • Expected kind ‘Optic b’, but ‘g2’ has kind ‘Optic (Get a g1)’\r\n • In the second argument of ‘Gettable’, namely ‘g2’\r\n In the instance declaration for ‘Gettable a (g1 :.: g2)’\r\n \r\n20  , Gettable b g2\r\n \r\n}}}\r\nI don't know if there is a way around that, and I'd be interested to hear any advice.\r\n","type_of_failure":"OtherFailure","blocking":[]} >I've been toying with some typelevel lenses and running into some issues with kind unification, when I ran into a panic:
```
bug.hs:30:34: error:ghc.exe: panic! (the 'impossible' happened)
(GHC version 8.6.2 for x86_64unknownmingw32):
No skolem info:
[k_a1Hgj]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\utils\Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler\\typecheck\\TcErrors.hs:2891:5 in ghc:TcErrors
```
Here's a boiled down version (with a bit of extraneous code left in for context, as it's so short):
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
data Optic a where
Index :: Nat > Optic a
Name :: Symbol > Optic a
(:.:) :: Optic a > Optic b > Optic a  composition
class Gettable a (optic :: Optic a) where
type Get a (optic :: Optic a)
{
some basic instances, e.g.
instance Gettable (a,b) (Index 0) where
type Get (a,b) (Index 0) = a
...
}
instance forall a b (g1 :: Optic a) (g2 :: Optic b).
( Gettable a g1
, b ~ Get a g1
, Gettable b g2
) => Gettable a (g1 :.: g2) where
type Get a (g1 :.: g2) = Get a g2
```
The program I am actually trying to write has the instance declaration changed to
```hs
instance forall a b (g1 :: Optic a) (g2 :: Optic (Get a g1)).
( Gettable a g1
, b ~ Get a g1
, Gettable b g2
) => Gettable a (g1 :.: g2) where
type Get a (g1 :.: g2) = Get (Get a g1) g2
```
but GHC complains that it can't match kinds:
```
• Expected kind ‘Optic b’, but ‘g2’ has kind ‘Optic (Get a g1)’
• In the second argument of ‘Gettable’, namely ‘g2’
In the instance declaration for ‘Gettable a (g1 :.: g2)’

20  , Gettable b g2

```
I don't know if there is a way around that, and I'd be interested to hear any advice.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.2 
 Type  Bug 
 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":"No skolem info panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I've been toying with some typelevel lenses and running into some issues with kind unification, when I ran into a panic:\r\n\r\n\r\n{{{\r\nbug.hs:30:34: error:ghc.exe: panic! (the 'impossible' happened)\r\n (GHC version 8.6.2 for x86_64unknownmingw32):\r\n No skolem info:\r\n [k_a1Hgj]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler\\utils\\Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler\\\\typecheck\\\\TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nHere's a boiled down version (with a bit of extraneous code left in for context, as it's so short):\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n\r\ndata Optic a where\r\n Index :: Nat > Optic a\r\n Name :: Symbol > Optic a\r\n (:.:) :: Optic a > Optic b > Optic a  composition\r\n\r\nclass Gettable a (optic :: Optic a) where\r\n type Get a (optic :: Optic a)\r\n\r\n{\r\nsome basic instances, e.g.\r\ninstance Gettable (a,b) (Index 0) where\r\n type Get (a,b) (Index 0) = a\r\n...\r\n}\r\n\r\ninstance forall a b (g1 :: Optic a) (g2 :: Optic b).\r\n ( Gettable a g1\r\n , b ~ Get a g1\r\n , Gettable b g2\r\n ) => Gettable a (g1 :.: g2) where\r\n type Get a (g1 :.: g2) = Get a g2\r\n}}}\r\n\r\nThe program I am actually trying to write has the instance declaration changed to\r\n{{{#!hs\r\ninstance forall a b (g1 :: Optic a) (g2 :: Optic (Get a g1)).\r\n ( Gettable a g1\r\n , b ~ Get a g1\r\n , Gettable b g2\r\n ) => Gettable a (g1 :.: g2) where\r\n type Get a (g1 :.: g2) = Get (Get a g1) g2\r\n}}}\r\nbut GHC complains that it can't match kinds:\r\n\r\n{{{\r\n • Expected kind ‘Optic b’, but ‘g2’ has kind ‘Optic (Get a g1)’\r\n • In the second argument of ‘Gettable’, namely ‘g2’\r\n In the instance declaration for ‘Gettable a (g1 :.: g2)’\r\n \r\n20  , Gettable b g2\r\n \r\n}}}\r\nI don't know if there is a way around that, and I'd be interested to hear any advice.\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.6.3https://gitlab.haskell.org/ghc/ghc//issues/15869Discrepancy between seemingly equivalent type synonym and type family20190707T18:02:38ZRyan ScottDiscrepancy between seemingly equivalent type synonym and type familyConsider the following code:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE LiberalTypeSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
KindOf2 (a :: k) = k
data A (a :: Type) :: a > Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
Apply1 f a x = f a x
```
`Apply1` kindchecks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
Apply2 f a x = f a x
```
However, GHC rejects this!
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error:
• Expecting two more arguments to ‘f’
Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* > a > *’
• In the first argument of ‘Apply2’, namely ‘f’
In the type family declaration for ‘Apply2’

25  Apply2 f a x = f a x
 ^
```
I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kindcheck:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
forall (f :: KindOf2 A) (a :: Type) (x :: a).
Apply2 f a x = f a x
```
Although the error message does change a bit:
```
$ ~/Software/ghc3/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error:
• Expected kind ‘* > a > *’, but ‘f’ has kind ‘KindOf2 A’
• In the type ‘f a x’
In the type family declaration for ‘Apply2’

26  Apply2 f a x = f a x
 ^^^^^
```Consider the following code:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE LiberalTypeSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
KindOf2 (a :: k) = k
data A (a :: Type) :: a > Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
Apply1 f a x = f a x
```
`Apply1` kindchecks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
Apply2 f a x = f a x
```
However, GHC rejects this!
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error:
• Expecting two more arguments to ‘f’
Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* > a > *’
• In the first argument of ‘Apply2’, namely ‘f’
In the type family declaration for ‘Apply2’

25  Apply2 f a x = f a x
 ^
```
I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kindcheck:
```hs
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
forall (f :: KindOf2 A) (a :: Type) (x :: a).
Apply2 f a x = f a x
```
Although the error message does change a bit:
```
$ ~/Software/ghc3/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error:
• Expected kind ‘* > a > *’, but ‘f’ has kind ‘KindOf2 A’
• In the type ‘f a x’
In the type family declaration for ‘Apply2’

26  Apply2 f a x = f a x
 ^^^^^
```https://gitlab.haskell.org/ghc/ghc//issues/15829Add a test case for tricky type synonyms involving visible dependent kinds20190707T18:02:49ZRyan ScottAdd a test case for tricky type synonyms involving visible dependent kindsThis code does not typecheck on GHC 8.6.1:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
module Bug where
import Data.Kind
data A :: Type > Type
data B a :: A a > Type
type C a = B a
```
However, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 Type  Bug 
 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":"Add a test case for tricky type synonyms involving visible dependent kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code does not typecheck on GHC 8.6.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata A :: Type > Type\r\ndata B a :: A a > Type\r\ntype C a = B a\r\n}}}\r\n\r\nHowever, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.","type_of_failure":"OtherFailure","blocking":[]} >This code does not typecheck on GHC 8.6.1:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
module Bug where
import Data.Kind
data A :: Type > Type
data B a :: A a > Type
type C a = B a
```
However, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.7 
 Type  Bug 
 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":"Add a test case for tricky type synonyms involving visible dependent kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code does not typecheck on GHC 8.6.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata A :: Type > Type\r\ndata B a :: A a > Type\r\ntype C a = B a\r\n}}}\r\n\r\nHowever, it //does// typecheck on GHC HEAD, after commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (Finish fix for #14880.). This is very cool, although it does alarm me that there is no test case which checks for this at the moment. Let's add one to ensure that this stays fixed.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15796Core Lint error with invalid newtype declaration20190707T18:02:56ZIcelandjackCore Lint error with invalid newtype declarationThis gives a Core Lint error
```hs
{# Language QuantifiedConstraints #}
{# Language TypeApplications #}
{# Language TypeOperators #}
{# Language PolyKinds #}
{# Language FlexibleInstances #}
{# Language DataKinds #}
{# Language TypeFamilies #}
{# Language MultiParamTypeClasses #}
{# Language ConstraintKinds #}
{# Language UndecidableInstances #}
{# Language GADTs #}
{# Options_GHC dcorelint #}
import Data.Kind
type Cat ob = ob > ob > Type
class Ríki (obj :: Type) where
type (>) :: Cat obj
class Varpi (f :: dom > cod)
newtype
(··>) :: Cat (a > b) where
Natu :: Varpi f
=> (forall xx. f xx > f' xx)
> (f ··> f')
instance
Ríki cod
=> 
Ríki (dom > cod)
where
type (>) = (··>) @dom @cod
```
```
$ ghci ignoredotghci 568_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 568_bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64unknownlinux):
Core Lint error
<no location info>: warning:
In the type ‘(··>)’
Found TcTyCon: ··>[tc]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
> :q
Leaving GHCi.
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This gives a Core Lint error\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints #}\r\n{# Language TypeApplications #}\r\n{# Language TypeOperators #}\r\n{# Language PolyKinds #}\r\n{# Language FlexibleInstances #}\r\n{# Language DataKinds #}\r\n{# Language TypeFamilies #}\r\n{# Language MultiParamTypeClasses #}\r\n{# Language ConstraintKinds #}\r\n{# Language UndecidableInstances #}\r\n{# Language GADTs #}\r\n\r\n{# Options_GHC dcorelint #}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\nclass Ríki (obj :: Type) where\r\n type (>) :: Cat obj\r\n\r\nclass Varpi (f :: dom > cod)\r\n\r\nnewtype\r\n (··>) :: Cat (a > b) where\r\n Natu :: Varpi f\r\n => (forall xx. f xx > f' xx)\r\n > (f ··> f')\r\n\r\ninstance\r\n Ríki cod\r\n => \r\n Ríki (dom > cod)\r\n where\r\n\r\n type (>) = (··>) @dom @cod\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci 568_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 568_bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64unknownlinux):\r\n Core Lint error\r\n <no location info>: warning:\r\n In the type ‘(··>)’\r\n Found TcTyCon: ··>[tc]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> :q\r\nLeaving GHCi.\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This gives a Core Lint error
```hs
{# Language QuantifiedConstraints #}
{# Language TypeApplications #}
{# Language TypeOperators #}
{# Language PolyKinds #}
{# Language FlexibleInstances #}
{# Language DataKinds #}
{# Language TypeFamilies #}
{# Language MultiParamTypeClasses #}
{# Language ConstraintKinds #}
{# Language UndecidableInstances #}
{# Language GADTs #}
{# Options_GHC dcorelint #}
import Data.Kind
type Cat ob = ob > ob > Type
class Ríki (obj :: Type) where
type (>) :: Cat obj
class Varpi (f :: dom > cod)
newtype
(··>) :: Cat (a > b) where
Natu :: Varpi f
=> (forall xx. f xx > f' xx)
> (f ··> f')
instance
Ríki cod
=> 
Ríki (dom > cod)
where
type (>) = (··>) @dom @cod
```
```
$ ghci ignoredotghci 568_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 568_bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64unknownlinux):
Core Lint error
<no location info>: warning:
In the type ‘(··>)’
Found TcTyCon: ··>[tc]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
> :q
Leaving GHCi.
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This gives a Core Lint error\r\n\r\n{{{#!hs\r\n{# Language QuantifiedConstraints #}\r\n{# Language TypeApplications #}\r\n{# Language TypeOperators #}\r\n{# Language PolyKinds #}\r\n{# Language FlexibleInstances #}\r\n{# Language DataKinds #}\r\n{# Language TypeFamilies #}\r\n{# Language MultiParamTypeClasses #}\r\n{# Language ConstraintKinds #}\r\n{# Language UndecidableInstances #}\r\n{# Language GADTs #}\r\n\r\n{# Options_GHC dcorelint #}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\nclass Ríki (obj :: Type) where\r\n type (>) :: Cat obj\r\n\r\nclass Varpi (f :: dom > cod)\r\n\r\nnewtype\r\n (··>) :: Cat (a > b) where\r\n Natu :: Varpi f\r\n => (forall xx. f xx > f' xx)\r\n > (f ··> f')\r\n\r\ninstance\r\n Ríki cod\r\n => \r\n Ríki (dom > cod)\r\n where\r\n\r\n type (>) = (··>) @dom @cod\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci 568_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 568_bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64unknownlinux):\r\n Core Lint error\r\n <no location info>: warning:\r\n In the type ‘(··>)’\r\n Found TcTyCon: ··>[tc]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> :q\r\nLeaving GHCi.\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.2https://gitlab.haskell.org/ghc/ghc//issues/15778GHC HEADonly panic (zonkTcTyVarToTyVar)20190707T18:03:02ZRyan ScottGHC HEADonly panic (zonkTcTyVarToTyVar)The following program typechecks on GHC 8.0.1 through 8.6.1:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
type a ~> b = a > b > Type
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing (a :: k)
data Flarble (a :: Type) where
MkFlarble :: Flarble Bool
data instance Sing (z :: Flarble a) where
SMkFlarble :: Sing MkFlarble
elimFlarble :: forall a
(p :: forall x. Flarble x ~> Type)
(f :: Flarble a).
Sing f
> Apply p MkFlarble
> Apply p f
elimFlarble s@SMkFlarble pMkFlarble =
case s of
(_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) >
pMkFlarble
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181015 for x86_64unknownlinux):
zonkTcTyVarToTyVar
probablyABadIdea_aWn[tau:2]
Bool
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType
```
If I replace `probablyABadIdea` with `Bool`, then it typechecks again.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEADonly panic (zonkTcTyVarToTyVar)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.0.1 through 8.6.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype a ~> b = a > b > Type\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing (a :: k)\r\n\r\ndata Flarble (a :: Type) where\r\n MkFlarble :: Flarble Bool\r\ndata instance Sing (z :: Flarble a) where\r\n SMkFlarble :: Sing MkFlarble\r\n\r\nelimFlarble :: forall a\r\n (p :: forall x. Flarble x ~> Type)\r\n (f :: Flarble a).\r\n Sing f\r\n > Apply p MkFlarble\r\n > Apply p f\r\nelimFlarble s@SMkFlarble pMkFlarble =\r\n case s of\r\n (_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) >\r\n pMkFlarble\r\n}}}\r\n\r\nHowever, it panics on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181015 for x86_64unknownlinux):\r\n zonkTcTyVarToTyVar\r\n probablyABadIdea_aWn[tau:2]\r\n Bool\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType\r\n}}}\r\n\r\nIf I replace `probablyABadIdea` with `Bool`, then it typechecks again.","type_of_failure":"OtherFailure","blocking":[]} >The following program typechecks on GHC 8.0.1 through 8.6.1:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
type a ~> b = a > b > Type
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing (a :: k)
data Flarble (a :: Type) where
MkFlarble :: Flarble Bool
data instance Sing (z :: Flarble a) where
SMkFlarble :: Sing MkFlarble
elimFlarble :: forall a
(p :: forall x. Flarble x ~> Type)
(f :: Flarble a).
Sing f
> Apply p MkFlarble
> Apply p f
elimFlarble s@SMkFlarble pMkFlarble =
case s of
(_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) >
pMkFlarble
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181015 for x86_64unknownlinux):
zonkTcTyVarToTyVar
probablyABadIdea_aWn[tau:2]
Bool
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType
```
If I replace `probablyABadIdea` with `Bool`, then it typechecks again.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEADonly panic (zonkTcTyVarToTyVar)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.0.1 through 8.6.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype a ~> b = a > b > Type\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing (a :: k)\r\n\r\ndata Flarble (a :: Type) where\r\n MkFlarble :: Flarble Bool\r\ndata instance Sing (z :: Flarble a) where\r\n SMkFlarble :: Sing MkFlarble\r\n\r\nelimFlarble :: forall a\r\n (p :: forall x. Flarble x ~> Type)\r\n (f :: Flarble a).\r\n Sing f\r\n > Apply p MkFlarble\r\n > Apply p f\r\nelimFlarble s@SMkFlarble pMkFlarble =\r\n case s of\r\n (_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) >\r\n pMkFlarble\r\n}}}\r\n\r\nHowever, it panics on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181015 for x86_64unknownlinux):\r\n zonkTcTyVarToTyVar\r\n probablyABadIdea_aWn[tau:2]\r\n Bool\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType\r\n}}}\r\n\r\nIf I replace `probablyABadIdea` with `Bool`, then it typechecks again.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15772Strange constraint error that disappears when adding another toplevel declar...20201226T13:06:22ZAndres LöhStrange constraint error that disappears when adding another toplevel declarationConsider this program:
```hs
{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}
module CURepro where
import Data.Kind
data NP (f :: Type > Type) (xs :: [Type])
type family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
Curry f xs r a = (xs ~ '[], r ~ a)
type family Tail (a :: [Type]) :: [Type] where
Tail (_ : xs) = xs
uncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a
uncurry_NP = undefined
fun_NP :: NP Id xs > ()
fun_NP = undefined
newtype Id a = MkId a
 test1 :: ()
 test1 = uncurry_NP fun_NP (MkId 5)
test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
```
With GHC 8.6.1 (and also 8.4.3), this produces the following error message:
```
CURepro.hs:27:9: error:
• Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
arising from a use of ‘uncurry_NP’
The type variable ‘t0’ is ambiguous
• In the expression:
uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
In an equation for ‘test2’:
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)

27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
However, uncommenting the definition of `test1` makes the whole program check without error!
I think both versions of the program should be accepted.
I've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Strange constraint error that disappears when adding another toplevel declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this program:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}\r\nmodule CURepro where\r\n\r\nimport Data.Kind\r\n\r\ndata NP (f :: Type > Type) (xs :: [Type])\r\n\r\ntype family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where\r\n Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)\r\n Curry f xs r a = (xs ~ '[], r ~ a)\r\n\r\ntype family Tail (a :: [Type]) :: [Type] where\r\n Tail (_ : xs) = xs\r\n\r\nuncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a\r\nuncurry_NP = undefined\r\n\r\nfun_NP :: NP Id xs > ()\r\nfun_NP = undefined\r\n\r\nnewtype Id a = MkId a\r\n\r\n test1 :: ()\r\n test1 = uncurry_NP fun_NP (MkId 5)\r\n\r\ntest2 :: ()\r\ntest2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n}}}\r\n\r\nWith GHC 8.6.1 (and also 8.4.3), this produces the following error message:\r\n{{{\r\nCURepro.hs:27:9: error:\r\n • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’\r\n arising from a use of ‘uncurry_NP’\r\n The type variable ‘t0’ is ambiguous\r\n • In the expression:\r\n uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n In an equation for ‘test2’:\r\n test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n \r\n27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nHowever, uncommenting the definition of `test1` makes the whole program check without error!\r\n\r\nI think both versions of the program should be accepted.\r\n\r\nI've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.","type_of_failure":"OtherFailure","blocking":[]} >Consider this program:
```hs
{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}
module CURepro where
import Data.Kind
data NP (f :: Type > Type) (xs :: [Type])
type family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
Curry f xs r a = (xs ~ '[], r ~ a)
type family Tail (a :: [Type]) :: [Type] where
Tail (_ : xs) = xs
uncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a
uncurry_NP = undefined
fun_NP :: NP Id xs > ()
fun_NP = undefined
newtype Id a = MkId a
 test1 :: ()
 test1 = uncurry_NP fun_NP (MkId 5)
test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
```
With GHC 8.6.1 (and also 8.4.3), this produces the following error message:
```
CURepro.hs:27:9: error:
• Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
arising from a use of ‘uncurry_NP’
The type variable ‘t0’ is ambiguous
• In the expression:
uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
In an equation for ‘test2’:
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)

27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
However, uncommenting the definition of `test1` makes the whole program check without error!
I think both versions of the program should be accepted.
I've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Strange constraint error that disappears when adding another toplevel declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this program:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #}\r\nmodule CURepro where\r\n\r\nimport Data.Kind\r\n\r\ndata NP (f :: Type > Type) (xs :: [Type])\r\n\r\ntype family Curry (f :: Type > Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where\r\n Curry f xs r (f x > a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)\r\n Curry f xs r a = (xs ~ '[], r ~ a)\r\n\r\ntype family Tail (a :: [Type]) :: [Type] where\r\n Tail (_ : xs) = xs\r\n\r\nuncurry_NP :: (Curry f xs r a) => (NP f xs > r) > a\r\nuncurry_NP = undefined\r\n\r\nfun_NP :: NP Id xs > ()\r\nfun_NP = undefined\r\n\r\nnewtype Id a = MkId a\r\n\r\n test1 :: ()\r\n test1 = uncurry_NP fun_NP (MkId 5)\r\n\r\ntest2 :: ()\r\ntest2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n}}}\r\n\r\nWith GHC 8.6.1 (and also 8.4.3), this produces the following error message:\r\n{{{\r\nCURepro.hs:27:9: error:\r\n • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’\r\n arising from a use of ‘uncurry_NP’\r\n The type variable ‘t0’ is ambiguous\r\n • In the expression:\r\n uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n In an equation for ‘test2’:\r\n test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n \r\n27  test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nHowever, uncommenting the definition of `test1` makes the whole program check without error!\r\n\r\nI think both versions of the program should be accepted.\r\n\r\nI've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that `NP` is parameterised over a type constructor `f` seems to be somehow essential to trigger this.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15708Crossmodule SPECIALZE pragmas aren't typechecked in O020190707T18:03:21ZregnatCrossmodule SPECIALZE pragmas aren't typechecked in O0If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

 Bar.hs
module Bar where
import Foo
{# SPECIALIZE foo :: Int > Bool #}
```
running `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int > Int
Actual type: Int > Bool
• In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

 Bar.hs
module Bar where
import Foo
{# SPECIALIZE foo :: Int > Bool #}
```
running `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int > Int
Actual type: Int > Bool
• In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15707More liberally kinded coercions for newtypes20190707T18:03:21ZmniipMore liberally kinded coercions for newtypesConsider the infinite data family (possible thanks to #12369):
```hs
data family I :: k > k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of etacontracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k > *). a ~R I a
forall (a :: k > l > *). a ~R I a
forall (a :: k > l > m > *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x > I a x
i1 = coerce
...
```Consider the infinite data family (possible thanks to #12369):
```hs
data family I :: k > k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of etacontracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k > *). a ~R I a
forall (a :: k > l > *). a ~R I a
forall (a :: k > l > m > *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x > I a x
i1 = coerce
...
```8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15704Different saturations of the same polymorphickinded type constructor aren't ...20190707T18:03:22ZmniipDifferent saturations of the same polymorphickinded type constructor aren't seen as apart types```hs
{# LANGUAGE TypeFamilies, PolyKinds #}
module A where
data family D :: k
type family F (a :: k) :: *
type instance F (D Int) = Int
type instance F (f a b) = Char
type instance F (D Int Bool) = Char
```
The last equation, even though a specialization of the middle one, trips up the equality consistency check:
```hs
a.hs:9:15: error:
Conflicting family instance declarations:
F (D Int) = Int  Defined at a.hs:9:15
F (D Int Bool) = Char  Defined at a.hs:10:15

9  type instance F (D Int) = Int
 ^
```
So GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Different saturations of the same polymorphickinded type constructor aren't seen as apart types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE TypeFamilies, PolyKinds #}\r\n\r\nmodule A where\r\n\r\ndata family D :: k\r\n\r\ntype family F (a :: k) :: *\r\n\r\ntype instance F (D Int) = Int\r\ntype instance F (f a b) = Char\r\ntype instance F (D Int Bool) = Char\r\n}}}\r\n\r\nThe last equation, even though a specialization of the middle one, trips up the equality consistency check:\r\n{{{#!hs\r\na.hs:9:15: error:\r\n Conflicting family instance declarations:\r\n F (D Int) = Int  Defined at a.hs:9:15\r\n F (D Int Bool) = Char  Defined at a.hs:10:15\r\n \r\n9  type instance F (D Int) = Int\r\n  ^\r\n}}}\r\n\r\nSo GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# LANGUAGE TypeFamilies, PolyKinds #}
module A where
data family D :: k
type family F (a :: k) :: *
type instance F (D Int) = Int
type instance F (f a b) = Char
type instance F (D Int Bool) = Char
```
The last equation, even though a specialization of the middle one, trips up the equality consistency check:
```hs
a.hs:9:15: error:
Conflicting family instance declarations:
F (D Int) = Int  Defined at a.hs:9:15
F (D Int Bool) = Char  Defined at a.hs:10:15

9  type instance F (D Int) = Int
 ^
```
So GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Different saturations of the same polymorphickinded type constructor aren't seen as apart types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# LANGUAGE TypeFamilies, PolyKinds #}\r\n\r\nmodule A where\r\n\r\ndata family D :: k\r\n\r\ntype family F (a :: k) :: *\r\n\r\ntype instance F (D Int) = Int\r\ntype instance F (f a b) = Char\r\ntype instance F (D Int Bool) = Char\r\n}}}\r\n\r\nThe last equation, even though a specialization of the middle one, trips up the equality consistency check:\r\n{{{#!hs\r\na.hs:9:15: error:\r\n Conflicting family instance declarations:\r\n F (D Int) = Int  Defined at a.hs:9:15\r\n F (D Int Bool) = Char  Defined at a.hs:10:15\r\n \r\n9  type instance F (D Int) = Int\r\n  ^\r\n}}}\r\n\r\nSo GHC is able to infer that `D Int ~/~ f a b` because `D ~/~ f a`, but for some reason the same reasoning doesn't work for `D ~/~ D a`.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1mniipmniiphttps://gitlab.haskell.org/ghc/ghc//issues/15691Marking Pred(S n) = n as injective20190707T18:03:26ZIcelandjackMarking Pred(S n) = n as injectiveShould `Pred` be injective? Please close the ticket if this is a known limitation
```hs
{# Language DataKinds, TypeFamilyDependencies #}
data N = O  S N
type family
Pred n = res  res > n where
Pred(S n) = n
```
fails with
```
• Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n  Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’

7  Pred(S n) = n
 ^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Marking Pred(S n) = n as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["InjectiveFamilies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Should `Pred` be injective? Please close the ticket if this is a known limitation \r\n\r\n{{{#!hs\r\n{# Language DataKinds, TypeFamilyDependencies #}\r\n\r\ndata N = O  S N\r\n\r\ntype family\r\n Pred n = res  res > n where\r\n Pred(S n) = n\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n • Type family equation violates injectivity annotation.\r\n RHS of injective type family equation is a bare type variable\r\n but these LHS type and kind patterns are not bare variables: ‘'S n’\r\n Pred ('S n) = n  Defined at 462.hs:7:2\r\n • In the equations for closed type family ‘Pred’\r\n In the type family declaration for ‘Pred’\r\n \r\n7  Pred(S n) = n\r\n  ^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Should `Pred` be injective? Please close the ticket if this is a known limitation
```hs
{# Language DataKinds, TypeFamilyDependencies #}
data N = O  S N
type family
Pred n = res  res > n where
Pred(S n) = n
```
fails with
```
• Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n  Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’

7  Pred(S n) = n
 ^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 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":"Marking Pred(S n) = n as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["InjectiveFamilies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Should `Pred` be injective? Please close the ticket if this is a known limitation \r\n\r\n{{{#!hs\r\n{# Language DataKinds, TypeFamilyDependencies #}\r\n\r\ndata N = O  S N\r\n\r\ntype family\r\n Pred n = res  res > n where\r\n Pred(S n) = n\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n • Type family equation violates injectivity annotation.\r\n RHS of injective type family equation is a bare type variable\r\n but these LHS type and kind patterns are not bare variables: ‘'S n’\r\n Pred ('S n) = n  Defined at 462.hs:7:2\r\n • In the equations for closed type family ‘Pred’\r\n In the type family declaration for ‘Pred’\r\n \r\n7  Pred(S n) = n\r\n  ^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15678Provide the provenance of unification variables in error messages when possible20210125T16:36:44ZRyan ScottProvide the provenance of unification variables in error messages when possibleConsider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:14: error:
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
• In the second argument of ‘const’, namely ‘_’
In the expression: const 42 _
In an equation for ‘x’: x = const 42 _
• Relevant bindings include x :: Int (bound at Bug.hs:4:1)
Valid hole fits include
x :: Int (bound at Bug.hs:4:1)
otherwise :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Base’))
False :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
True :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
lines :: String > [String]
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
unlines :: [String] > String
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
(Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)

4  x = const 42 _
 ^
```
One thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.
simonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:
```
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
Arising from an application of
(const 42 :: b0 > Int)
In the expression: const 42 _
```
This would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  Tritlo 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Provide the provenance of unification variables in error messages when possible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nx :: Int\r\nx = const 42 _\r\n}}}\r\n\r\nWhen compiles, this gives the following suggestion:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:14: error:\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n • In the second argument of ‘const’, namely ‘_’\r\n In the expression: const 42 _\r\n In an equation for ‘x’: x = const 42 _\r\n • Relevant bindings include x :: Int (bound at Bug.hs:4:1)\r\n Valid hole fits include\r\n x :: Int (bound at Bug.hs:4:1)\r\n otherwise :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Base’))\r\n False :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n True :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n lines :: String > [String]\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n unlines :: [String] > String\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n (Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)\r\n \r\n4  x = const 42 _\r\n  ^\r\n}}}\r\n\r\nOne thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.\r\n\r\nsimonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:\r\n\r\n{{{\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n Arising from an application of\r\n (const 42 :: b0 > Int)\r\n In the expression: const 42 _\r\n}}}\r\n\r\nThis would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:14: error:
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
• In the second argument of ‘const’, namely ‘_’
In the expression: const 42 _
In an equation for ‘x’: x = const 42 _
• Relevant bindings include x :: Int (bound at Bug.hs:4:1)
Valid hole fits include
x :: Int (bound at Bug.hs:4:1)
otherwise :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Base’))
False :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
True :: Bool
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘GHC.Types’))
lines :: String > [String]
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
unlines :: [String] > String
(imported from ‘Prelude’ at Bug.hs:1:810
(and originally defined in ‘base4.12.0.0:Data.OldList’))
(Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)

4  x = const 42 _
 ^
```
One thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.
simonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:
```
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
Arising from an application of
(const 42 :: b0 > Int)
In the expression: const 42 _
```
This would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  Tritlo 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Provide the provenance of unification variables in error messages when possible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nx :: Int\r\nx = const 42 _\r\n}}}\r\n\r\nWhen compiles, this gives the following suggestion:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:14: error:\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n • In the second argument of ‘const’, namely ‘_’\r\n In the expression: const 42 _\r\n In an equation for ‘x’: x = const 42 _\r\n • Relevant bindings include x :: Int (bound at Bug.hs:4:1)\r\n Valid hole fits include\r\n x :: Int (bound at Bug.hs:4:1)\r\n otherwise :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Base’))\r\n False :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n True :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘GHC.Types’))\r\n lines :: String > [String]\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n unlines :: [String] > String\r\n (imported from ‘Prelude’ at Bug.hs:1:810\r\n (and originally defined in ‘base4.12.0.0:Data.OldList’))\r\n (Some hole fits suppressed; use fmaxvalidholefits=N or fnomaxvalidholefits)\r\n \r\n4  x = const 42 _\r\n  ^\r\n}}}\r\n\r\nOne thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.\r\n\r\nsimonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 > Int`. Let's report this! Something like:\r\n\r\n{{{\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n Arising from an application of\r\n (const 42 :: b0 > Int)\r\n In the expression: const 42 _\r\n}}}\r\n\r\nThis would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.","type_of_failure":"OtherFailure","blocking":[]} >9.2.1Matthías Páll GissurarsonMatthías Páll Gissurarsonhttps://gitlab.haskell.org/ghc/ghc//issues/15639Surprising failure combining QuantifiedConstraints with Coercible20190707T18:03:38ZDavid FeuerSurprising failure combining QuantifiedConstraints with CoercibleI don't understand what's going wrong here.
```hs
 Fishy.hs
{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r
yeahCoercible r = r
 Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I don't understand what's going wrong here.
```hs
 Fishy.hs
{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r
yeahCoercible r = r
 Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15629"No skolem info" panic (GHC 8.6 only)20190707T18:03:40ZRyan Scott"No skolem info" panic (GHC 8.6 only)The following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
import GHC.Generics
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k > Type
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f
singFun1 f = SLambda f
data From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a
data To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = Apply f (Apply g x)
data (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing x > Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)
(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)
f :: forall (m :: Type > Type) x. Proxy (m x) > ()
f _ = ()
where
sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
sFrom1Fun = undefined
sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
sTo1Fun = undefined
sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
```
Panics on GHC 8.6:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab1’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180823 for x86_64unknownlinux):
No skolem info:
[ab_a1UW[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
But merely errors on GHC 8.4.3:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab2’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:
• Couldn't match type ‘ab1’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing From1Sym0
Actual type: Sing From1Sym0
• In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^^^
Bug.hs:51:36: error:
• Couldn't match type ‘ab’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing To1Sym0
Actual type: Sing To1Sym0
• In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 Type  Bug 
 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":"\"No skolem info\" panic (GHC 8.6 only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport GHC.Generics\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata family Sing :: forall k. k > Type\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\nsingFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f\r\nsingFun1 f = SLambda f\r\n\r\ndata From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a\r\ndata To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a\r\n\r\ntype family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where\r\n (f :. g) x = Apply f (Apply g x)\r\n\r\ndata (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)\r\ntype instance Apply (f .@#@$$$ g) x = (f :. g) x\r\n\r\n(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing x > Sing ((f :. g) x)\r\n(sf %. sg) sx = applySing sf (applySing sg sx)\r\n\r\n(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing (f .@#@$$$ g)\r\nsf %.$$$ sg = singFun1 (sf %. sg)\r\n\r\nf :: forall (m :: Type > Type) x. Proxy (m x) > ()\r\nf _ = ()\r\n where\r\n sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)\r\n sFrom1Fun = undefined\r\n\r\n sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)\r\n sTo1Fun = undefined\r\n\r\n sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n}}}\r\n\r\nPanics on GHC 8.6:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab1’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180823 for x86_64unknownlinux):\r\n No skolem info:\r\n [ab_a1UW[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nBut merely errors on GHC 8.4.3:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab2’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:\r\n • Couldn't match type ‘ab1’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing From1Sym0\r\n Actual type: Sing From1Sym0\r\n • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^^^\r\n\r\nBug.hs:51:36: error:\r\n • Couldn't match type ‘ab’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing To1Sym0\r\n Actual type: Sing To1Sym0\r\n • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
import GHC.Generics
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k > Type
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f
singFun1 f = SLambda f
data From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a
data To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = Apply f (Apply g x)
data (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing x > Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)
(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f > Sing g > Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)
f :: forall (m :: Type > Type) x. Proxy (m x) > ()
f _ = ()
where
sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
sFrom1Fun = undefined
sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
sTo1Fun = undefined
sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
```
Panics on GHC 8.6:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab1’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180823 for x86_64unknownlinux):
No skolem info:
[ab_a1UW[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
But merely errors on GHC 8.4.3:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab2’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)

50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:
• Couldn't match type ‘ab1’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing From1Sym0
Actual type: Sing From1Sym0
• In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^^^
Bug.hs:51:36: error:
• Couldn't match type ‘ab’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5112
Expected type: Sing To1Sym0
Actual type: Sing To1Sym0
• In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)

51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
 ^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 Type  Bug 
 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":"\"No skolem info\" panic (GHC 8.6 only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport GHC.Generics\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata family Sing :: forall k. k > Type\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\nsingFun1 :: forall f. (forall t. Sing t > Sing (Apply f t)) > Sing f\r\nsingFun1 f = SLambda f\r\n\r\ndata From1Sym0 :: forall k (f :: k > Type) (a :: k). f a ~> Rep1 f a\r\ndata To1Sym0 :: forall k (f :: k > Type) (a :: k). Rep1 f a ~> f a\r\n\r\ntype family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where\r\n (f :. g) x = Apply f (Apply g x)\r\n\r\ndata (.@#@$$$) :: forall b c a. (b ~> c) > (a ~> b) > (a ~> c)\r\ntype instance Apply (f .@#@$$$ g) x = (f :. g) x\r\n\r\n(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing x > Sing ((f :. g) x)\r\n(sf %. sg) sx = applySing sf (applySing sg sx)\r\n\r\n(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f > Sing g > Sing (f .@#@$$$ g)\r\nsf %.$$$ sg = singFun1 (sf %. sg)\r\n\r\nf :: forall (m :: Type > Type) x. Proxy (m x) > ()\r\nf _ = ()\r\n where\r\n sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)\r\n sFrom1Fun = undefined\r\n\r\n sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)\r\n sTo1Fun = undefined\r\n\r\n sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n}}}\r\n\r\nPanics on GHC 8.6:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab1’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180823 for x86_64unknownlinux):\r\n No skolem info:\r\n [ab_a1UW[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nBut merely errors on GHC 8.4.3:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab2’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n \r\n50  sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:\r\n • Couldn't match type ‘ab1’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing From1Sym0\r\n Actual type: Sing From1Sym0\r\n • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^^^\r\n\r\nBug.hs:51:36: error:\r\n • Couldn't match type ‘ab’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5112\r\n Expected type: Sing To1Sym0\r\n Actual type: Sing To1Sym0\r\n • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n \r\n51  sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n  ^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15624defertypeerrors and equality constraints20190707T18:03:42ZKrzysztof Gogolewskidefertypeerrors and equality constraintsConsider
```
{# OPTIONS_GHC fdefertypeerrors #}
x = const True ('a' + 'a')
y = const True (not 'a')
```
Currently `x` is True, but `y` is undefined. I think it would make sense for both to be True.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  low 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"defertypeerrors and equality constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{\r\n{# OPTIONS_GHC fdefertypeerrors #}\r\nx = const True ('a' + 'a')\r\ny = const True (not 'a')\r\n}}}\r\n\r\nCurrently `x` is True, but `y` is undefined. I think it would make sense for both to be True.","type_of_failure":"OtherFailure","blocking":[]} >Consider
```
{# OPTIONS_GHC fdefertypeerrors #}
x = const True ('a' + 'a')
y = const True (not 'a')
```
Currently `x` is True, but `y` is undefined. I think it would make sense for both to be True.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  low 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"defertypeerrors and equality constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{\r\n{# OPTIONS_GHC fdefertypeerrors #}\r\nx = const True ('a' + 'a')\r\ny = const True (not 'a')\r\n}}}\r\n\r\nCurrently `x` is True, but `y` is undefined. I think it would make sense for both to be True.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15621Error message involving type families points to wrong location20210125T16:37:52ZRyan ScottError message involving type families points to wrong locationConsider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()

12  a = Refl
 ^^^^
```
This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.
Another interesting facet of this bug is that if you comment out `a`:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let { a :: F Int :~: F Int
a = Refl }
b :: F Int :~: F Bool
b = Refl
in ()
```
Then the error message will actually point to `b` this time:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()

15  b = Refl
 ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 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":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n \r\n12  a = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let { a :: F Int :~: F Int\r\n a = Refl }\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n \r\n15  b = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Consider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()

12  a = Refl
 ^^^^
```
This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.
Another interesting facet of this bug is that if you comment out `a`:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let { a :: F Int :~: F Int
a = Refl }
b :: F Int :~: F Bool
b = Refl
in ()
```
Then the error message will actually point to `b` this time:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a noninjective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()

15  b = Refl
 ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 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":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n \r\n12  a = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let { a :: F Int :~: F Int\r\n a = Refl }\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a noninjective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n \r\n15  b = Refl\r\n  ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/15596When a type application cannot be applied to an identifier due to the absence...20210125T16:37:52ZkindaroWhen a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!Consider this code:
```hs
{# language TypeApplications #}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 > a0 > a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer

6  g = f @Integer
 ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{# language TypeApplications #}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 > a0 > a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n \r\n6  g = f @Integer\r\n  ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code:
```hs
{# language TypeApplications #}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 > a0 > a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer

6  g = f @Integer
 ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{# language TypeApplications #}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 > a0 > a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n \r\n6  g = f @Integer\r\n  ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} >9.2.1https://gitlab.haskell.org/ghc/ghc//issues/15577TypeApplicationsrelated infinite loop (GHC 8.6+ only)20190830T12:55:21ZRyan ScottTypeApplicationsrelated infinite loop (GHC 8.6+ only)The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k > Type
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r > From1 (To1 r :: f a) :~: r
foo x
 Refl < sFot1  Uncommenting the line below makes it work again:
 @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* > *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl

35  @f @a @r x
 ^
Bug.hs:35:23: error:
• Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* > *’ with ‘*’
When matching kinds
f1 :: * > *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:58
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 > From1 (To1 r1) :~: r1
at Bug.hs:(29,1)(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

36  = Refl
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeApplicationsrelated infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r > From1 (To1 r :: f a) :~: r\r\nfoo x\r\n  Refl < sFot1  Uncommenting the line below makes it work again:\r\n  @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* > *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* > *’ with ‘*’\r\n When matching kinds\r\n f1 :: * > *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:58\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 > From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n36  = Refl\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k > Type
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r > From1 (To1 r :: f a) :~: r
foo x
 Refl < sFot1  Uncommenting the line below makes it work again:
 @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* > *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl

35  @f @a @r x
 ^
Bug.hs:35:23: error:
• Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* > *’ with ‘*’
When matching kinds
f1 :: * > *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:58
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 > From1 (To1 r1) :~: r1
at Bug.hs:(29,1)(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

36  = Refl
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeApplicationsrelated infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r > From1 (To1 r :: f a) :~: r\r\nfoo x\r\n  Refl < sFot1  Uncommenting the line below makes it work again:\r\n  @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* > *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* > *’ with ‘*’\r\n When matching kinds\r\n f1 :: * > *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:58\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 > From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n36  = Refl\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.2Alp MestanogullariBen GamariAlp Mestanogullarihttps://gitlab.haskell.org/ghc/ghc//issues/15557Reduce type families in equations' RHS when testing equation compatibility20190707T18:04:08ZmniipReduce type families in equations' RHS when testing equation compatibilityThe reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf
There in Definition 8 in section 3.4 it states:
Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.
Examine the following families:
```hs
type family If (a :: Bool) (b :: k) (c :: k) :: k where
If False a b = b
If True a b = a
type family Eql (a :: k) (b :: k) :: Bool where
Eql a a = True
Eql _ _ = False
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
Test a a = a
Test Nothing _ = Nothing
Test _ Nothing = Nothing
```
Applying the check to the equations 1 and 2 of `Test` we get:
unify(\<`Just x`, `Just y`\>, \<`a`, `a`\>) = Ω = \[`a` \> `Just x`, `y` \> `x`\]
Ω(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)
Therefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`
That doesn't happen:
```hs
> :t undefined :: p a > p (Test a a)
p a > p (Test a a)
```
Examining the IfaceAxBranches (cf #15546) we see:
```hs
axiom D:R:Test::
Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
Test k a a = a
(incompatible indices: [0])
Test k 'Nothing _ = 'Nothing
Test k _ 'Nothing = 'Nothing
```
GHC did not consider the two equations compatible.
Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's [ticket:8423\#comment:80951](https://gitlab.haskell.org//ghc/ghc/issues/8423#note_80951), but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).
The family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).
This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?
P.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:
```hs
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
Test a a = If (Eql a a) a Nothing
Test Nothing a = If (Eql Nothing a) Nothing Nothing
Test a Nothing = If (Eql a Nothing) Nothing Nothing
```
This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.
P.P.S: In [ticket:15546\#comment:158797](https://gitlab.haskell.org//ghc/ghc/issues/15546#note_158797) I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 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":"Reduce type families in equations' RHS when testing equation compatibility","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"FeatureRequest","description":"The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf\r\n\r\nThere in Definition 8 in section 3.4 it states:\r\n\r\nDefinition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.\r\n\r\nExamine the following families:\r\n\r\n{{{#!hs\r\ntype family If (a :: Bool) (b :: k) (c :: k) :: k where\r\n If False a b = b\r\n If True a b = a\r\n\r\ntype family Eql (a :: k) (b :: k) :: Bool where\r\n Eql a a = True\r\n Eql _ _ = False\r\n\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing\r\n Test a a = a\r\n Test Nothing _ = Nothing\r\n Test _ Nothing = Nothing\r\n}}}\r\n\r\nApplying the check to the equations 1 and 2 of `Test` we get:\r\n\r\nunify(<`Just x`, `Just y`>, <`a`, `a`>) = Ω = [`a` > `Just x`, `y` > `x`]\r\n\r\nΩ(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)\r\n\r\nTherefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`\r\n\r\nThat doesn't happen:\r\n{{{#!hs\r\n> :t undefined :: p a > p (Test a a)\r\np a > p (Test a a)\r\n}}}\r\n\r\nExamining the IfaceAxBranches (cf #15546) we see:\r\n{{{#!hs\r\n axiom D:R:Test::\r\n Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing\r\n Test k a a = a\r\n (incompatible indices: [0])\r\n Test k 'Nothing _ = 'Nothing\r\n Test k _ 'Nothing = 'Nothing\r\n}}}\r\n\r\nGHC did not consider the two equations compatible.\r\n\r\nDigging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:10, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).\r\n\r\nThe family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).\r\n\r\nThis brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?\r\n\r\nP.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:\r\n{{{#!hs\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing\r\n Test a a = If (Eql a a) a Nothing\r\n Test Nothing a = If (Eql Nothing a) Nothing Nothing\r\n Test a Nothing = If (Eql a Nothing) Nothing Nothing\r\n}}}\r\n\r\nThis lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.\r\n\r\nP.P.S: In ticket:15546#comment:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.","type_of_failure":"OtherFailure","blocking":[]} >The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf
There in Definition 8 in section 3.4 it states:
Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.
Examine the following families:
```hs
type family If (a :: Bool) (b :: k) (c :: k) :: k where
If False a b = b
If True a b = a
type family Eql (a :: k) (b :: k) :: Bool where
Eql a a = True
Eql _ _ = False
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
Test a a = a
Test Nothing _ = Nothing
Test _ Nothing = Nothing
```
Applying the check to the equations 1 and 2 of `Test` we get:
unify(\<`Just x`, `Just y`\>, \<`a`, `a`\>) = Ω = \[`a` \> `Just x`, `y` \> `x`\]
Ω(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)
Therefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`
That doesn't happen:
```hs
> :t undefined :: p a > p (Test a a)
p a > p (Test a a)
```
Examining the IfaceAxBranches (cf #15546) we see:
```hs
axiom D:R:Test::
Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
Test k a a = a
(incompatible indices: [0])
Test k 'Nothing _ = 'Nothing
Test k _ 'Nothing = 'Nothing
```
GHC did not consider the two equations compatible.
Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's [ticket:8423\#comment:80951](https://gitlab.haskell.org//ghc/ghc/issues/8423#note_80951), but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).
The family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).
This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?
P.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:
```hs
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
Test a a = If (Eql a a) a Nothing
Test Nothing a = If (Eql Nothing a) Nothing Nothing
Test a Nothing = If (Eql a Nothing) Nothing Nothing
```
This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.
P.P.S: In [ticket:15546\#comment:158797](https://gitlab.haskell.org//ghc/ghc/issues/15546#note_158797) I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 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":"Reduce type families in equations' RHS when testing equation compatibility","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"FeatureRequest","description":"The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf\r\n\r\nThere in Definition 8 in section 3.4 it states:\r\n\r\nDefinition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.\r\n\r\nExamine the following families:\r\n\r\n{{{#!hs\r\ntype family If (a :: Bool) (b :: k) (c :: k) :: k where\r\n If False a b = b\r\n If True a b = a\r\n\r\ntype family Eql (a :: k) (b :: k) :: Bool where\r\n Eql a a = True\r\n Eql _ _ = False\r\n\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing\r\n Test a a = a\r\n Test Nothing _ = Nothing\r\n Test _ Nothing = Nothing\r\n}}}\r\n\r\nApplying the check to the equations 1 and 2 of `Test` we get:\r\n\r\nunify(<`Just x`, `Just y`>, <`a`, `a`>) = Ω = [`a` > `Just x`, `y` > `x`]\r\n\r\nΩ(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)\r\n\r\nTherefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`\r\n\r\nThat doesn't happen:\r\n{{{#!hs\r\n> :t undefined :: p a > p (Test a a)\r\np a > p (Test a a)\r\n}}}\r\n\r\nExamining the IfaceAxBranches (cf #15546) we see:\r\n{{{#!hs\r\n axiom D:R:Test::\r\n Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing\r\n Test k a a = a\r\n (incompatible indices: [0])\r\n Test k 'Nothing _ = 'Nothing\r\n Test k _ 'Nothing = 'Nothing\r\n}}}\r\n\r\nGHC did not consider the two equations compatible.\r\n\r\nDigging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:10, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).\r\n\r\nThe family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).\r\n\r\nThis brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?\r\n\r\nP.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:\r\n{{{#!hs\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing\r\n Test a a = If (Eql a a) a Nothing\r\n Test Nothing a = If (Eql Nothing a) Nothing Nothing\r\n Test a Nothing = If (Eql a Nothing) Nothing Nothing\r\n}}}\r\n\r\nThis lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.\r\n\r\nP.P.S: In ticket:15546#comment:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15549Core Lint error with EmptyCase20190707T18:04:11ZRyan ScottCore Lint error with EmptyCaseThe following program gives a Core Lint error on GHC 8.2.2 and later:
```hs
{# LANGUAGE EmptyCase #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Void
data family Sing (a :: k)
data V1 :: Type > Type
data instance Sing (z :: V1 p)
class Generic a where
type Rep a :: Type > Type
to :: Rep a x > a
class PGeneric a where
type To (z :: Rep a x) :: a
class SGeneric a where
sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)

instance Generic Void where
type Rep Void = V1
to x = case x of {}
type family EmptyCase (a :: j) :: k where
instance PGeneric Void where
type To x = EmptyCase x
instance SGeneric Void where
sTo x = case x of
```
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
Function kind = forall k. k > *
Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
*** Offending Program ***
<elided>
$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)
[LclId,
Arity=1,
Str=<L,U>x,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
= \ (@ x_a12p)
(@ (r_a12q :: Rep Void x_a12p))
(x_aZ8 :: Sing r_a12q) >
case x_aZ8
`cast` ((Sing
(D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
<x_a12p>_N <r_a12q>_N
:: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
of nt_s13T {
}
```
GHC 8.0.2 does not appear to suffer from this Core Lint error.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 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":"Core Lint error with empty closed type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program gives a Core Lint error on GHC 8.2.2 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata V1 :: Type > Type\r\ndata instance Sing (z :: V1 p)\r\n\r\nclass Generic a where\r\n type Rep a :: Type > Type\r\n to :: Rep a x > a\r\n\r\nclass PGeneric a where\r\n type To (z :: Rep a x) :: a\r\n\r\nclass SGeneric a where\r\n sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)\r\n\r\n\r\n\r\ninstance Generic Void where\r\n type Rep Void = V1\r\n to x = case x of {}\r\n\r\ntype family EmptyCase (a :: j) :: k where\r\n\r\ninstance PGeneric Void where\r\n type To x = EmptyCase x\r\n\r\ninstance SGeneric Void where\r\n sTo x = case x of\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’\r\n Function kind = forall k. k > *\r\n Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\n$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)\r\n[LclId,\r\n Arity=1,\r\n Str=<L,U>x,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,\r\n WorkFree=True, Expandable=True,\r\n Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]\r\n$csTo_a12n\r\n = \\ (@ x_a12p)\r\n (@ (r_a12q :: Rep Void x_a12p))\r\n (x_aZ8 :: Sing r_a12q) >\r\n case x_aZ8\r\n `cast` ((Sing\r\n (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]\r\n <x_a12p>_N <r_a12q>_N\r\n :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))\r\n of nt_s13T {\r\n }\r\n}}}\r\n\r\nGHC 8.0.2 does not appear to suffer from this Core Lint error.","type_of_failure":"OtherFailure","blocking":[]} >The following program gives a Core Lint error on GHC 8.2.2 and later:
```hs
{# LANGUAGE EmptyCase #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Void
data family Sing (a :: k)
data V1 :: Type > Type
data instance Sing (z :: V1 p)
class Generic a where
type Rep a :: Type > Type
to :: Rep a x > a
class PGeneric a where
type To (z :: Rep a x) :: a
class SGeneric a where
sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)

instance Generic Void where
type Rep Void = V1
to x = case x of {}
type family EmptyCase (a :: j) :: k where
instance PGeneric Void where
type To x = EmptyCase x
instance SGeneric Void where
sTo x = case x of
```
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
Function kind = forall k. k > *
Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
*** Offending Program ***
<elided>
$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)
[LclId,
Arity=1,
Str=<L,U>x,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
= \ (@ x_a12p)
(@ (r_a12q :: Rep Void x_a12p))
(x_aZ8 :: Sing r_a12q) >
case x_aZ8
`cast` ((Sing
(D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
<x_a12p>_N <r_a12q>_N
:: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
of nt_s13T {
}
```
GHC 8.0.2 does not appear to suffer from this Core Lint error.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 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":"Core Lint error with empty closed type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program gives a Core Lint error on GHC 8.2.2 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata V1 :: Type > Type\r\ndata instance Sing (z :: V1 p)\r\n\r\nclass Generic a where\r\n type Rep a :: Type > Type\r\n to :: Rep a x > a\r\n\r\nclass PGeneric a where\r\n type To (z :: Rep a x) :: a\r\n\r\nclass SGeneric a where\r\n sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)\r\n\r\n\r\n\r\ninstance Generic Void where\r\n type Rep Void = V1\r\n to x = case x of {}\r\n\r\ntype family EmptyCase (a :: j) :: k where\r\n\r\ninstance PGeneric Void where\r\n type To x = EmptyCase x\r\n\r\ninstance SGeneric Void where\r\n sTo x = case x of\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’\r\n Function kind = forall k. k > *\r\n Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\n$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)\r\n[LclId,\r\n Arity=1,\r\n Str=<L,U>x,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,\r\n WorkFree=True, Expandable=True,\r\n Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]\r\n$csTo_a12n\r\n = \\ (@ x_a12p)\r\n (@ (r_a12q :: Rep Void x_a12p))\r\n (x_aZ8 :: Sing r_a12q) >\r\n case x_aZ8\r\n `cast` ((Sing\r\n (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]\r\n <x_a12p>_N <r_a12q>_N\r\n :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))\r\n of nt_s13T {\r\n }\r\n}}}\r\n\r\nGHC 8.0.2 does not appear to suffer from this Core Lint error.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1