GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20200218T12:30:12Zhttps://gitlab.haskell.org/ghc/ghc/issues/16877GHCi panics using fdefertypeerrors when pattern matching on types with mul...20200218T12:30:12ZBerengalGHCi panics using fdefertypeerrors when pattern matching on types with multiple constructors using outofscope variables# Summary
With fdefertypeerrors enabled GHCi will panic on certain errors involving pattern matching on types with multiple constructors. At least as far as I can tell.
# Steps to reproduce
The following is the smallest module I could find that causes the panic:
```
foo = x
where (x:xs) = bar
```
GHCi command and output:
```
▶ ghci ignoredotghci fdefertypeerrors Foo.hs
GHCi, version 8.6.5: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:2:18: warning: [Wdeferredoutofscopevariables]
Variable not in scope: bar :: [a1]

2  where (x:xs) = bar
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.5 for x86_64unknownlinux):
getIdFromTrivialExpr
\ (@ a_a1x4) > case ds_s1yU @ a_a1x4 of wild_Xb { }
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/coreSyn/CoreUtils.hs:977:18 in ghc:CoreUtils
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
The equivalent using `let` also panics. The pattern match in the where is neccessary, as is using a matched variable in the main expression (either one will do). Matching on a tuple does not cause a panic, nor does matching on `data Foo a = Foo a a`, but matching on `data Foo a = Foo a a  Bar a a` panics regardless of which constructor is chosen.
# Expected behavior
GHCi doesn't panic, but either loads the module correctly or explains why it can't do so.
# Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Archlinux
* System Architecture: x86_64# Summary
With fdefertypeerrors enabled GHCi will panic on certain errors involving pattern matching on types with multiple constructors. At least as far as I can tell.
# Steps to reproduce
The following is the smallest module I could find that causes the panic:
```
foo = x
where (x:xs) = bar
```
GHCi command and output:
```
▶ ghci ignoredotghci fdefertypeerrors Foo.hs
GHCi, version 8.6.5: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:2:18: warning: [Wdeferredoutofscopevariables]
Variable not in scope: bar :: [a1]

2  where (x:xs) = bar
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.5 for x86_64unknownlinux):
getIdFromTrivialExpr
\ (@ a_a1x4) > case ds_s1yU @ a_a1x4 of wild_Xb { }
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/coreSyn/CoreUtils.hs:977:18 in ghc:CoreUtils
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
The equivalent using `let` also panics. The pattern match in the where is neccessary, as is using a matched variable in the main expression (either one will do). Matching on a tuple does not cause a panic, nor does matching on `data Foo a = Foo a a`, but matching on `data Foo a = Foo a a  Bar a a` panics regardless of which constructor is chosen.
# Expected behavior
GHCi doesn't panic, but either loads the module correctly or explains why it can't do so.
# Environment
* GHC version used: 8.6.5
Optional:
* Operating System: Archlinux
* System Architecture: x86_648.8.2https://gitlab.haskell.org/ghc/ghc/issues/16775Don't zap naughty quantification candidates: error instead20200113T10:52:17ZRichard Eisenbergrae@richarde.devDon't zap naughty quantification candidates: error insteadNote [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to `Any`.
However, we recently decided not to `Any`ify in type declarations. And I think we are wrong to `Any`ify here, too. We should just error. If not, we risk having `Any` leak in error messages, and it seems a nice goal not to ever let users see `Any` (short of TH or reflection or other dastardly deeds).
The example is `partialsigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_168778 reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locallybound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that `tcHsPartialSigType` was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions `Any`.
Here is a simpler test case:
```
foo :: forall (f :: forall a (b :: a > Type). b _). f _
foo = foo
```
Note that the type of the first `_` must be `a`, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get
```
• Expected kind ‘k > *’, but ‘f’ has kind ‘k > Any @*’
• In the type ‘f _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). f _
```
This is correct enough, but there's `Any` in the error message. I think it would be much better just to reject the type signature a priori.
If I make the program correct (by wrapping the `f _` in a call to `Proxy`, I get
```
Scratch.hs:44:50: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘Any @a :: a’
Where: ‘a’ is a rigid type variable bound by
‘forall a (b :: a > Type). b _’
at Scratch.hs:44:28
• In the first argument of ‘b’, namely ‘_’
In the kind ‘forall a (b :: a > Type). b _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
Scratch.hs:44:63: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_ :: k’
Where: ‘k’, ‘_’ are rigid type variables bound by
the inferred type of
foo :: Proxy
@{Any @Type} (f @Type @((>) @{'LiftedRep} @{'LiftedRep} k) _)
at Scratch.hs:45:19
• In the first argument of ‘f’, namely ‘_’
In the first argument of ‘Proxy’, namely ‘(f _)’
In the type ‘Proxy (f _)’

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
```
More `Any`s. No! Reject!
What think you (for any value of you)?Note [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to `Any`.
However, we recently decided not to `Any`ify in type declarations. And I think we are wrong to `Any`ify here, too. We should just error. If not, we risk having `Any` leak in error messages, and it seems a nice goal not to ever let users see `Any` (short of TH or reflection or other dastardly deeds).
The example is `partialsigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_168778 reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locallybound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that `tcHsPartialSigType` was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions `Any`.
Here is a simpler test case:
```
foo :: forall (f :: forall a (b :: a > Type). b _). f _
foo = foo
```
Note that the type of the first `_` must be `a`, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get
```
• Expected kind ‘k > *’, but ‘f’ has kind ‘k > Any @*’
• In the type ‘f _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). f _
```
This is correct enough, but there's `Any` in the error message. I think it would be much better just to reject the type signature a priori.
If I make the program correct (by wrapping the `f _` in a call to `Proxy`, I get
```
Scratch.hs:44:50: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘Any @a :: a’
Where: ‘a’ is a rigid type variable bound by
‘forall a (b :: a > Type). b _’
at Scratch.hs:44:28
• In the first argument of ‘b’, namely ‘_’
In the kind ‘forall a (b :: a > Type). b _’
In the type signature:
foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
Scratch.hs:44:63: warning: [Wpartialtypesignatures]
• Found type wildcard ‘_’ standing for ‘_ :: k’
Where: ‘k’, ‘_’ are rigid type variables bound by
the inferred type of
foo :: Proxy
@{Any @Type} (f @Type @((>) @{'LiftedRep} @{'LiftedRep} k) _)
at Scratch.hs:45:19
• In the first argument of ‘f’, namely ‘_’
In the first argument of ‘Proxy’, namely ‘(f _)’
In the type ‘Proxy (f _)’

44  foo :: forall (f :: forall a (b :: a > Type). b _). Proxy (f _)
 ^
```
More `Any`s. No! Reject!
What think you (for any value of you)?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