GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210111T13:07:45Zhttps://gitlab.haskell.org/ghc/ghc//issues/17562`Any` appearing in a quantified constraint20210111T13:07:45ZRichard Eisenbergrae@richarde.dev`Any` appearing in a quantified constraintIf I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.If I say
```hs
{# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #}
module Bug where
class (forall a. a b ~ a c) => C b c
```
I get
```
Bug.hs:5:1: error:
• Illegal type synonym family application ‘GHC.Types.Any
@*’ in instance:
(a b :: GHC.Types.Any @*) ~ (a c :: GHC.Types.Any @*)
• In the quantified constraint ‘forall (a :: k > GHC.Types.Any).
a b ~ a c’
In the context: forall (a :: k > GHC.Types.Any). a b ~ a c
While checking the superclasses of class ‘C’
In the class declaration for ‘C’

5  class (forall a. a b ~ a c) => C b c
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a specific case of #17567. Despite superficial similarity, this is unrelated to #16775.9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/16245GHC panic (No skolem info) with RankNTypes and strange scoping20201231T13:44:06ZRyan ScottGHC panic (No skolem info) with RankNTypes and strange scopingThe following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[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
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[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\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >The following program panics with GHC 8.6.3 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DataKinds #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64unknownlinux):
No skolem info:
[k1_a1X4[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
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64unknownlinux):\r\n No skolem info:\r\n [k1_a1X4[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\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be illscoped.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15316Regarding coherence and implication loops in presence of QuantifiedConstraints20201003T12:38:44ZmniipRegarding coherence and implication loops in presence of QuantifiedConstraintsFirst of all this piece of code:
```hs
{# LANGUAGE RankNTypes, QuantifiedConstraints #}
 NB: disabling these if enabled:
{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}
import Data.Proxy
class Class a where
method :: a
subsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r
subsume _ _ x = x
value :: Proxy a > a
value p = subsume p p method
```
This produces a nonterminating `value` even though nothing warranting recursion was used.
Adding:
```hs
value' :: Class a => Proxy a > a
value' p = subsume p p method
```
Produces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)
If we add:
```hs
joinSubsume :: Proxy a > ((Class a => Class a) => r) > r
joinSubsume p x = subsume p p x
```
The fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.
Another issue is the following:
```hs
{# LANGUAGE ConstraintKinds #}
subsume' :: Proxy c > ((c => c) => r) > r
subsume' _ x = x
```
```
• Reduction stack overflow; size = 201
When simplifying the following type: c
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the type signature:
subsume' :: Proxy c > ((c => c) => r) > r
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Regarding coherence and implication loops in presence of QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First of all this piece of code:\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes, QuantifiedConstraints #}\r\n NB: disabling these if enabled:\r\n{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}\r\n\r\nimport Data.Proxy\r\n\r\nclass Class a where\r\n\t method :: a\r\n\r\nsubsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r\r\nsubsume _ _ x = x\r\n\r\nvalue :: Proxy a > a\r\nvalue p = subsume p p method\r\n}}}\r\n\r\nThis produces a nonterminating `value` even though nothing warranting recursion was used.\r\n\r\nAdding:\r\n{{{#!hs\r\nvalue' :: Class a => Proxy a > a\r\nvalue' p = subsume p p method\r\n}}}\r\nProduces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)\r\n\r\nIf we add:\r\n{{{#!hs\r\njoinSubsume :: Proxy a > ((Class a => Class a) => r) > r\r\njoinSubsume p x = subsume p p x\r\n}}}\r\nThe fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.\r\n\r\nAnother issue is the following:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\nsubsume' :: Proxy c > ((c => c) => r) > r\r\nsubsume' _ x = x\r\n}}}\r\n{{{\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type: c\r\n Use freductiondepth=0 to disable this check\r\n (any upper bound you could choose might fail unpredictably with\r\n minor updates to GHC, so disabling the check is recommended if\r\n you're sure that type checking should terminate)\r\n • In the type signature:\r\n subsume' :: Proxy c > ((c => c) => r) > r\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >First of all this piece of code:
```hs
{# LANGUAGE RankNTypes, QuantifiedConstraints #}
 NB: disabling these if enabled:
{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}
import Data.Proxy
class Class a where
method :: a
subsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r
subsume _ _ x = x
value :: Proxy a > a
value p = subsume p p method
```
This produces a nonterminating `value` even though nothing warranting recursion was used.
Adding:
```hs
value' :: Class a => Proxy a > a
value' p = subsume p p method
```
Produces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)
If we add:
```hs
joinSubsume :: Proxy a > ((Class a => Class a) => r) > r
joinSubsume p x = subsume p p x
```
The fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.
Another issue is the following:
```hs
{# LANGUAGE ConstraintKinds #}
subsume' :: Proxy c > ((c => c) => r) > r
subsume' _ x = x
```
```
• Reduction stack overflow; size = 201
When simplifying the following type: c
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the type signature:
subsume' :: Proxy c > ((c => c) => r) > r
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Regarding coherence and implication loops in presence of QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First of all this piece of code:\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes, QuantifiedConstraints #}\r\n NB: disabling these if enabled:\r\n{# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #}\r\n\r\nimport Data.Proxy\r\n\r\nclass Class a where\r\n\t method :: a\r\n\r\nsubsume :: (Class a => Class b) => Proxy a > Proxy b > ((Class a => Class b) => r) > r\r\nsubsume _ _ x = x\r\n\r\nvalue :: Proxy a > a\r\nvalue p = subsume p p method\r\n}}}\r\n\r\nThis produces a nonterminating `value` even though nothing warranting recursion was used.\r\n\r\nAdding:\r\n{{{#!hs\r\nvalue' :: Class a => Proxy a > a\r\nvalue' p = subsume p p method\r\n}}}\r\nProduces a `value'` that is legitimately equivalent to `method` in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)\r\n\r\nIf we add:\r\n{{{#!hs\r\njoinSubsume :: Proxy a > ((Class a => Class a) => r) > r\r\njoinSubsume p x = subsume p p x\r\n}}}\r\nThe fact that this typechecks suggests that GHC is able to infer `Class a => Class a` at will, which doesn't seem wrong. However, the fact that `Class a` is solved from `Class a => Class a` via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of `UndecidableInstances`.\r\n\r\nAnother issue is the following:\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\nsubsume' :: Proxy c > ((c => c) => r) > r\r\nsubsume' _ x = x\r\n}}}\r\n{{{\r\n • Reduction stack overflow; size = 201\r\n When simplifying the following type: c\r\n Use freductiondepth=0 to disable this check\r\n (any upper bound you could choose might fail unpredictably with\r\n minor updates to GHC, so disabling the check is recommended if\r\n you're sure that type checking should terminate)\r\n • In the type signature:\r\n subsume' :: Proxy c > ((c => c) => r) > r\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.1Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc//issues/17332ImpredicativeTypes lets you pluck QuantifiedConstraints out of nowhere20200924T18:36:49ZRyan ScottImpredicativeTypes lets you pluck QuantifiedConstraints out of nowhereThis typechecks on GHC 8.6.5, 8.8.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import GHC.Exts
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
```
This is, to put it mildly, a bit concerning. Here is the most destructive use case I can find for this:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Main where
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
class (forall a. a) => Bottom where
no :: a
sortOfUnsafeCoerce :: a > b
sortOfUnsafeCoerce
 Dict < aux
= no
main :: IO ()
main = print (sortOfUnsafeCoerce True :: Int)
```
I call this function `sortOfUnsafeCoerce` and not `unsafeCoerce` because I can't actually make it exhibit any sort of unsafety at runtime—it just panics in various ways:
```
$ /opt/ghc/8.8.1/bin/runghc Bug.hs
Bug.hs: Bug.hs: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
nameModule
system irred_a1uI
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Name.hs:249:3 in ghc:Name
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O0 Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
StgCmmEnv: variable not found
irred_a1gL
local binds for:
no
$tc'Dict
$tcBottom
$tcDict
$trModule
$p1Bottom
$tcBottom1_r1HY
$tcBottom2_r1Iz
$tc'Dict1_r1IA
$tc'Dict2_r1IB
$tcDict1_r1IC
$tcDict2_r1ID
$krep_r1IE
$krep1_r1IF
$krep2_r1IG
$krep3_r1IH
$trModule1_r1II
$trModule2_r1IJ
$trModule3_r1IK
$trModule4_r1IL
$krep4_r1IM
$krep5_r1IN
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
piResultTys1
c_a1i0[tau:0]
[Bottom]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1061:5 in ghc:Type
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I'm unclear if this is the same underlying issue as #17267, but I thought I would file a separate ticket just to be sure.This typechecks on GHC 8.6.5, 8.8.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE QuantifiedConstraints #}
module Bug where
import GHC.Exts
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
```
This is, to put it mildly, a bit concerning. Here is the most destructive use case I can find for this:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
module Main where
data Dict c = c => Dict
aux :: Dict (forall a. a)
aux = Dict
class (forall a. a) => Bottom where
no :: a
sortOfUnsafeCoerce :: a > b
sortOfUnsafeCoerce
 Dict < aux
= no
main :: IO ()
main = print (sortOfUnsafeCoerce True :: Int)
```
I call this function `sortOfUnsafeCoerce` and not `unsafeCoerce` because I can't actually make it exhibit any sort of unsafety at runtime—it just panics in various ways:
```
$ /opt/ghc/8.8.1/bin/runghc Bug.hs
Bug.hs: Bug.hs: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
nameModule
system irred_a1uI
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Name.hs:249:3 in ghc:Name
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O0 Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
StgCmmEnv: variable not found
irred_a1gL
local binds for:
no
$tc'Dict
$tcBottom
$tcDict
$trModule
$p1Bottom
$tcBottom1_r1HY
$tcBottom2_r1Iz
$tc'Dict1_r1IA
$tc'Dict2_r1IB
$tcDict1_r1IC
$tcDict2_r1ID
$krep_r1IE
$krep1_r1IF
$krep2_r1IG
$krep3_r1IH
$trModule1_r1II
$trModule2_r1IJ
$trModule3_r1IK
$trModule4_r1IL
$krep4_r1IM
$krep5_r1IN
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
$ /opt/ghc/8.8.1/bin/ghc O Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64unknownlinux):
piResultTys1
c_a1i0[tau:0]
[Bottom]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1061:5 in ghc:Type
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I'm unclear if this is the same underlying issue as #17267, but I thought I would file a separate ticket just to be sure.https://gitlab.haskell.org/ghc/ghc//issues/18071:instances returns ill kinded result when combined with QuantifiedConstraints20200528T20:58:32ZRyan Scott:instances returns ill kinded result when combined with QuantifiedConstraintsIf I load the following module into GHCi:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
class (forall (z :: k). Show (Proxy z)) => ShowProxy (k :: Type)
instance (forall (z :: k). Show (Proxy z)) => ShowProxy (k :: Type)
data T :: Type > Type
```
And then run the following GHCi command, here is what I get:
```
$ ghci Bug.hs
GHCi, version 8.10.1: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :instances T
instance [safe] ShowProxy T  Defined at Bug.hs:11:10
```
`instance ShowProxy T` is utter nonsense, and that won't even kindcheck:
```
λ> :kind ShowProxy T
<interactive>:1:11: error:
• Expecting one more argument to ‘T’
Expected a type, but ‘T’ has kind ‘* > *’
• In the first argument of ‘ShowProxy’, namely ‘T’
In the type ‘ShowProxy T’
```
So I have no idea how `:instances` is coming up with that. cc @xldenisIf I load the following module into GHCi:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Proxy
class (forall (z :: k). Show (Proxy z)) => ShowProxy (k :: Type)
instance (forall (z :: k). Show (Proxy z)) => ShowProxy (k :: Type)
data T :: Type > Type
```
And then run the following GHCi command, here is what I get:
```
$ ghci Bug.hs
GHCi, version 8.10.1: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :instances T
instance [safe] ShowProxy T  Defined at Bug.hs:11:10
```
`instance ShowProxy T` is utter nonsense, and that won't even kindcheck:
```
λ> :kind ShowProxy T
<interactive>:1:11: error:
• Expecting one more argument to ‘T’
Expected a type, but ‘T’ has kind ‘* > *’
• In the first argument of ‘ShowProxy’, namely ‘T’
In the type ‘ShowProxy T’
```
So I have no idea how `:instances` is coming up with that. cc @xldenishttps://gitlab.haskell.org/ghc/ghc//issues/15290QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"20200521T11:42:34ZRichard Eisenbergrae@richarde.devQuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:
```hs
{# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #}
module Bug where
import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible )
class Monad m where
(>>=) :: m a > (a > m b) > m b
join :: m (m a) > m a
newtype StateT s m a = StateT { runStateT :: s > m (s, a) }
instance Monad m => Monad (StateT s m) where
ma >>= fmb = StateT $ \s > runStateT ma s >>= \(s1, a) > runStateT (fmb a) s1
join ssa = StateT $ \s > runStateT ssa s >>= \(s, sa) > runStateT sa s
newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
deriving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)
```
This looks like it should be accepted. But I get
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180617 for x86_64appledarwin):
addTcEvBind NoEvBindsVar
[G] df_a67k
= \ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) >
coercible_sel
@ *
@ (m_a64Z[ssk:1] p_a62C)
@ (m_a64Z[ssk:1] q_a62D)
(df_a651 @ p_a62C @ q_a62D v_B1)
a67c
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"QuantifiedConstraints: panic \"addTcEvBind NoEvBindsVar\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:\r\n\r\n{{{#!hs\r\n{# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #}\r\n\r\nmodule Bug where\r\n\r\nimport Prelude hiding ( Monad(..) )\r\nimport Data.Coerce ( Coercible )\r\n\r\nclass Monad m where\r\n (>>=) :: m a > (a > m b) > m b\r\n join :: m (m a) > m a\r\n\r\nnewtype StateT s m a = StateT { runStateT :: s > m (s, a) }\r\n\r\ninstance Monad m => Monad (StateT s m) where\r\n ma >>= fmb = StateT $ \\s > runStateT ma s >>= \\(s1, a) > runStateT (fmb a) s1\r\n join ssa = StateT $ \\s > runStateT ssa s >>= \\(s, sa) > runStateT sa s\r\n\r\nnewtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }\r\n\r\nderiving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)\r\n\r\n}}}\r\n\r\nThis looks like it should be accepted. But I get\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180617 for x86_64appledarwin):\r\n\taddTcEvBind NoEvBindsVar\r\n [G] df_a67k\r\n = \\ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) >\r\n coercible_sel\r\n @ *\r\n @ (m_a64Z[ssk:1] p_a62C)\r\n @ (m_a64Z[ssk:1] q_a62D)\r\n (df_a651 @ p_a62C @ q_a62D v_B1)\r\n a67c\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:
```hs
{# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #}
module Bug where
import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible )
class Monad m where
(>>=) :: m a > (a > m b) > m b
join :: m (m a) > m a
newtype StateT s m a = StateT { runStateT :: s > m (s, a) }
instance Monad m => Monad (StateT s m) where
ma >>= fmb = StateT $ \s > runStateT ma s >>= \(s1, a) > runStateT (fmb a) s1
join ssa = StateT $ \s > runStateT ssa s >>= \(s, sa) > runStateT sa s
newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
deriving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)
```
This looks like it should be accepted. But I get
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180617 for x86_64appledarwin):
addTcEvBind NoEvBindsVar
[G] df_a67k
= \ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) >
coercible_sel
@ *
@ (m_a64Z[ssk:1] p_a62C)
@ (m_a64Z[ssk:1] q_a62D)
(df_a651 @ p_a62C @ q_a62D v_B1)
a67c
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"QuantifiedConstraints: panic \"addTcEvBind NoEvBindsVar\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I wanted to see if we're ready to put `join` into `Monad`. So I typed this in:\r\n\r\n{{{#!hs\r\n{# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #}\r\n\r\nmodule Bug where\r\n\r\nimport Prelude hiding ( Monad(..) )\r\nimport Data.Coerce ( Coercible )\r\n\r\nclass Monad m where\r\n (>>=) :: m a > (a > m b) > m b\r\n join :: m (m a) > m a\r\n\r\nnewtype StateT s m a = StateT { runStateT :: s > m (s, a) }\r\n\r\ninstance Monad m => Monad (StateT s m) where\r\n ma >>= fmb = StateT $ \\s > runStateT ma s >>= \\(s1, a) > runStateT (fmb a) s1\r\n join ssa = StateT $ \\s > runStateT ssa s >>= \\(s, sa) > runStateT sa s\r\n\r\nnewtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }\r\n\r\nderiving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)\r\n\r\n}}}\r\n\r\nThis looks like it should be accepted. But I get\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180617 for x86_64appledarwin):\r\n\taddTcEvBind NoEvBindsVar\r\n [G] df_a67k\r\n = \\ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) >\r\n coercible_sel\r\n @ *\r\n @ (m_a64Z[ssk:1] p_a62C)\r\n @ (m_a64Z[ssk:1] q_a62D)\r\n (df_a651 @ p_a62C @ q_a62D v_B1)\r\n a67c\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/17939Quantified constraint doesn't evidence type family instances20200329T23:36:37ZTom HardingQuantified constraint doesn't evidence type family instances## Summary
First up, sorry in advance: I'm unsure on the exact vocabulary for this particular problem.
In the below code, I would expect the `DC` constraint on `eg1` to imply the `CC` constraint required for `eg0` via the quantified constraint on `D`. However, it doesn't seem to be able to do so.
Interestingly, if I change the constraint on `eg0` to use the `Magic` class (which I created because of the recent restrictions on QC instance heads), everything seems to work happily.
Is this a case of GHC not searching hard enough for the `CC` instance? I'm certainly not an expert, but this behaviour feels bizarre to me; my intuition until now would have been to say that `CC f x` and `Magic f x` are equivalent in all circumstances!
## Steps to reproduce
```haskell
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
import Data.Kind (Constraint, Type)
class CC f x => Magic f x
instance CC f x => Magic f x
class C (f :: Type > Type) where
type CC f :: Type > Constraint
eg0 :: CC f x => f x > f x  Changing the constraint to `Magic f x => ...` works!
eg0 = id
class (C f, forall x. DC f x => Magic f x) => D (f :: Type > Type) where
type DC f :: Type > Constraint
eg1 :: (D f, DC f x) => f x > f x
eg1 = eg0
```
```
• Could not deduce: CC f x arising from a use of ‘eg0’
from the context: (D f, DC f x)
bound by the type signature for:
eg1 :: forall (f :: * > *) x. (D f, DC f x) => f x > f x
at Test.hs:23:134
• In the expression: eg0
In an equation for ‘eg1’: eg1 = eg0
• Relevant bindings include
eg1 :: f x > f x (bound at Test.hs:24:1)

24  eg1 = eg0
 ^^^
```
## Expected behavior
I would expect the aforementioned change to be a noop, though I suspect I'm missing some context!
## Environment
* GHC version used: 8.6.5, 8.8.1, 8.10## Summary
First up, sorry in advance: I'm unsure on the exact vocabulary for this particular problem.
In the below code, I would expect the `DC` constraint on `eg1` to imply the `CC` constraint required for `eg0` via the quantified constraint on `D`. However, it doesn't seem to be able to do so.
Interestingly, if I change the constraint on `eg0` to use the `Magic` class (which I created because of the recent restrictions on QC instance heads), everything seems to work happily.
Is this a case of GHC not searching hard enough for the `CC` instance? I'm certainly not an expert, but this behaviour feels bizarre to me; my intuition until now would have been to say that `CC f x` and `Magic f x` are equivalent in all circumstances!
## Steps to reproduce
```haskell
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
import Data.Kind (Constraint, Type)
class CC f x => Magic f x
instance CC f x => Magic f x
class C (f :: Type > Type) where
type CC f :: Type > Constraint
eg0 :: CC f x => f x > f x  Changing the constraint to `Magic f x => ...` works!
eg0 = id
class (C f, forall x. DC f x => Magic f x) => D (f :: Type > Type) where
type DC f :: Type > Constraint
eg1 :: (D f, DC f x) => f x > f x
eg1 = eg0
```
```
• Could not deduce: CC f x arising from a use of ‘eg0’
from the context: (D f, DC f x)
bound by the type signature for:
eg1 :: forall (f :: * > *) x. (D f, DC f x) => f x > f x
at Test.hs:23:134
• In the expression: eg0
In an equation for ‘eg1’: eg1 = eg0
• Relevant bindings include
eg1 :: f x > f x (bound at Test.hs:24:1)

24  eg1 = eg0
 ^^^
```
## Expected behavior
I would expect the aforementioned change to be a noop, though I suspect I'm missing some context!
## Environment
* GHC version used: 8.6.5, 8.8.1, 8.10https://gitlab.haskell.org/ghc/ghc//issues/17202GHC does not use quantified constraint from transitive superclass20200319T18:05:13ZAlexis KingGHC does not use quantified constraint from transitive superclass## Summary
GHC sometimes does not choose to use a quantified constraint made available by a superclass, and I am not sure why. The program typechecks if a type annotation is added to give the instance search a hint. Here’s a small program that reproduces the issue:
```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module Sandbox where
type family F a
class C1 a
class (forall c. C1 c) => C2 a
class (forall b. (b ~ F a) => C2 a) => C3 a
data Dict c = c => Dict
foo :: forall a. C3 a => Dict (C1 a)
foo = Dict
bar :: forall a. C3 a => Dict (C1 a)
bar = Dict :: C2 a => Dict (C1 a)
```
The definition of `foo` is rejected with the following error:
```
error:
• Could not deduce (C1 a) arising from a use of ‘Dict’
from the context: C3 a
bound by the type signature for:
foo :: forall a. C3 a => Dict (C1 a)
Possible fix:
add (C1 a) to the context of
the type signature for:
foo :: forall a. C3 a => Dict (C1 a)
• In the expression: Dict
In an equation for ‘foo’: foo = Dict
```
However, `bar` is accepted, as GHC successfully solves the `C2 a` constraint using the quantified superclass of `C3`, then proceeds to use the quantified superclass of `C2` to solve `C1 a`.
What’s especially strange to me about this program is that the problem goes away if either constraint is nonquantified *or* if the type family is removed from the context of `C3`’s superclass. The second of those two conditions makes it sound like maybe this is related to #15347, but I don’t think it is. That issue is about equalities in quantified heads, while this involves an equality in a quantified instance context, and equalities in instance contexts are entirely legal.
I think `foo` should typecheck, but if it can’t for some reason I don’t understand, I’d prefer it at least fail with a more helpful error message.
## Environment
* GHC version used: 8.8.1## Summary
GHC sometimes does not choose to use a quantified constraint made available by a superclass, and I am not sure why. The program typechecks if a type annotation is added to give the instance search a hint. Here’s a small program that reproduces the issue:
```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module Sandbox where
type family F a
class C1 a
class (forall c. C1 c) => C2 a
class (forall b. (b ~ F a) => C2 a) => C3 a
data Dict c = c => Dict
foo :: forall a. C3 a => Dict (C1 a)
foo = Dict
bar :: forall a. C3 a => Dict (C1 a)
bar = Dict :: C2 a => Dict (C1 a)
```
The definition of `foo` is rejected with the following error:
```
error:
• Could not deduce (C1 a) arising from a use of ‘Dict’
from the context: C3 a
bound by the type signature for:
foo :: forall a. C3 a => Dict (C1 a)
Possible fix:
add (C1 a) to the context of
the type signature for:
foo :: forall a. C3 a => Dict (C1 a)
• In the expression: Dict
In an equation for ‘foo’: foo = Dict
```
However, `bar` is accepted, as GHC successfully solves the `C2 a` constraint using the quantified superclass of `C3`, then proceeds to use the quantified superclass of `C2` to solve `C1 a`.
What’s especially strange to me about this program is that the problem goes away if either constraint is nonquantified *or* if the type family is removed from the context of `C3`’s superclass. The second of those two conditions makes it sound like maybe this is related to #15347, but I don’t think it is. That issue is about equalities in quantified heads, while this involves an equality in a quantified instance context, and equalities in instance contexts are entirely legal.
I think `foo` should typecheck, but if it can’t for some reason I don’t understand, I’d prefer it at least fail with a more helpful error message.
## Environment
* GHC version used: 8.8.1https://gitlab.haskell.org/ghc/ghc//issues/17794Quantified constraints leads to type errors when deriving default class methods20200319T18:02:03ZPatrick ThomsonQuantified constraints leads to type errors when deriving default class methods## Summary
When working with a GADT, ConstraintKinds, and QuantifiedConstraints, I can build a `Show` instance that fails to typecheck if any of the default methods (`showList` and `show` xor `showsPrec`) are missing. Copyandpasting these implementations from the typeclass’s definition makes them typecheck, so I think this is a bug in code generation.
## Steps to reproduce
Define
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
Then try to write a `Show` instance using `QuantifiedConstraints`:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
An error message is emitted about not being able to make a deduction when generating `$dmshow` and `$dmshowList`:
```
src/Data/Some.hs:45:10: error:
• Could not deduce: c (Some c)
arising from a use of ‘GHC.Show.$dmshow’
from the context: forall x. c x => Show x
bound by the instance declaration at src/Data/Some.hs:45:1052
• In the expression: GHC.Show.$dmshow @(Some c)
In an equation for ‘show’: show = GHC.Show.$dmshow @(Some c)
In the instance declaration for ‘Show (Some c)’
• Relevant bindings include
show :: Some c > String (bound at src/Data/Some.hs:45:10)

45  instance (forall x . c x => Show x) => Show (Some c) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
src/Data/Some.hs:45:10: error:
• Could not deduce: c (Some c)
arising from a use of ‘GHC.Show.$dmshowList’
from the context: forall x. c x => Show x
bound by the instance declaration at src/Data/Some.hs:45:1052
• In the expression: GHC.Show.$dmshowList @(Some c)
In an equation for ‘showList’:
showList = GHC.Show.$dmshowList @(Some c)
In the instance declaration for ‘Show (Some c)’
• Relevant bindings include
showList :: [Some c] > ShowS (bound at src/Data/Some.hs:45:10)

45  instance (forall x . c x => Show x) => Show (Some c) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
If you copypaste in a definition of `showList` and `show`, things will typecheck. Example:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show (Some a) = show a
showList ls s = showList__ shows' ls s
 Not sure why this is necessary: defining it inline produces another error
 about being unable to deduce c (Some c).
shows' :: (forall x . c x => Show x) => Some c > ShowS
shows' (Some x) = shows x
```
## Expected behavior
I expected the original definition (one expressed solely in terms of `showsPrec`) to typecheck.
## Environment
* GHC version used: 8.8.1
Optional:
* Operating System: macOS
* System Architecture: x86_64## Summary
When working with a GADT, ConstraintKinds, and QuantifiedConstraints, I can build a `Show` instance that fails to typecheck if any of the default methods (`showList` and `show` xor `showsPrec`) are missing. Copyandpasting these implementations from the typeclass’s definition makes them typecheck, so I think this is a bug in code generation.
## Steps to reproduce
Define
```haskell
data Some (c :: Type > Constraint) where
Some :: c a => a > Some c
```
Then try to write a `Show` instance using `QuantifiedConstraints`:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
An error message is emitted about not being able to make a deduction when generating `$dmshow` and `$dmshowList`:
```
src/Data/Some.hs:45:10: error:
• Could not deduce: c (Some c)
arising from a use of ‘GHC.Show.$dmshow’
from the context: forall x. c x => Show x
bound by the instance declaration at src/Data/Some.hs:45:1052
• In the expression: GHC.Show.$dmshow @(Some c)
In an equation for ‘show’: show = GHC.Show.$dmshow @(Some c)
In the instance declaration for ‘Show (Some c)’
• Relevant bindings include
show :: Some c > String (bound at src/Data/Some.hs:45:10)

45  instance (forall x . c x => Show x) => Show (Some c) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
src/Data/Some.hs:45:10: error:
• Could not deduce: c (Some c)
arising from a use of ‘GHC.Show.$dmshowList’
from the context: forall x. c x => Show x
bound by the instance declaration at src/Data/Some.hs:45:1052
• In the expression: GHC.Show.$dmshowList @(Some c)
In an equation for ‘showList’:
showList = GHC.Show.$dmshowList @(Some c)
In the instance declaration for ‘Show (Some c)’
• Relevant bindings include
showList :: [Some c] > ShowS (bound at src/Data/Some.hs:45:10)

45  instance (forall x . c x => Show x) => Show (Some c) where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
If you copypaste in a definition of `showList` and `show`, things will typecheck. Example:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show (Some a) = show a
showList ls s = showList__ shows' ls s
 Not sure why this is necessary: defining it inline produces another error
 about being unable to deduce c (Some c).
shows' :: (forall x . c x => Show x) => Some c > ShowS
shows' (Some x) = shows x
```
## Expected behavior
I expected the original definition (one expressed solely in terms of `showsPrec`) to typecheck.
## Environment
* GHC version used: 8.8.1
Optional:
* Operating System: macOS
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/15244Ambiguity checks in QuantifiedConstraints20200120T14:59:39ZbitwiseshiftleftAmbiguity checks in QuantifiedConstraintsGreat work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check.
```
{# LANGUAGE QuantifiedConstraints, TypeFamilies #}
class (forall t . Eq (c t)) => Blah c
 Unquantified works
foo :: (Eq (a t), Eq (b t), a ~ b) => a t > b t > Bool
foo a b = a == b
 Works
 Two quantified instances fail with double ambiguity check errors
bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool
bar a b = a == b
 Minimal.hs:11:8: error:
 • Could not deduce (Eq (b t1))
 from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),
 a ~ b)
 bound by the type signature for:
 bar :: forall (a :: * > *) (b :: * > *) t.
 (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>
 a t > b t > Bool
 at Minimal.hs:11:878
 • In the ambiguity check for ‘bar’
 To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
 In the type signature:
 bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>
 a t > b t > Bool
 
 11  bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool
 
 [And then another copy of the same error]
 Two copies from superclass instances fail
baz :: (Blah a, Blah b, a ~ b) => a t > b t > Bool
baz a b = a == b
 Minimal.hs:34:11: error:
 • Could not deduce (Eq (b t)) arising from a use of ‘==’
 from the context: (Blah a, Blah b, a ~ b)
 bound by the type signature for:
 baz :: forall (a :: * > *) (b :: * > *) t.
 (Blah a, Blah b, a ~ b) =>
 a t > b t > Bool
 at Minimal.hs:33:152
 • In the expression: a == b
 In an equation for ‘baz’: baz a b = a == b
 
 34  baz a b = a == b
 
 Two copies from superclass from same declaration also fail
mugga :: (Blah a, Blah a) => a t > a t > Bool
mugga a b = a == b
 • Could not deduce (Eq (a t)) arising from a use of ‘==’
 from the context: (Blah a, Blah a)
 bound by the type signature for:
 mugga :: forall (a :: * > *) t.
 (Blah a, Blah a) =>
 a t > a t > Bool
 at Minimal.hs:50:147
 • In the expression: a == b
 In an equation for ‘mugga’: mugga a b = a == b
 
 51  mugga a b = a == b
 
 One copy works
quux :: (Blah a, a ~ b) => a t > b t > Bool
quux a b = a == b
 Works
```
My program is similar to `Baz`. The constraints `Blah a` and `Blah b` are in scope from a pattern match, and I want to compare values of types `a t` and `b t` if they're the same type. So I get `a ~ b` from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes `(Blah a, Typeable a, Typeable b)`, so only one instance is in scope.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Ambiguity checks in QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Great work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check.\r\n\r\n{{{\r\n{# LANGUAGE QuantifiedConstraints, TypeFamilies #}\r\n\r\nclass (forall t . Eq (c t)) => Blah c\r\n\r\n Unquantified works\r\nfoo :: (Eq (a t), Eq (b t), a ~ b) => a t > b t > Bool\r\nfoo a b = a == b\r\n Works\r\n \r\n Two quantified instances fail with double ambiguity check errors\r\nbar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool\r\nbar a b = a == b\r\n Minimal.hs:11:8: error:\r\n • Could not deduce (Eq (b t1))\r\n from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),\r\n a ~ b)\r\n bound by the type signature for:\r\n bar :: forall (a :: * > *) (b :: * > *) t.\r\n (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>\r\n a t > b t > Bool\r\n at Minimal.hs:11:878\r\n • In the ambiguity check for ‘bar’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>\r\n a t > b t > Bool\r\n \r\n 11  bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool\r\n \r\n [And then another copy of the same error]\r\n\r\n Two copies from superclass instances fail\r\nbaz :: (Blah a, Blah b, a ~ b) => a t > b t > Bool\r\nbaz a b = a == b\r\n Minimal.hs:34:11: error:\r\n • Could not deduce (Eq (b t)) arising from a use of ‘==’\r\n from the context: (Blah a, Blah b, a ~ b)\r\n bound by the type signature for:\r\n baz :: forall (a :: * > *) (b :: * > *) t.\r\n (Blah a, Blah b, a ~ b) =>\r\n a t > b t > Bool\r\n at Minimal.hs:33:152\r\n • In the expression: a == b\r\n In an equation for ‘baz’: baz a b = a == b\r\n \r\n 34  baz a b = a == b\r\n  \r\n\r\n Two copies from superclass from same declaration also fail\r\nmugga :: (Blah a, Blah a) => a t > a t > Bool\r\nmugga a b = a == b\r\n • Could not deduce (Eq (a t)) arising from a use of ‘==’\r\n from the context: (Blah a, Blah a)\r\n bound by the type signature for:\r\n mugga :: forall (a :: * > *) t.\r\n (Blah a, Blah a) =>\r\n a t > a t > Bool\r\n at Minimal.hs:50:147\r\n • In the expression: a == b\r\n In an equation for ‘mugga’: mugga a b = a == b\r\n \r\n 51  mugga a b = a == b\r\n \r\n\r\n One copy works\r\nquux :: (Blah a, a ~ b) => a t > b t > Bool\r\nquux a b = a == b\r\n Works\r\n}}}\r\n\r\nMy program is similar to {{{Baz}}}. The constraints {{{Blah a}}} and {{{Blah b}}} are in scope from a pattern match, and I want to compare values of types {{{a t}}} and {{{b t}}} if they're the same type. So I get {{{a ~ b}}} from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes {{{(Blah a, Typeable a, Typeable b)}}}, so only one instance is in scope.","type_of_failure":"OtherFailure","blocking":[]} >Great work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check.
```
{# LANGUAGE QuantifiedConstraints, TypeFamilies #}
class (forall t . Eq (c t)) => Blah c
 Unquantified works
foo :: (Eq (a t), Eq (b t), a ~ b) => a t > b t > Bool
foo a b = a == b
 Works
 Two quantified instances fail with double ambiguity check errors
bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool
bar a b = a == b
 Minimal.hs:11:8: error:
 • Could not deduce (Eq (b t1))
 from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),
 a ~ b)
 bound by the type signature for:
 bar :: forall (a :: * > *) (b :: * > *) t.
 (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>
 a t > b t > Bool
 at Minimal.hs:11:878
 • In the ambiguity check for ‘bar’
 To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
 In the type signature:
 bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>
 a t > b t > Bool
 
 11  bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool
 
 [And then another copy of the same error]
 Two copies from superclass instances fail
baz :: (Blah a, Blah b, a ~ b) => a t > b t > Bool
baz a b = a == b
 Minimal.hs:34:11: error:
 • Could not deduce (Eq (b t)) arising from a use of ‘==’
 from the context: (Blah a, Blah b, a ~ b)
 bound by the type signature for:
 baz :: forall (a :: * > *) (b :: * > *) t.
 (Blah a, Blah b, a ~ b) =>
 a t > b t > Bool
 at Minimal.hs:33:152
 • In the expression: a == b
 In an equation for ‘baz’: baz a b = a == b
 
 34  baz a b = a == b
 
 Two copies from superclass from same declaration also fail
mugga :: (Blah a, Blah a) => a t > a t > Bool
mugga a b = a == b
 • Could not deduce (Eq (a t)) arising from a use of ‘==’
 from the context: (Blah a, Blah a)
 bound by the type signature for:
 mugga :: forall (a :: * > *) t.
 (Blah a, Blah a) =>
 a t > a t > Bool
 at Minimal.hs:50:147
 • In the expression: a == b
 In an equation for ‘mugga’: mugga a b = a == b
 
 51  mugga a b = a == b
 
 One copy works
quux :: (Blah a, a ~ b) => a t > b t > Bool
quux a b = a == b
 Works
```
My program is similar to `Baz`. The constraints `Blah a` and `Blah b` are in scope from a pattern match, and I want to compare values of types `a t` and `b t` if they're the same type. So I get `a ~ b` from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes `(Blah a, Typeable a, Typeable b)`, so only one instance is in scope.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Ambiguity checks in QuantifiedConstraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Great work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check.\r\n\r\n{{{\r\n{# LANGUAGE QuantifiedConstraints, TypeFamilies #}\r\n\r\nclass (forall t . Eq (c t)) => Blah c\r\n\r\n Unquantified works\r\nfoo :: (Eq (a t), Eq (b t), a ~ b) => a t > b t > Bool\r\nfoo a b = a == b\r\n Works\r\n \r\n Two quantified instances fail with double ambiguity check errors\r\nbar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool\r\nbar a b = a == b\r\n Minimal.hs:11:8: error:\r\n • Could not deduce (Eq (b t1))\r\n from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1),\r\n a ~ b)\r\n bound by the type signature for:\r\n bar :: forall (a :: * > *) (b :: * > *) t.\r\n (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) =>\r\n a t > b t > Bool\r\n at Minimal.hs:11:878\r\n • In the ambiguity check for ‘bar’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) =>\r\n a t > b t > Bool\r\n \r\n 11  bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t > b t > Bool\r\n \r\n [And then another copy of the same error]\r\n\r\n Two copies from superclass instances fail\r\nbaz :: (Blah a, Blah b, a ~ b) => a t > b t > Bool\r\nbaz a b = a == b\r\n Minimal.hs:34:11: error:\r\n • Could not deduce (Eq (b t)) arising from a use of ‘==’\r\n from the context: (Blah a, Blah b, a ~ b)\r\n bound by the type signature for:\r\n baz :: forall (a :: * > *) (b :: * > *) t.\r\n (Blah a, Blah b, a ~ b) =>\r\n a t > b t > Bool\r\n at Minimal.hs:33:152\r\n • In the expression: a == b\r\n In an equation for ‘baz’: baz a b = a == b\r\n \r\n 34  baz a b = a == b\r\n  \r\n\r\n Two copies from superclass from same declaration also fail\r\nmugga :: (Blah a, Blah a) => a t > a t > Bool\r\nmugga a b = a == b\r\n • Could not deduce (Eq (a t)) arising from a use of ‘==’\r\n from the context: (Blah a, Blah a)\r\n bound by the type signature for:\r\n mugga :: forall (a :: * > *) t.\r\n (Blah a, Blah a) =>\r\n a t > a t > Bool\r\n at Minimal.hs:50:147\r\n • In the expression: a == b\r\n In an equation for ‘mugga’: mugga a b = a == b\r\n \r\n 51  mugga a b = a == b\r\n \r\n\r\n One copy works\r\nquux :: (Blah a, a ~ b) => a t > b t > Bool\r\nquux a b = a == b\r\n Works\r\n}}}\r\n\r\nMy program is similar to {{{Baz}}}. The constraints {{{Blah a}}} and {{{Blah b}}} are in scope from a pattern match, and I want to compare values of types {{{a t}}} and {{{b t}}} if they're the same type. So I get {{{a ~ b}}} from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes {{{(Blah a, Typeable a, Typeable b)}}}, so only one instance is in scope.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/17267QuantifiedConstraints can prove anything with an infinite loop.20191223T14:23:41ZJames PayorQuantifiedConstraints can prove anything with an infinite loop.## Initial foothold: `a ~ b => a ~ b`
The following is with GHC `8.8.1`.
Issue #15316 considers a case of loopy `k => k` implications. The solution there was to reject functions like `f : (k => k) => (k => r) > r` on the grounds of `k => k` not looking like a decidable instance. GHC does now complain about those, but the problem remains.
Consider this example:
```haskell
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}  for equational constraints
unsafeCoerce :: a > b
unsafeCoerce = oops where
oops :: (a ~ b => a ~ b) => a > b
oops a = a
main :: IO ()
main = unsafeCoerce "Hello!"
```
The checks to avoid loopiness aren't firing, and it compiles.
The example above at runtime outputs `Oops: <<loop>>`. However, I can modify it so that the compiler erases the infinite loop, to get a true `unsafeCoerce`:
```haskell
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
class a ~ b => Thing a b
instance a ~ b => Thing a b
unsafeCoerce :: forall a b. a > b
unsafeCoerce a = oops a where
oops :: (a ~ b => Thing a b) => (Thing a b => r) > r
oops r = r
main :: IO ()
main = unsafeCoerce "Hello!"
```
Compiling with `O0` gives:
```
[1 of 1] Compiling Main ( Oops.hs, Oops.o ) [Optimisation flags changed]
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64appledarwin):
primRepCmmType:VoidRep
```
...and with `O2` the program crashes at runtime:
```
[1 of 1] Compiling Main ( Oops.hs, Oops.o )
Linking Oops ...
Oops: internal error: stg_ap_v_ret
(GHC version 8.8.1 for x86_64_apple_darwin)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
fish: './Oops' terminated by signal SIGABRT (Abort)
```
## More generally: sidestepping the decidability checker, inhabiting any constraint with `<<loop>>`
Here's a simple example for getting a `Show (IO ())` "instance", which will just be a loop.
```
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FlexibleInstances #}
class Show a => Thing a b
instance Show a => Thing a b
pseudoShow :: (Show a => Thing a ()) => a > String
pseudoShow = show
main :: IO ()
main = putStrLn $ pseudoShow main
```
## My take on what's going on
If you just try to use `Show a => Show a` or `Show a => Thing a`, GHC will complain and demand `UndecidableInstances`. But this is easy to sidestep, if one just has `Show a => Thing a b`, because `Thing a b` is a bigger instance head...
Even if you only ever add smaller and smaller instance heads to your wanteds, the problem is that you started off by saying "I need `Show a`, and fortunately that's a superclass of `Thing a ()`  so all I need is to provide a `Show a` instance". And rapidly you have a loop.## Initial foothold: `a ~ b => a ~ b`
The following is with GHC `8.8.1`.
Issue #15316 considers a case of loopy `k => k` implications. The solution there was to reject functions like `f : (k => k) => (k => r) > r` on the grounds of `k => k` not looking like a decidable instance. GHC does now complain about those, but the problem remains.
Consider this example:
```haskell
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}  for equational constraints
unsafeCoerce :: a > b
unsafeCoerce = oops where
oops :: (a ~ b => a ~ b) => a > b
oops a = a
main :: IO ()
main = unsafeCoerce "Hello!"
```
The checks to avoid loopiness aren't firing, and it compiles.
The example above at runtime outputs `Oops: <<loop>>`. However, I can modify it so that the compiler erases the infinite loop, to get a true `unsafeCoerce`:
```haskell
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
class a ~ b => Thing a b
instance a ~ b => Thing a b
unsafeCoerce :: forall a b. a > b
unsafeCoerce a = oops a where
oops :: (a ~ b => Thing a b) => (Thing a b => r) > r
oops r = r
main :: IO ()
main = unsafeCoerce "Hello!"
```
Compiling with `O0` gives:
```
[1 of 1] Compiling Main ( Oops.hs, Oops.o ) [Optimisation flags changed]
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64appledarwin):
primRepCmmType:VoidRep
```
...and with `O2` the program crashes at runtime:
```
[1 of 1] Compiling Main ( Oops.hs, Oops.o )
Linking Oops ...
Oops: internal error: stg_ap_v_ret
(GHC version 8.8.1 for x86_64_apple_darwin)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
fish: './Oops' terminated by signal SIGABRT (Abort)
```
## More generally: sidestepping the decidability checker, inhabiting any constraint with `<<loop>>`
Here's a simple example for getting a `Show (IO ())` "instance", which will just be a loop.
```
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE FlexibleInstances #}
class Show a => Thing a b
instance Show a => Thing a b
pseudoShow :: (Show a => Thing a ()) => a > String
pseudoShow = show
main :: IO ()
main = putStrLn $ pseudoShow main
```
## My take on what's going on
If you just try to use `Show a => Show a` or `Show a => Thing a`, GHC will complain and demand `UndecidableInstances`. But this is easy to sidestep, if one just has `Show a => Thing a b`, because `Thing a b` is a bigger instance head...
Even if you only ever add smaller and smaller instance heads to your wanteds, the problem is that you started off by saying "I need `Show a`, and fortunately that's a superclass of `Thing a ()`  so all I need is to provide a `Show a` instance". And rapidly you have a loop.8.10.1https://gitlab.haskell.org/ghc/ghc//issues/17458Runtime loop when using eqT20191113T21:59:02ZMax HarmsRuntime loop when using eqT## Summary
Use of eqT causes runtime divergence in a weird edgecase.
## Steps to reproduce
This example is minimized for simplicity; my actual use case was large and it took me 5 hours to get it down to this:
```haskell
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE TypeOperators #}
import Data.Void
import Data.Typeable
import Data.Type.Equality
class (forall k. k a => k b) => Equ a b
instance Equ a a
data Z' a where
Z' :: Z' Void
data Z where
Z :: forall a. Equ Void a => Z' a > Z
checkZ :: Z > Bool
checkZ (Z (Z' :: Z' a)) = case eqT of
Nothing > False
Just (Refl :: a :~: Void) > True
main :: IO ()
main = do
putStrLn "before..."
print $ checkZ $ Z Z'
putStrLn "after!"
```
Compiles ok. Exe output is:
```
before...
MinExample: <<loop>>
```
## Expected behavior
This should work and produce
```
before...
True
after...
```
Poking around indicates that Eq can propagate along the quantified constraint of `Equ`, but apparently something magic is happening with Typeable?
## Environment
Tested with GHC 8.6 and 8.8 on NixOS.## Summary
Use of eqT causes runtime divergence in a weird edgecase.
## Steps to reproduce
This example is minimized for simplicity; my actual use case was large and it took me 5 hours to get it down to this:
```haskell
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE TypeOperators #}
import Data.Void
import Data.Typeable
import Data.Type.Equality
class (forall k. k a => k b) => Equ a b
instance Equ a a
data Z' a where
Z' :: Z' Void
data Z where
Z :: forall a. Equ Void a => Z' a > Z
checkZ :: Z > Bool
checkZ (Z (Z' :: Z' a)) = case eqT of
Nothing > False
Just (Refl :: a :~: Void) > True
main :: IO ()
main = do
putStrLn "before..."
print $ checkZ $ Z Z'
putStrLn "after!"
```
Compiles ok. Exe output is:
```
before...
MinExample: <<loop>>
```
## Expected behavior
This should work and produce
```
before...
True
after...
```
Poking around indicates that Eq can propagate along the quantified constraint of `Equ`, but apparently something magic is happening with Typeable?
## Environment
Tested with GHC 8.6 and 8.8 on NixOS.https://gitlab.haskell.org/ghc/ghc//issues/17427Weird interaction between QuantifiedConstraints and TypeFamilies20191102T12:35:46ZDarwin226Weird interaction between QuantifiedConstraints and TypeFamilies## Summary
The title is kind of bad. The gist of the issue is that deducing `Constr X` from `forall a. Constr a` doesn't work if `Constr` is a result of a type family evaluation.
## Steps to reproduce
Here's an example
```haskell
data Dict c where
Dict :: c => Dict c
class Class (a :: Type)
type family Class' where
Class' = Class
test :: (forall a. Class' a) => Dict (Class' Int)
test = Dict
```
## Expected behavior
Since `test` does typecheck if I replace `Class'` with `Class`, I expected it to typecheck the way it's written as well. Instead I get
```haskell
Could not deduce (Class Int) arising from a use of ‘Dict’ from the context:
forall a. Class' a
bound by the type signature for:
test :: (forall a. Class' a) => Dict (Class' Int)
```
## Environment
* GHC version used: 8.6.4
Optional:
* Operating System: Windows
* System Architecture: x64## Summary
The title is kind of bad. The gist of the issue is that deducing `Constr X` from `forall a. Constr a` doesn't work if `Constr` is a result of a type family evaluation.
## Steps to reproduce
Here's an example
```haskell
data Dict c where
Dict :: c => Dict c
class Class (a :: Type)
type family Class' where
Class' = Class
test :: (forall a. Class' a) => Dict (Class' Int)
test = Dict
```
## Expected behavior
Since `test` does typecheck if I replace `Class'` with `Class`, I expected it to typecheck the way it's written as well. Instead I get
```haskell
Could not deduce (Class Int) arising from a use of ‘Dict’ from the context:
forall a. Class' a
bound by the type signature for:
test :: (forall a. Class' a) => Dict (Class' Int)
```
## Environment
* GHC version used: 8.6.4
Optional:
* Operating System: Windows
* System Architecture: x64https://gitlab.haskell.org/ghc/ghc//issues/14943Make (=>) polykinded (:: k > k > Constraint)20191018T18:43:28ZIcelandjackMake (=>) polykinded (:: k > k > Constraint)Would it be a good idea to treat `=>` in `XQuantifiedConstraints` as
```hs
type family
(=>) :: k > k > Constraint where
(=>) = Implies0
(=>) = Implies1
(=>) = Implies2 ..
```
```hs
class (a => b) => Implies a b
instance (a => b) => Implies a b
class (forall x. f x => g x) => Implies1 f g
instance (forall x. f x => g x) => Implies1 f g
class (forall x y. f x y => g x y) => Implies2 f g
instance (forall x y. f x y => g x y) => Implies2 f g
..
```
or will this get too confusing? This means type signatures like the ones from #14942
```hs
oneTwo :: (forall x. semi x => Semigroup x) => Free semi Int
nil :: (forall x. mon x => Monoid x) => Free mon Int
together :: (forall x. mon x => Monoid x) => [Free mon Int]
```
could equivalently be written
```hs
oneTwo :: (semi => Semigroup) => Free semi Int
nil :: (mon => Monoid) => Free mon Int
together :: (mon => Monoid) => [Free mon Int]
```
I'm not sold on this idea myself. It's quite possible this would screw with the parser.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"Make (=>) polykinded (:: k > k > Constraint)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Would it be a good idea to treat `=>` in `XQuantifiedConstraints` as\r\n\r\n{{{#!hs\r\ntype family\r\n (=>) :: k > k > Constraint where\r\n (=>) = Implies0\r\n (=>) = Implies1\r\n (=>) = Implies2 ..\r\n}}}\r\n\r\n{{{#!hs\r\nclass (a => b) => Implies a b\r\ninstance (a => b) => Implies a b\r\n\r\nclass (forall x. f x => g x) => Implies1 f g\r\ninstance (forall x. f x => g x) => Implies1 f g\r\n\r\nclass (forall x y. f x y => g x y) => Implies2 f g\r\ninstance (forall x y. f x y => g x y) => Implies2 f g\r\n..\r\n}}}\r\n\r\nor will this get too confusing? This means type signatures like the ones from #14942\r\n\r\n{{{#!hs\r\noneTwo :: (forall x. semi x => Semigroup x) => Free semi Int\r\n\r\nnil :: (forall x. mon x => Monoid x) => Free mon Int\r\n\r\ntogether :: (forall x. mon x => Monoid x) => [Free mon Int]\r\n}}}\r\n\r\ncould equivalently be written\r\n\r\n{{{#!hs\r\noneTwo :: (semi => Semigroup) => Free semi Int\r\n\r\nnil :: (mon => Monoid) => Free mon Int\r\n\r\ntogether :: (mon => Monoid) => [Free mon Int]\r\n}}}\r\n\r\nI'm not sold on this idea myself. It's quite possible this would screw with the parser.","type_of_failure":"OtherFailure","blocking":[]} >Would it be a good idea to treat `=>` in `XQuantifiedConstraints` as
```hs
type family
(=>) :: k > k > Constraint where
(=>) = Implies0
(=>) = Implies1
(=>) = Implies2 ..
```
```hs
class (a => b) => Implies a b
instance (a => b) => Implies a b
class (forall x. f x => g x) => Implies1 f g
instance (forall x. f x => g x) => Implies1 f g
class (forall x y. f x y => g x y) => Implies2 f g
instance (forall x y. f x y => g x y) => Implies2 f g
..
```
or will this get too confusing? This means type signatures like the ones from #14942
```hs
oneTwo :: (forall x. semi x => Semigroup x) => Free semi Int
nil :: (forall x. mon x => Monoid x) => Free mon Int
together :: (forall x. mon x => Monoid x) => [Free mon Int]
```
could equivalently be written
```hs
oneTwo :: (semi => Semigroup) => Free semi Int
nil :: (mon => Monoid) => Free mon Int
together :: (mon => Monoid) => [Free mon Int]
```
I'm not sold on this idea myself. It's quite possible this would screw with the parser.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"Make (=>) polykinded (:: k > k > Constraint)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["QuantifiedConstraints,","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Would it be a good idea to treat `=>` in `XQuantifiedConstraints` as\r\n\r\n{{{#!hs\r\ntype family\r\n (=>) :: k > k > Constraint where\r\n (=>) = Implies0\r\n (=>) = Implies1\r\n (=>) = Implies2 ..\r\n}}}\r\n\r\n{{{#!hs\r\nclass (a => b) => Implies a b\r\ninstance (a => b) => Implies a b\r\n\r\nclass (forall x. f x => g x) => Implies1 f g\r\ninstance (forall x. f x => g x) => Implies1 f g\r\n\r\nclass (forall x y. f x y => g x y) => Implies2 f g\r\ninstance (forall x y. f x y => g x y) => Implies2 f g\r\n..\r\n}}}\r\n\r\nor will this get too confusing? This means type signatures like the ones from #14942\r\n\r\n{{{#!hs\r\noneTwo :: (forall x. semi x => Semigroup x) => Free semi Int\r\n\r\nnil :: (forall x. mon x => Monoid x) => Free mon Int\r\n\r\ntogether :: (forall x. mon x => Monoid x) => [Free mon Int]\r\n}}}\r\n\r\ncould equivalently be written\r\n\r\n{{{#!hs\r\noneTwo :: (semi => Semigroup) => Free semi Int\r\n\r\nnil :: (mon => Monoid) => Free mon Int\r\n\r\ntogether :: (mon => Monoid) => [Free mon Int]\r\n}}}\r\n\r\nI'm not sold on this idea myself. It's quite possible this would screw with the parser.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/17025Undecidable quantified superclass constraints aren’t rejected by the decidabi...20190902T21:21:26ZAlexis KingUndecidable quantified superclass constraints aren’t rejected by the decidability checker## Summary
This small (albeit somewhat nonsensical) program using `QuantifiedConstraints` causes the constraint solver to diverge:
```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module QC where
class (forall c. C (F f c) c) => C f b where
type F f c :: * > *
f :: (c > b) > F f c a > f a
bar :: C f String => f ()
bar = f show undefined
```
```
src/QC.hs:1:1: error:
solveWanteds: too many iterations (limit = 100)
Unsolved: WC {wc_simple =
[WD] $dShow_a2mS {0}:: Show a0 (CDictCan)
[WD] $dIP_a3xb {0}:: ?callStack::GHC.Stack.Types.CallStack (CDictCan)}
Set limit with fconstraintsolveriterations=n; n=0 for no limit

1  {# LANGUAGE FlexibleContexts #}
 ^
src/QC.hs:13:9: error:
• Could not deduce (Show a0) arising from a use of ‘show’
from the context: C f String
bound by the type signature for:
bar :: forall (f :: * > *). C f String => f ()
at src/QC.hs:12:125
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance Show Ordering  Defined in ‘GHC.Show’
instance Show Integer  Defined in ‘GHC.Show’
instance Show a => Show (Maybe a)  Defined in ‘GHC.Show’
...plus 22 others
...plus 27 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• In the first argument of ‘f’, namely ‘show’
In the expression: f show undefined
In an equation for ‘bar’: bar = f show undefined

13  bar = f show undefined
 ^^^^
```
The above program is silly, and the reported error (that the `Show` instance is ambiguous) is ultimately still correct, so who cares, right? But I actually have a slightly larger example that fails with the same error, even though I believe it is actually welltyped:
```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module QCFunDep where
class (Applicative f, forall c. C (F f c) c) => C f b  f > b where
type F f c :: * > *
f :: (c > b) > F f c a > f a
foo :: C f Integer => f ()
foo = pure ()
bar :: C f String => f ()
bar = f show foo
```
I think the second program might fail to typecheck because of #15351, so that issue might not be new. Either way, it seems like the solver diverging is something that shouldn’t happen, so this report is really about that.
## Environment
* GHC version used: 8.6.5
* Operating System: macOS 10.14.5 (18F132)
* System Architecture: x86_64## Summary
This small (albeit somewhat nonsensical) program using `QuantifiedConstraints` causes the constraint solver to diverge:
```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module QC where
class (forall c. C (F f c) c) => C f b where
type F f c :: * > *
f :: (c > b) > F f c a > f a
bar :: C f String => f ()
bar = f show undefined
```
```
src/QC.hs:1:1: error:
solveWanteds: too many iterations (limit = 100)
Unsolved: WC {wc_simple =
[WD] $dShow_a2mS {0}:: Show a0 (CDictCan)
[WD] $dIP_a3xb {0}:: ?callStack::GHC.Stack.Types.CallStack (CDictCan)}
Set limit with fconstraintsolveriterations=n; n=0 for no limit

1  {# LANGUAGE FlexibleContexts #}
 ^
src/QC.hs:13:9: error:
• Could not deduce (Show a0) arising from a use of ‘show’
from the context: C f String
bound by the type signature for:
bar :: forall (f :: * > *). C f String => f ()
at src/QC.hs:12:125
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance Show Ordering  Defined in ‘GHC.Show’
instance Show Integer  Defined in ‘GHC.Show’
instance Show a => Show (Maybe a)  Defined in ‘GHC.Show’
...plus 22 others
...plus 27 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• In the first argument of ‘f’, namely ‘show’
In the expression: f show undefined
In an equation for ‘bar’: bar = f show undefined

13  bar = f show undefined
 ^^^^
```
The above program is silly, and the reported error (that the `Show` instance is ambiguous) is ultimately still correct, so who cares, right? But I actually have a slightly larger example that fails with the same error, even though I believe it is actually welltyped:
```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
module QCFunDep where
class (Applicative f, forall c. C (F f c) c) => C f b  f > b where
type F f c :: * > *
f :: (c > b) > F f c a > f a
foo :: C f Integer => f ()
foo = pure ()
bar :: C f String => f ()
bar = f show foo
```
I think the second program might fail to typecheck because of #15351, so that issue might not be new. Either way, it seems like the solver diverging is something that shouldn’t happen, so this report is really about that.
## Environment
* GHC version used: 8.6.5
* Operating System: macOS 10.14.5 (18F132)
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/15334(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)20190805T08:46:55ZRyan Scott(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)Consider the following code:
```hs
{# LANGUAGE DeriveTraversable #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE UndecidableInstances #}
module Foo where
import Data.Kind
type family F a :: Type > Type
newtype WrappedF a b = WrapF (F a b)
deriving instance Functor (F a) => Functor (WrappedF a)
deriving instance Foldable (F a) => Foldable (WrappedF a)
deriving instance Traversable (F a) => Traversable (WrappedF a)
data SomeF b = forall a. MkSomeF (WrappedF a b)
deriving instance (forall a. Functor (WrappedF a)) => Functor SomeF
deriving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF
deriving instance ( forall a. Functor (WrappedF a)
, forall a. Foldable (WrappedF a)
, forall a. Traversable (WrappedF a)
) => Traversable SomeF
```
This typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:
```hs
deriving instance (forall a. ( Functor (WrappedF a)
, Foldable (WrappedF a)
, Traversable (WrappedF a)
)) => Traversable SomeF
```
But then the file no longer typechecked!
```
$ /opt/ghc/8.6.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:21:1: error:
• Could not deduce (Functor (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Foldable (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Traversable (F a1))
arising from a use of ‘traverse’
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
or from: Applicative f
bound by the type signature for:
traverse :: forall (f :: * > *) a b.
Applicative f =>
(a > f b) > SomeF a > f (SomeF b)
at Foo.hs:(21,1)(24,52)
• In the second argument of ‘fmap’, namely ‘(traverse f a1)’
In the expression: fmap (\ b1 > MkSomeF b1) (traverse f a1)
In an equation for ‘traverse’:
traverse f (MkSomeF a1) = fmap (\ b1 > MkSomeF b1) (traverse f a1)
When typechecking the code for ‘traverse’
in a derived instance for ‘Traversable SomeF’:
To see the code I am typechecking, use ddumpderiv

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
Richard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.
<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":"(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveTraversable #}\r\n{# LANGUAGE ExistentialQuantification #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family F a :: Type > Type\r\nnewtype WrappedF a b = WrapF (F a b)\r\nderiving instance Functor (F a) => Functor (WrappedF a)\r\nderiving instance Foldable (F a) => Foldable (WrappedF a)\r\nderiving instance Traversable (F a) => Traversable (WrappedF a)\r\n\r\ndata SomeF b = forall a. MkSomeF (WrappedF a b)\r\n\r\nderiving instance (forall a. Functor (WrappedF a)) => Functor SomeF\r\nderiving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF\r\nderiving instance ( forall a. Functor (WrappedF a)\r\n , forall a. Foldable (WrappedF a)\r\n , forall a. Traversable (WrappedF a)\r\n ) => Traversable SomeF\r\n}}}\r\n\r\nThis typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:\r\n\r\n{{{#!hs\r\nderiving instance (forall a. ( Functor (WrappedF a)\r\n , Foldable (WrappedF a)\r\n , Traversable (WrappedF a)\r\n )) => Traversable SomeF\r\n}}}\r\n\r\nBut then the file no longer typechecked!\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Foo.hs\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Functor (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Foldable (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Traversable (F a1))\r\n arising from a use of ‘traverse’\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n or from: Applicative f\r\n bound by the type signature for:\r\n traverse :: forall (f :: * > *) a b.\r\n Applicative f =>\r\n (a > f b) > SomeF a > f (SomeF b)\r\n at Foo.hs:(21,1)(24,52)\r\n • In the second argument of ‘fmap’, namely ‘(traverse f a1)’\r\n In the expression: fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n In an equation for ‘traverse’:\r\n traverse f (MkSomeF a1) = fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n When typechecking the code for ‘traverse’\r\n in a derived instance for ‘Traversable SomeF’:\r\n To see the code I am typechecking, use ddumpderiv\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nRichard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following code:
```hs
{# LANGUAGE DeriveTraversable #}
{# LANGUAGE ExistentialQuantification #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE UndecidableInstances #}
module Foo where
import Data.Kind
type family F a :: Type > Type
newtype WrappedF a b = WrapF (F a b)
deriving instance Functor (F a) => Functor (WrappedF a)
deriving instance Foldable (F a) => Foldable (WrappedF a)
deriving instance Traversable (F a) => Traversable (WrappedF a)
data SomeF b = forall a. MkSomeF (WrappedF a b)
deriving instance (forall a. Functor (WrappedF a)) => Functor SomeF
deriving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF
deriving instance ( forall a. Functor (WrappedF a)
, forall a. Foldable (WrappedF a)
, forall a. Traversable (WrappedF a)
) => Traversable SomeF
```
This typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:
```hs
deriving instance (forall a. ( Functor (WrappedF a)
, Foldable (WrappedF a)
, Traversable (WrappedF a)
)) => Traversable SomeF
```
But then the file no longer typechecked!
```
$ /opt/ghc/8.6.1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:21:1: error:
• Could not deduce (Functor (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Foldable (F a))
arising from the superclasses of an instance declaration
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
• In the instance declaration for ‘Traversable SomeF’

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:21:1: error:
• Could not deduce (Traversable (F a1))
arising from a use of ‘traverse’
from the context: forall a.
(Functor (WrappedF a), Foldable (WrappedF a),
Traversable (WrappedF a))
bound by the instance declaration at Foo.hs:(21,1)(24,52)
or from: Applicative f
bound by the type signature for:
traverse :: forall (f :: * > *) a b.
Applicative f =>
(a > f b) > SomeF a > f (SomeF b)
at Foo.hs:(21,1)(24,52)
• In the second argument of ‘fmap’, namely ‘(traverse f a1)’
In the expression: fmap (\ b1 > MkSomeF b1) (traverse f a1)
In an equation for ‘traverse’:
traverse f (MkSomeF a1) = fmap (\ b1 > MkSomeF b1) (traverse f a1)
When typechecking the code for ‘traverse’
in a derived instance for ‘Traversable SomeF’:
To see the code I am typechecking, use ddumpderiv

21  deriving instance (forall a. ( Functor (WrappedF a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
Richard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.
<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":"(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DeriveTraversable #}\r\n{# LANGUAGE ExistentialQuantification #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype family F a :: Type > Type\r\nnewtype WrappedF a b = WrapF (F a b)\r\nderiving instance Functor (F a) => Functor (WrappedF a)\r\nderiving instance Foldable (F a) => Foldable (WrappedF a)\r\nderiving instance Traversable (F a) => Traversable (WrappedF a)\r\n\r\ndata SomeF b = forall a. MkSomeF (WrappedF a b)\r\n\r\nderiving instance (forall a. Functor (WrappedF a)) => Functor SomeF\r\nderiving instance (forall a. Foldable (WrappedF a)) => Foldable SomeF\r\nderiving instance ( forall a. Functor (WrappedF a)\r\n , forall a. Foldable (WrappedF a)\r\n , forall a. Traversable (WrappedF a)\r\n ) => Traversable SomeF\r\n}}}\r\n\r\nThis typechecks. However, the last `Traversable SomeF` is a bit unfortunate in that is uses three separate `forall a.`s. I attempted to factor this out, like so:\r\n\r\n{{{#!hs\r\nderiving instance (forall a. ( Functor (WrappedF a)\r\n , Foldable (WrappedF a)\r\n , Traversable (WrappedF a)\r\n )) => Traversable SomeF\r\n}}}\r\n\r\nBut then the file no longer typechecked!\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Foo.hs\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Functor (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Foldable (F a))\r\n arising from the superclasses of an instance declaration\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n • In the instance declaration for ‘Traversable SomeF’\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:21:1: error:\r\n • Could not deduce (Traversable (F a1))\r\n arising from a use of ‘traverse’\r\n from the context: forall a.\r\n (Functor (WrappedF a), Foldable (WrappedF a),\r\n Traversable (WrappedF a))\r\n bound by the instance declaration at Foo.hs:(21,1)(24,52)\r\n or from: Applicative f\r\n bound by the type signature for:\r\n traverse :: forall (f :: * > *) a b.\r\n Applicative f =>\r\n (a > f b) > SomeF a > f (SomeF b)\r\n at Foo.hs:(21,1)(24,52)\r\n • In the second argument of ‘fmap’, namely ‘(traverse f a1)’\r\n In the expression: fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n In an equation for ‘traverse’:\r\n traverse f (MkSomeF a1) = fmap (\\ b1 > MkSomeF b1) (traverse f a1)\r\n When typechecking the code for ‘traverse’\r\n in a derived instance for ‘Traversable SomeF’:\r\n To see the code I am typechecking, use ddumpderiv\r\n \r\n21  deriving instance (forall a. ( Functor (WrappedF a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nRichard suspects that this is a bug in the way quantified constraints expands superclasses, so I decided to post it here.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15359Quantified constraints do not work with equality constraints20190707T18:13:01ZRichard Eisenbergrae@richarde.devQuantified constraints do not work with equality constraintsFeeling abusive toward GHC this morning, I tried this:
```hs
class C a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
foo Dict x = x
```
I thought it wouldn't work, and I was right:
```
• Class ‘~’ does not support userspecified instances
• In the quantified constraint ‘forall (a :: k) (b :: k).
C a b =>
a ~ b’
In the type signature:
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
```
Good. But then I tried something more devious:
```hs
class C a b
class a ~ b => D a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b
foo Dict x = x
```
This also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.
I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Quantified constraints do not work with equality constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Feeling abusive toward GHC this morning, I tried this:\r\n\r\n{{{#!hs\r\nclass C a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nI thought it wouldn't work, and I was right:\r\n\r\n{{{\r\n • Class ‘~’ does not support userspecified instances\r\n • In the quantified constraint ‘forall (a :: k) (b :: k).\r\n C a b =>\r\n a ~ b’\r\n In the type signature:\r\n foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\n}}}\r\n\r\nGood. But then I tried something more devious:\r\n\r\n{{{#!hs\r\nclass C a b\r\nclass a ~ b => D a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nThis also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.\r\n\r\nI'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.","type_of_failure":"OtherFailure","blocking":[]} >Feeling abusive toward GHC this morning, I tried this:
```hs
class C a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
foo Dict x = x
```
I thought it wouldn't work, and I was right:
```
• Class ‘~’ does not support userspecified instances
• In the quantified constraint ‘forall (a :: k) (b :: k).
C a b =>
a ~ b’
In the type signature:
foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b
```
Good. But then I tried something more devious:
```hs
class C a b
class a ~ b => D a b
data Dict c where
Dict :: c => Dict c
foo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b
foo Dict x = x
```
This also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.
I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Quantified constraints do not work with equality constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Feeling abusive toward GHC this morning, I tried this:\r\n\r\n{{{#!hs\r\nclass C a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nI thought it wouldn't work, and I was right:\r\n\r\n{{{\r\n • Class ‘~’ does not support userspecified instances\r\n • In the quantified constraint ‘forall (a :: k) (b :: k).\r\n C a b =>\r\n a ~ b’\r\n In the type signature:\r\n foo :: (forall a b. C a b => a ~ b) => Dict (C a b) > a > b\r\n}}}\r\n\r\nGood. But then I tried something more devious:\r\n\r\n{{{#!hs\r\nclass C a b\r\nclass a ~ b => D a b\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nfoo :: (forall a b. C a b => D a b) => Dict (C a b) > a > b\r\nfoo Dict x = x\r\n}}}\r\n\r\nThis also fails, with ` Couldn't match expected type ‘b’ with actual type ‘a’`.\r\n\r\nI'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason  like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15507Deriving with QuantifiedConstraints is unable to penetrate type families20190707T18:04:26ZisovectorDeriving with QuantifiedConstraints is unable to penetrate type familiesI'd expect the following code to successfully derive a usable `Eq` instance for `Foo`.
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module QuantifiedConstraints where
import Data.Functor.Identity
type family HKD f a where
HKD Identity a = a
HKD f a = f a
data Foo f = Foo
{ zoo :: HKD f Int
, zum :: HKD f Bool
}
deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
```
However, it complains:
```
• Could not deduce (Eq (HKD f a))
from the context: forall a. Eq a => Eq (HKD f a)
bound by an instance declaration:
forall (f :: * > *).
(forall a. Eq a => Eq (HKD f a)) =>
Eq (Foo f)
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:20:1964
or from: Eq a
bound by a quantified context
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:20:1964
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the standalone deriving instance for
‘(forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)’
```
Adding XAllowAmbiguousTypes doesn't fix the situation:
```
• Could not deduce (Eq (HKD f Int)) arising from a use of ‘==’
from the context: forall a. Eq a => Eq (HKD f a)
bound by the instance declaration
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:21:164
• In the first argument of ‘(&&)’, namely ‘((a1 == b1))’
In the expression: (((a1 == b1)) && ((a2 == b2)))
In an equation for ‘==’:
(==) (Foo a1 a2) (Foo b1 b2) = (((a1 == b1)) && ((a2 == b2)))
When typechecking the code for ‘==’
in a derived instance for ‘Eq (Foo f)’:
To see the code I am typechecking, use ddumpderiv

21  deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:21:1: error:
• Could not deduce (Eq (HKD f a))
arising from a use of ‘GHC.Classes.$dm/=’
from the context: forall a. Eq a => Eq (HKD f a)
bound by the instance declaration
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:21:164
or from: Eq a
bound by a quantified context
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:1:1
• In the expression: GHC.Classes.$dm/= @(Foo f)
In an equation for ‘/=’: (/=) = GHC.Classes.$dm/= @(Foo f)
When typechecking the code for ‘/=’
in a derived instance for ‘Eq (Foo f)’:
To see the code I am typechecking, use ddumpderiv
In the instance declaration for ‘Eq (Foo f)’

21  deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
and the result of ddumpderiv:
```
==================== Derived instances ====================
Derived class instances:
instance (forall a.
GHC.Classes.Eq a =>
GHC.Classes.Eq (QuantifiedConstraints.HKD f a)) =>
GHC.Classes.Eq (QuantifiedConstraints.Foo f) where
(GHC.Classes.==)
(QuantifiedConstraints.Foo a1_a74s a2_a74t)
(QuantifiedConstraints.Foo b1_a74u b2_a74v)
= (((a1_a74s GHC.Classes.== b1_a74u))
GHC.Classes.&& ((a2_a74t GHC.Classes.== b2_a74v)))
Derived type family instances:
==================== Filling in method body ====================
GHC.Classes.Eq [QuantifiedConstraints.Foo f_a74w[ssk:1]]
GHC.Classes./= = GHC.Classes.$dm/=
@(QuantifiedConstraints.Foo f_a74w[ssk:1])
```I'd expect the following code to successfully derive a usable `Eq` instance for `Foo`.
```hs
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module QuantifiedConstraints where
import Data.Functor.Identity
type family HKD f a where
HKD Identity a = a
HKD f a = f a
data Foo f = Foo
{ zoo :: HKD f Int
, zum :: HKD f Bool
}
deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
```
However, it complains:
```
• Could not deduce (Eq (HKD f a))
from the context: forall a. Eq a => Eq (HKD f a)
bound by an instance declaration:
forall (f :: * > *).
(forall a. Eq a => Eq (HKD f a)) =>
Eq (Foo f)
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:20:1964
or from: Eq a
bound by a quantified context
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:20:1964
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the standalone deriving instance for
‘(forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)’
```
Adding XAllowAmbiguousTypes doesn't fix the situation:
```
• Could not deduce (Eq (HKD f Int)) arising from a use of ‘==’
from the context: forall a. Eq a => Eq (HKD f a)
bound by the instance declaration
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:21:164
• In the first argument of ‘(&&)’, namely ‘((a1 == b1))’
In the expression: (((a1 == b1)) && ((a2 == b2)))
In an equation for ‘==’:
(==) (Foo a1 a2) (Foo b1 b2) = (((a1 == b1)) && ((a2 == b2)))
When typechecking the code for ‘==’
in a derived instance for ‘Eq (Foo f)’:
To see the code I am typechecking, use ddumpderiv

21  deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:21:1: error:
• Could not deduce (Eq (HKD f a))
arising from a use of ‘GHC.Classes.$dm/=’
from the context: forall a. Eq a => Eq (HKD f a)
bound by the instance declaration
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:21:164
or from: Eq a
bound by a quantified context
at /home/sandy/prj/bookoftypes/code/QuantifiedConstraints.hs:1:1
• In the expression: GHC.Classes.$dm/= @(Foo f)
In an equation for ‘/=’: (/=) = GHC.Classes.$dm/= @(Foo f)
When typechecking the code for ‘/=’
in a derived instance for ‘Eq (Foo f)’:
To see the code I am typechecking, use ddumpderiv
In the instance declaration for ‘Eq (Foo f)’

21  deriving instance (forall a. Eq a => Eq (HKD f a)) => Eq (Foo f)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
and the result of ddumpderiv:
```
==================== Derived instances ====================
Derived class instances:
instance (forall a.
GHC.Classes.Eq a =>
GHC.Classes.Eq (QuantifiedConstraints.HKD f a)) =>
GHC.Classes.Eq (QuantifiedConstraints.Foo f) where
(GHC.Classes.==)
(QuantifiedConstraints.Foo a1_a74s a2_a74t)
(QuantifiedConstraints.Foo b1_a74u b2_a74v)
= (((a1_a74s GHC.Classes.== b1_a74u))
GHC.Classes.&& ((a2_a74t GHC.Classes.== b2_a74v)))
Derived type family instances:
==================== Filling in method body ====================
GHC.Classes.Eq [QuantifiedConstraints.Foo f_a74w[ssk:1]]
GHC.Classes./= = GHC.Classes.$dm/=
@(QuantifiedConstraints.Foo f_a74w[ssk:1])
```8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15593QuantifiedConstraints: trouble with type family20190707T18:03:59ZIcelandjackQuantifiedConstraints: trouble with type family```hs
{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #}
import Data.Kind
data TreeF a b = T0  T1 a  T2 b b
 from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type > Type
class (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
```
fails with
```
$ ~/code/qcghc/inplace/bin/ghcstage2 interactive ignoredotghci 351.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 351.hs, interpreted )
351.hs:12:10: error:
• Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’
arising from the superclasses of an instance declaration
• In the instance declaration for ‘MuRef1 tree’

12  instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```

What I want to write:
```hs
{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #}
import Data.Kind
 from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type > Type
type T = Type
type TT = T > T
type TTT = T > TT
class (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)
instance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)
```
where I am trying to capture [MuRef1 & DeRef1](https://hackage.haskell.org/package/folds0.7.4/docs/src/DataFoldInternal.html)
```hs
class MuRef1 (f :: TT) where
type DeRef1 f :: TTT
muRef1 :: proxy (f a) > Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)
```

Workarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not
```hs
{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #}
 ..
class (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx
instance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx
class (forall xx. cls xx) => Forall cls
instance (forall xx. cls xx) => Forall cls
class Forall (MuRef1_ f deRef1) => MuRef1 f deRef1
instance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1
```
or as a regular type/constraint synonym (at the loss of partial application)
```hs
type MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"QuantifiedConstraints: trouble with type family","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["ConstraintKinds","QuantifiedConstraints,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #}\r\n\r\nimport Data.Kind\r\n\r\ndata TreeF a b = T0  T1 a  T2 b b\r\n\r\n from Data.Reify\r\nclass MuRef (a :: Type) where\r\n type DeRef a :: Type > Type\r\n\r\nclass (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\ninstance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n$ ~/code/qcghc/inplace/bin/ghcstage2 interactive ignoredotghci 351.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 351.hs, interpreted )\r\n\r\n351.hs:12:10: error:\r\n • Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’\r\n arising from the superclasses of an instance declaration\r\n • In the instance declaration for ‘MuRef1 tree’\r\n \r\n12  instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\n\r\n\r\nWhat I want to write:\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #}\r\n\r\nimport Data.Kind\r\n\r\n from Data.Reify\r\nclass MuRef (a :: Type) where\r\n type DeRef a :: Type > Type\r\n\r\ntype T = Type\r\ntype TT = T > T\r\ntype TTT = T > TT\r\n\r\nclass (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)\r\ninstance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)\r\n}}}\r\n\r\nwhere I am trying to capture [https://hackage.haskell.org/package/folds0.7.4/docs/src/DataFoldInternal.html MuRef1 & DeRef1]\r\n\r\n{{{#!hs\r\nclass MuRef1 (f :: TT) where\r\n type DeRef1 f :: TTT\r\n muRef1 :: proxy (f a) > Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)\r\n}}}\r\n\r\n\r\n\r\nWorkarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #}\r\n\r\n ..\r\n\r\nclass (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx\r\ninstance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx\r\n\r\nclass (forall xx. cls xx) => Forall cls\r\ninstance (forall xx. cls xx) => Forall cls\r\n\r\nclass Forall (MuRef1_ f deRef1) => MuRef1 f deRef1\r\ninstance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1\r\n}}}\r\n\r\nor as a regular type/constraint synonym (at the loss of partial application)\r\n\r\n{{{#!hs\r\ntype MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #}
import Data.Kind
data TreeF a b = T0  T1 a  T2 b b
 from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type > Type
class (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
```
fails with
```
$ ~/code/qcghc/inplace/bin/ghcstage2 interactive ignoredotghci 351.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 351.hs, interpreted )
351.hs:12:10: error:
• Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’
arising from the superclasses of an instance declaration
• In the instance declaration for ‘MuRef1 tree’

12  instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
```

What I want to write:
```hs
{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #}
import Data.Kind
 from Data.Reify
class MuRef (a :: Type) where
type DeRef a :: Type > Type
type T = Type
type TT = T > T
type TTT = T > TT
class (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)
instance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)
```
where I am trying to capture [MuRef1 & DeRef1](https://hackage.haskell.org/package/folds0.7.4/docs/src/DataFoldInternal.html)
```hs
class MuRef1 (f :: TT) where
type DeRef1 f :: TTT
muRef1 :: proxy (f a) > Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)
```

Workarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not
```hs
{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #}
 ..
class (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx
instance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx
class (forall xx. cls xx) => Forall cls
instance (forall xx. cls xx) => Forall cls
class Forall (MuRef1_ f deRef1) => MuRef1 f deRef1
instance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1
```
or as a regular type/constraint synonym (at the loss of partial application)
```hs
type MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"QuantifiedConstraints: trouble with type family","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["ConstraintKinds","QuantifiedConstraints,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #}\r\n\r\nimport Data.Kind\r\n\r\ndata TreeF a b = T0  T1 a  T2 b b\r\n\r\n from Data.Reify\r\nclass MuRef (a :: Type) where\r\n type DeRef a :: Type > Type\r\n\r\nclass (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\ninstance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\n$ ~/code/qcghc/inplace/bin/ghcstage2 interactive ignoredotghci 351.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 351.hs, interpreted )\r\n\r\n351.hs:12:10: error:\r\n • Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’\r\n arising from the superclasses of an instance declaration\r\n • In the instance declaration for ‘MuRef1 tree’\r\n \r\n12  instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\n\r\n\r\nWhat I want to write:\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #}\r\n\r\nimport Data.Kind\r\n\r\n from Data.Reify\r\nclass MuRef (a :: Type) where\r\n type DeRef a :: Type > Type\r\n\r\ntype T = Type\r\ntype TT = T > T\r\ntype TTT = T > TT\r\n\r\nclass (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)\r\ninstance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT > TTT)\r\n}}}\r\n\r\nwhere I am trying to capture [https://hackage.haskell.org/package/folds0.7.4/docs/src/DataFoldInternal.html MuRef1 & DeRef1]\r\n\r\n{{{#!hs\r\nclass MuRef1 (f :: TT) where\r\n type DeRef1 f :: TTT\r\n muRef1 :: proxy (f a) > Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)\r\n}}}\r\n\r\n\r\n\r\nWorkarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #}\r\n\r\n ..\r\n\r\nclass (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx\r\ninstance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx\r\n\r\nclass (forall xx. cls xx) => Forall cls\r\ninstance (forall xx. cls xx) => Forall cls\r\n\r\nclass Forall (MuRef1_ f deRef1) => MuRef1 f deRef1\r\ninstance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1\r\n}}}\r\n\r\nor as a regular type/constraint synonym (at the loss of partial application)\r\n\r\n{{{#!hs\r\ntype MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15625GHC panic, with QuantifiedConstraints20190707T18:03:41ZIcelandjackGHC panic, with QuantifiedConstraintsI got a GHC Panic (I made some minor changes to GHC so it may have been added by me) but I think it's caused by the equality constraint
```
$ ~/code/latestghc/inplace/bin/ghcstage2 interactive ignoredotghci ~/hs/390.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/390.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180828 for x86_64unknownlinux):
ASSERT failed!
co_a2DG
df_a2DS @ Any
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/coreSyn/CoreSubst.hs:189:49 in ghc:CoreSubst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
given this code
```hs
{# Language RankNTypes, TypeInType, DataKinds, PolyKinds, TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP, UndecidableSuperClasses, QuantifiedConstraints, FlexibleContexts #}
import Data.Kind
type Cat ob = ob > ob > Type
data KLEISLI (m :: Type > Type) :: Cat (KL_kind m) where
MkKLEISLI :: (a > m b) > KLEISLI(m) (KL a) (KL b)
data KL_kind (m :: Type > Type) = KL Type
class (a ~ KL xx) => AsKL a xx
instance (a ~ KL xx) => AsKL a xx
ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a
ekki__ = MkKLEISLI undefined
```I got a GHC Panic (I made some minor changes to GHC so it may have been added by me) but I think it's caused by the equality constraint
```
$ ~/code/latestghc/inplace/bin/ghcstage2 interactive ignoredotghci ~/hs/390.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/390.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180828 for x86_64unknownlinux):
ASSERT failed!
co_a2DG
df_a2DS @ Any
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/coreSyn/CoreSubst.hs:189:49 in ghc:CoreSubst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
given this code
```hs
{# Language RankNTypes, TypeInType, DataKinds, PolyKinds, TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP, UndecidableSuperClasses, QuantifiedConstraints, FlexibleContexts #}
import Data.Kind
type Cat ob = ob > ob > Type
data KLEISLI (m :: Type > Type) :: Cat (KL_kind m) where
MkKLEISLI :: (a > m b) > KLEISLI(m) (KL a) (KL b)
data KL_kind (m :: Type > Type) = KL Type
class (a ~ KL xx) => AsKL a xx
instance (a ~ KL xx) => AsKL a xx
ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a
ekki__ = MkKLEISLI undefined
```