GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20191108T11:09:14Zhttps://gitlab.haskell.org/ghc/ghc/issues/17428GHC produces an incorrect DWARF .debug_aranges section in some cases20191108T11:09:14ZSzymon NowickiKorgolGHC produces an incorrect DWARF .debug_aranges section in some cases## Summary
When parsing the `.debug_aranges` section of code produced by GHC (for example using the [folly symboliser](https://github.com/facebook/folly/tree/master/folly/experimental/symbolizer)) the parsing fails because of an incorrect value of the length field.
The bug seems to be here:
https://gitlab.haskell.org/ghc/ghc/blob/4898df1cc25132dc9e2599d4fa4e1bbc9423cda5/compiler/nativeGen/Dwarf/Types.hs#L233
where the `initialLength` is set to a constant value, while the length should depend on the amount of address range entries in a given section.
It seems to have been introduced in this commit:
https://gitlab.haskell.org/ghc/ghc/commit/4a32bf925b8aba7885d9c745769fe84a10979a53
where the capability to create a `.debug_aranges` section with multiple address ranges was added, but the calculation for `initialLength` was not changed.
## Environment
* GHC version used: 8.4.4## Summary
When parsing the `.debug_aranges` section of code produced by GHC (for example using the [folly symboliser](https://github.com/facebook/folly/tree/master/folly/experimental/symbolizer)) the parsing fails because of an incorrect value of the length field.
The bug seems to be here:
https://gitlab.haskell.org/ghc/ghc/blob/4898df1cc25132dc9e2599d4fa4e1bbc9423cda5/compiler/nativeGen/Dwarf/Types.hs#L233
where the `initialLength` is set to a constant value, while the length should depend on the amount of address range entries in a given section.
It seems to have been introduced in this commit:
https://gitlab.haskell.org/ghc/ghc/commit/4a32bf925b8aba7885d9c745769fe84a10979a53
where the capability to create a `.debug_aranges` section with multiple address ranges was added, but the calculation for `initialLength` was not changed.
## Environment
* GHC version used: 8.4.48.8.2https://gitlab.haskell.org/ghc/ghc/issues/17297CNF.c:insertCompactHash doesn't correctly dirty regions20191103T20:24:49ZBen GamariCNF.c:insertCompactHash doesn't correctly dirty regionsConsider `CNF.c:insertCompactHash`:
```c
void
insertCompactHash (Capability *cap,
StgCompactNFData *str,
StgClosure *p, StgClosure *to)
{
insertHashTable(str>hash, (StgWord)p, (const void*)to);
const StgInfoTable *strinfo = &str>header.info;
if (strinfo == &stg_COMPACT_NFDATA_CLEAN_info) {
strinfo = &stg_COMPACT_NFDATA_DIRTY_info;
recordClosureMutated(cap, (StgClosure*)str);
}
}
```
At first glance this looks reasonable. However, note how we are dirtying the region:
```
strinfo = &stg_COMPACT_NFDATA_DIRTY_info;
```
This does not do at all what we want; it simply sets the local variable, not the info table pointer.
For this reason compact regions with sharing preservation enabled get added to the `mut_list` once for every object in the region. Terrible!Consider `CNF.c:insertCompactHash`:
```c
void
insertCompactHash (Capability *cap,
StgCompactNFData *str,
StgClosure *p, StgClosure *to)
{
insertHashTable(str>hash, (StgWord)p, (const void*)to);
const StgInfoTable *strinfo = &str>header.info;
if (strinfo == &stg_COMPACT_NFDATA_CLEAN_info) {
strinfo = &stg_COMPACT_NFDATA_DIRTY_info;
recordClosureMutated(cap, (StgClosure*)str);
}
}
```
At first glance this looks reasonable. However, note how we are dirtying the region:
```
strinfo = &stg_COMPACT_NFDATA_DIRTY_info;
```
This does not do at all what we want; it simply sets the local variable, not the info table pointer.
For this reason compact regions with sharing preservation enabled get added to the `mut_list` once for every object in the region. Terrible!8.8.2Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/issues/17265Source distributions contain rts.cabal20191103T20:24:49ZJudah JacobsonSource distributions contain rts.cabal## Summary
GHC source distributions contain the file `rts.cabal`, which is generated by the build. That file should probably be excluded from source distributions.
## Steps to reproduce
```
$ tar tf ghc8.8.1src.tar.xz  grep rts.cabal
ghc8.8.1/rts/rts.cabal.in
ghc8.8.1/rts/rts.cabal
```
I also confirmed that this is still happening in HEAD with Hadrian:
```
$ tar tf _build/sourcedist/ghc8.9.0.20190926src.tar.xz  grep rts.cabal
_build/sourcedist/ghc8.9.0.20190926src/rts/rts.cabal
_build/sourcedist/ghc8.9.0.20190926src/rts/rts.cabal.in
```
## Expected behavior
The tarballs should not include `rts.cabal`.
## Environment
* GHC version used: 8.6.4 and 8.8.1## Summary
GHC source distributions contain the file `rts.cabal`, which is generated by the build. That file should probably be excluded from source distributions.
## Steps to reproduce
```
$ tar tf ghc8.8.1src.tar.xz  grep rts.cabal
ghc8.8.1/rts/rts.cabal.in
ghc8.8.1/rts/rts.cabal
```
I also confirmed that this is still happening in HEAD with Hadrian:
```
$ tar tf _build/sourcedist/ghc8.9.0.20190926src.tar.xz  grep rts.cabal
_build/sourcedist/ghc8.9.0.20190926src/rts/rts.cabal
_build/sourcedist/ghc8.9.0.20190926src/rts/rts.cabal.in
```
## Expected behavior
The tarballs should not include `rts.cabal`.
## Environment
* GHC version used: 8.6.4 and 8.8.18.8.2https://gitlab.haskell.org/ghc/ghc/issues/17107Sphinx documentation missing in Darwin bindists20191206T20:07:45ZBen GamariSphinx documentation missing in Darwin bindists'Tis all.'Tis all.8.8.2Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/issues/17044Putting large objects in compact regions causes a segfault under the right co...20191103T20:24:49ZFabian ThorandPutting large objects in compact regions causes a segfault under the right conditions## Summary
When putting a large object in a compact region, and then several smaller ones afterwards,
the program crashes with a segfault because the GC tries to follow an invalid pointer.
## Steps to reproduce
The following Haskell program reliably causes a segfault for me:
```haskell
import Data.Traversable (for)
import Data.Primitive.ByteArray
import GHC.Compact
import System.Mem (performGC)
main :: IO ()
main = do
 Make a fresh compact region. So far, it only contains a single almost empty small block
c < compact ()
print =<< compactSize c  prints 32768, as the default block size is 32K
 Now add a big object to the compact region. The size is chosen so that the compact region
 allocator will allocate two megablocks while actually leaving space in the first megablock.
let
totalSizeInWords = 129016
arraySizeInWords = totalSizeInWords  2 { header words }
big < newByteArray (arraySizeInWords * 8)
bigFrozen < unsafeFreezeByteArray big
 Add the big object to the compact region.
 It is larger than the existing block, and also larger than the big object threshold.
 The `ByteArray` wrapper is likely put still into the first block,
 but the `ByteArray#` is put in a new block.
 One can fit 129024 words into a megablock. Our object is 129016 words in size,
 but the allocator reserves a bit too much space, so it needs to allocate 129025 words,
 and therefore two megablocks.
_ < compactAdd c bigFrozen
print =<< compactSize c  prints 2113536, because it allocated a megablock group of 2 megablocks
 Now we have to fill the first block, which is currently the nursery,
 and eventually, one of the Ints will be added to the second block,
 causing the segfault.
placeholders < for [0 :: Int ..10000] $ \i > do
r < getCompact <$> compactAdd c i
print i
performGC
pure r
 Keep the placeholders alive so the GC actually has a pointer to follow into the invalid
 parts of the compact region.
print $ length placeholders
```
I dug a bit into the RTS source code, but I don't yet fully understand what is going on.
The segfault above is the result of an invariant about megablock groups that is violated by `allocateForCompact`.
In the example program, when we start adding the `Int`s in a loop, it will first allocate them from the nursery,
which at that point is still the first block of the compact region.
I think that those allocations happen in the `ALLOCATE` macro (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/Compact.cmm#L25).
Then, once the nursery is full, `allocateForCompact` is called (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/Compact.cmm#L29).
There, it first does the same check on the nursery as the `ALLOCATE` macro (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L479), which obviously fails.
Then it proceeds, and it will find that the `Int` is not a large object, therefore skipping the special logic there (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L490).
However, then it will find that the nursery is full (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L501) and pick the next block that is not full as new nursery.
In the example above, there is a new block: the one that was allocated for the large array. It consists of 2 megablocks,
but it's `free` pointer still points within the first megablock, and there's enough room, so it picks that block.
But once that block has been chosen as a nursery, it will start allocating closures even in the second megablock of that group. If I understand the comment in BlockAlloc.c (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/BlockAlloc.c#L120) correctly, this violates the invariants of megablock groups, as closures that are allocated there don't have a valid `bdescr` of the block they've been placed into.
The remaining question is: why is there still space left in the first megablock, when the allocator actually allocated two megablocks?
I think this is because the size computation for large objects at https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L491.
It reserves room for an `StgCompactNFData` while only space for a `StgCompactNFDataBlock` is needed.
I tried to fix this by changing it to not picking megablock groups as nursery,
and that indeed fixed the issue above, but then we got other segfaults that
I wasn't able to reliably reproduce yet, as they occurred as part of a large application.
It could be that the loop that tries to fit the allocation in subsequent blocks (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L517) is at fault, as it would still put more than one object into a megablock allocation, while https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/BlockAlloc.c#L117 seems to imply that only a single object should be put in those.
Additionally, the `bdescr` initialization in `compactAllocateBlockInternal` (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L247) seems to write into the data area of the allocation when the allocated area is larger than one megablock.
## Expected behavior
I expect the program to print the sizes of the compact regions and then all numbers from 0 to 10000,
and not segfault after printing number 2046.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System: Ubuntu 18.04
* System Architecture: x86_64## Summary
When putting a large object in a compact region, and then several smaller ones afterwards,
the program crashes with a segfault because the GC tries to follow an invalid pointer.
## Steps to reproduce
The following Haskell program reliably causes a segfault for me:
```haskell
import Data.Traversable (for)
import Data.Primitive.ByteArray
import GHC.Compact
import System.Mem (performGC)
main :: IO ()
main = do
 Make a fresh compact region. So far, it only contains a single almost empty small block
c < compact ()
print =<< compactSize c  prints 32768, as the default block size is 32K
 Now add a big object to the compact region. The size is chosen so that the compact region
 allocator will allocate two megablocks while actually leaving space in the first megablock.
let
totalSizeInWords = 129016
arraySizeInWords = totalSizeInWords  2 { header words }
big < newByteArray (arraySizeInWords * 8)
bigFrozen < unsafeFreezeByteArray big
 Add the big object to the compact region.
 It is larger than the existing block, and also larger than the big object threshold.
 The `ByteArray` wrapper is likely put still into the first block,
 but the `ByteArray#` is put in a new block.
 One can fit 129024 words into a megablock. Our object is 129016 words in size,
 but the allocator reserves a bit too much space, so it needs to allocate 129025 words,
 and therefore two megablocks.
_ < compactAdd c bigFrozen
print =<< compactSize c  prints 2113536, because it allocated a megablock group of 2 megablocks
 Now we have to fill the first block, which is currently the nursery,
 and eventually, one of the Ints will be added to the second block,
 causing the segfault.
placeholders < for [0 :: Int ..10000] $ \i > do
r < getCompact <$> compactAdd c i
print i
performGC
pure r
 Keep the placeholders alive so the GC actually has a pointer to follow into the invalid
 parts of the compact region.
print $ length placeholders
```
I dug a bit into the RTS source code, but I don't yet fully understand what is going on.
The segfault above is the result of an invariant about megablock groups that is violated by `allocateForCompact`.
In the example program, when we start adding the `Int`s in a loop, it will first allocate them from the nursery,
which at that point is still the first block of the compact region.
I think that those allocations happen in the `ALLOCATE` macro (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/Compact.cmm#L25).
Then, once the nursery is full, `allocateForCompact` is called (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/Compact.cmm#L29).
There, it first does the same check on the nursery as the `ALLOCATE` macro (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L479), which obviously fails.
Then it proceeds, and it will find that the `Int` is not a large object, therefore skipping the special logic there (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L490).
However, then it will find that the nursery is full (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L501) and pick the next block that is not full as new nursery.
In the example above, there is a new block: the one that was allocated for the large array. It consists of 2 megablocks,
but it's `free` pointer still points within the first megablock, and there's enough room, so it picks that block.
But once that block has been chosen as a nursery, it will start allocating closures even in the second megablock of that group. If I understand the comment in BlockAlloc.c (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/BlockAlloc.c#L120) correctly, this violates the invariants of megablock groups, as closures that are allocated there don't have a valid `bdescr` of the block they've been placed into.
The remaining question is: why is there still space left in the first megablock, when the allocator actually allocated two megablocks?
I think this is because the size computation for large objects at https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L491.
It reserves room for an `StgCompactNFData` while only space for a `StgCompactNFDataBlock` is needed.
I tried to fix this by changing it to not picking megablock groups as nursery,
and that indeed fixed the issue above, but then we got other segfaults that
I wasn't able to reliably reproduce yet, as they occurred as part of a large application.
It could be that the loop that tries to fit the allocation in subsequent blocks (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L517) is at fault, as it would still put more than one object into a megablock allocation, while https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/BlockAlloc.c#L117 seems to imply that only a single object should be put in those.
Additionally, the `bdescr` initialization in `compactAllocateBlockInternal` (https://gitlab.haskell.org/ghc/ghc/blob/ghc8.6.3release/rts/sm/CNF.c#L247) seems to write into the data area of the allocation when the allocated area is larger than one megablock.
## Expected behavior
I expect the program to print the sizes of the compact regions and then all numbers from 0 to 10000,
and not segfault after printing number 2046.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System: Ubuntu 18.04
* System Architecture: x86_648.8.2https://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 Mestanogullarialp@welltyped.comBen GamariAlp Mestanogullarialp@welltyped.com