GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20191108T20:29:02Zhttps://gitlab.haskell.org/ghc/ghc/issues/16387Duplicate vsnwprintf symbol on Windows20191108T20:29:02ZBen GamariDuplicate vsnwprintf symbol on WindowsLeading to failure of `T5836`:
```
Stderr ( T5836 ):
GHC runtime linker: fatal error: I found a duplicate definition for symbol
__mingw_vsnwprintf
whilst processing object file
C:\GitLabRunner\builds\8fc0e283\0\ghc\ghc\inplace\mingw\x86_64w64mingw32\lib\libmingwex.a
The symbol was previously defined in
(GHCi builtin symbols)
This could be caused by:
* Loading two different object files which export the same symbol
* Specifying the same object file twice on the GHCi command line
* An incorrect `package.conf' entry, causing some object to be
loaded twice.
ghcstage2.exe: panic! (the 'impossible' happened)
(GHC version 8.9.20190303 for x86_64unknownmingw32):
loadArchive "C:\\GitLabRunner\\builds\\8fc0e283\\0\\ghc\\ghc\\inplace\\mingw\\x86_64w64mingw32\\lib\\libmingwex.a": failed
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
*** unexpected failure for T5836(ghci)
```Leading to failure of `T5836`:
```
Stderr ( T5836 ):
GHC runtime linker: fatal error: I found a duplicate definition for symbol
__mingw_vsnwprintf
whilst processing object file
C:\GitLabRunner\builds\8fc0e283\0\ghc\ghc\inplace\mingw\x86_64w64mingw32\lib\libmingwex.a
The symbol was previously defined in
(GHCi builtin symbols)
This could be caused by:
* Loading two different object files which export the same symbol
* Specifying the same object file twice on the GHCi command line
* An incorrect `package.conf' entry, causing some object to be
loaded twice.
ghcstage2.exe: panic! (the 'impossible' happened)
(GHC version 8.9.20190303 for x86_64unknownmingw32):
loadArchive "C:\\GitLabRunner\\builds\\8fc0e283\\0\\ghc\\ghc\\inplace\\mingw\\x86_64w64mingw32\\lib\\libmingwex.a": failed
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
*** unexpected failure for T5836(ghci)
```8.8.2https://gitlab.haskell.org/ghc/ghc/issues/15742GHC configure step can fail when CC=clang20191103T01:44:03ZjudahGHC configure step can fail when CC=clangIn our internal build of GHC from source, we are building it on Linux with Clang. Unfortunately, this results in an error on ghc8.4.3:
```
$ ./configure CC=clang CC_STAGE0=clang prefix=... withghc=...
...
checking version of gcc... configure: error: Need at least gcc version 4.4 (4.7+ recommended)
```
Looking in the code, it seems that the logic is wrong: it calls `$CC v` and parses the output unconditionally, whether or not the compiler is actually GCC:
https://github.com/ghc/ghc/blob/ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2/aclocal.m4\#L1245
In our case, the test fails since the compiler is a build of Clang that doesn't produce a useful version number.
I also realized that on macOS (where gcc \*is\* clang), this test succeeds accidentally, since the output of `gcc v` is:
```
Configured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1
Apple LLVM version 10.0.0 (clang1000.10.44.2)
Target: x86_64appledarwin17.7.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
judahjacobsonmacbookpro:~ judahjacobson$ gcc v
Configured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1
Apple LLVM version 10.0.0 (clang1000.10.44.2)
Target: x86_64appledarwin17.7.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Build System 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC configure step can fail when CC=clang","status":"New","operating_system":"","component":"Build System","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In our internal build of GHC from source, we are building it on Linux with Clang. Unfortunately, this results in an error on ghc8.4.3:\r\n{{{\r\n$ ./configure CC=clang CC_STAGE0=clang prefix=... withghc=...\r\n...\r\nchecking version of gcc... configure: error: Need at least gcc version 4.4 (4.7+ recommended)\r\n}}}\r\nLooking in the code, it seems that the logic is wrong: it calls `$CC v` and parses the output unconditionally, whether or not the compiler is actually GCC:\r\nhttps://github.com/ghc/ghc/blob/ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2/aclocal.m4#L1245\r\nIn our case, the test fails since the compiler is a build of Clang that doesn't produce a useful version number.\r\n\r\nI also realized that on macOS (where gcc *is* clang), this test succeeds accidentally, since the output of {{{gcc v}}} is:\r\n{{{\r\nConfigured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1\r\nApple LLVM version 10.0.0 (clang1000.10.44.2)\r\nTarget: x86_64appledarwin17.7.0\r\nThread model: posix\r\nInstalledDir: /Library/Developer/CommandLineTools/usr/bin\r\njudahjacobsonmacbookpro:~ judahjacobson$ gcc v\r\nConfigured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1\r\nApple LLVM version 10.0.0 (clang1000.10.44.2)\r\nTarget: x86_64appledarwin17.7.0\r\nThread model: posix\r\nInstalledDir: /Library/Developer/CommandLineTools/usr/bin\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >In our internal build of GHC from source, we are building it on Linux with Clang. Unfortunately, this results in an error on ghc8.4.3:
```
$ ./configure CC=clang CC_STAGE0=clang prefix=... withghc=...
...
checking version of gcc... configure: error: Need at least gcc version 4.4 (4.7+ recommended)
```
Looking in the code, it seems that the logic is wrong: it calls `$CC v` and parses the output unconditionally, whether or not the compiler is actually GCC:
https://github.com/ghc/ghc/blob/ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2/aclocal.m4\#L1245
In our case, the test fails since the compiler is a build of Clang that doesn't produce a useful version number.
I also realized that on macOS (where gcc \*is\* clang), this test succeeds accidentally, since the output of `gcc v` is:
```
Configured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1
Apple LLVM version 10.0.0 (clang1000.10.44.2)
Target: x86_64appledarwin17.7.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
judahjacobsonmacbookpro:~ judahjacobson$ gcc v
Configured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1
Apple LLVM version 10.0.0 (clang1000.10.44.2)
Target: x86_64appledarwin17.7.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Build System 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC configure step can fail when CC=clang","status":"New","operating_system":"","component":"Build System","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In our internal build of GHC from source, we are building it on Linux with Clang. Unfortunately, this results in an error on ghc8.4.3:\r\n{{{\r\n$ ./configure CC=clang CC_STAGE0=clang prefix=... withghc=...\r\n...\r\nchecking version of gcc... configure: error: Need at least gcc version 4.4 (4.7+ recommended)\r\n}}}\r\nLooking in the code, it seems that the logic is wrong: it calls `$CC v` and parses the output unconditionally, whether or not the compiler is actually GCC:\r\nhttps://github.com/ghc/ghc/blob/ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2/aclocal.m4#L1245\r\nIn our case, the test fails since the compiler is a build of Clang that doesn't produce a useful version number.\r\n\r\nI also realized that on macOS (where gcc *is* clang), this test succeeds accidentally, since the output of {{{gcc v}}} is:\r\n{{{\r\nConfigured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1\r\nApple LLVM version 10.0.0 (clang1000.10.44.2)\r\nTarget: x86_64appledarwin17.7.0\r\nThread model: posix\r\nInstalledDir: /Library/Developer/CommandLineTools/usr/bin\r\njudahjacobsonmacbookpro:~ judahjacobson$ gcc v\r\nConfigured with: prefix=/Library/Developer/CommandLineTools/usr withgxxincludedir=/usr/include/c++/4.2.1\r\nApple LLVM version 10.0.0 (clang1000.10.44.2)\r\nTarget: x86_64appledarwin17.7.0\r\nThread model: posix\r\nInstalledDir: /Library/Developer/CommandLineTools/usr/bin\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.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.2Ben GamariAlp Mestanogullarialp@welltyped.comBen Gamari