GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:03:39Zhttps://gitlab.haskell.org/ghc/ghc//issues/15636Implication constraint priority breaks default class implementations20190707T18:03:39ZiamtomImplication constraint priority breaks default class implementationsHello,
Not 100% sure that this is a bug, but I've done some investigating (with a *lot* of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
module Test where
class D a where
f :: a > String
g :: a > String
g = f
class C a
instance (forall a. C a => D a) => D x where
f _ = "uh oh"
```
1. .. produces the error:
```
• Could not deduce (C x) arising from a use of ‘Test.$dmg’
from the context: forall a. C a => D a
bound by the instance declaration at Test.hs:19:1038
Possible fix: add (C x) to the context of the instance declaration
• In the expression: Test.$dmg @(x)
In an equation for ‘g’: g = Test.$dmg @(x)
In the instance declaration for ‘D x’

19  instance (forall a. C a => D a) => D x where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
It appears that the problem here is with the default implementation for `g`. Namely, when `f` is called, two matching instances are found:
 `forall a. C a => D a`
 `(forall a. C a => D a) => D x`
The issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.
Let me know if I've missed anything from this ticket  it's my first one!
Thanks,
Tom
† An example of this can be found at https://github.com/iamtom/learnmeahaskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs\#L92L94
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 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":"Implication constraint priority breaks default class implementations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Hello,\r\n\r\nNot 100% sure that this is a bug, but I've done some investigating (with a ''lot'' of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Test where\r\n\r\nclass D a where\r\n f :: a > String\r\n g :: a > String\r\n g = f\r\n\r\nclass C a\r\n\r\ninstance (forall a. C a => D a) => D x where\r\n f _ = \"uh oh\"\r\n}}}\r\n\r\n... produces the error:\r\n\r\n{{{\r\n • Could not deduce (C x) arising from a use of ‘Test.$dmg’\r\n from the context: forall a. C a => D a\r\n bound by the instance declaration at Test.hs:19:1038\r\n Possible fix: add (C x) to the context of the instance declaration\r\n • In the expression: Test.$dmg @(x)\r\n In an equation for ‘g’: g = Test.$dmg @(x)\r\n In the instance declaration for ‘D x’\r\n \r\n19  instance (forall a. C a => D a) => D x where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nIt appears that the problem here is with the default implementation for `g`. Namely, when `f` is called, two matching instances are found:\r\n\r\n `forall a. C a => D a`\r\n `(forall a. C a => D a) => D x`\r\n\r\nThe issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.\r\n\r\nLet me know if I've missed anything from this ticket  it's my first one!\r\n\r\nThanks,\r\nTom\r\n\r\n† An example of this can be found at https://github.com/iamtom/learnmeahaskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs#L92L94","type_of_failure":"OtherFailure","blocking":[]} >Hello,
Not 100% sure that this is a bug, but I've done some investigating (with a *lot* of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
module Test where
class D a where
f :: a > String
g :: a > String
g = f
class C a
instance (forall a. C a => D a) => D x where
f _ = "uh oh"
```
1. .. produces the error:
```
• Could not deduce (C x) arising from a use of ‘Test.$dmg’
from the context: forall a. C a => D a
bound by the instance declaration at Test.hs:19:1038
Possible fix: add (C x) to the context of the instance declaration
• In the expression: Test.$dmg @(x)
In an equation for ‘g’: g = Test.$dmg @(x)
In the instance declaration for ‘D x’

19  instance (forall a. C a => D a) => D x where
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
It appears that the problem here is with the default implementation for `g`. Namely, when `f` is called, two matching instances are found:
 `forall a. C a => D a`
 `(forall a. C a => D a) => D x`
The issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.
Let me know if I've missed anything from this ticket  it's my first one!
Thanks,
Tom
† An example of this can be found at https://github.com/iamtom/learnmeahaskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs\#L92L94
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 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":"Implication constraint priority breaks default class implementations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Hello,\r\n\r\nNot 100% sure that this is a bug, but I've done some investigating (with a ''lot'' of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Test where\r\n\r\nclass D a where\r\n f :: a > String\r\n g :: a > String\r\n g = f\r\n\r\nclass C a\r\n\r\ninstance (forall a. C a => D a) => D x where\r\n f _ = \"uh oh\"\r\n}}}\r\n\r\n... produces the error:\r\n\r\n{{{\r\n • Could not deduce (C x) arising from a use of ‘Test.$dmg’\r\n from the context: forall a. C a => D a\r\n bound by the instance declaration at Test.hs:19:1038\r\n Possible fix: add (C x) to the context of the instance declaration\r\n • In the expression: Test.$dmg @(x)\r\n In an equation for ‘g’: g = Test.$dmg @(x)\r\n In the instance declaration for ‘D x’\r\n \r\n19  instance (forall a. C a => D a) => D x where\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nIt appears that the problem here is with the default implementation for `g`. Namely, when `f` is called, two matching instances are found:\r\n\r\n `forall a. C a => D a`\r\n `(forall a. C a => D a) => D x`\r\n\r\nThe issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.\r\n\r\nLet me know if I've missed anything from this ticket  it's my first one!\r\n\r\nThanks,\r\nTom\r\n\r\n† An example of this can be found at https://github.com/iamtom/learnmeahaskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs#L92L94","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15635Implication introduction for quantified constraints20190707T18:03:39ZDavid FeuerImplication introduction for quantified constraintsNow that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:
```hs
data Dict a where
Dict :: a => Dict a
newtype a : b = Sub (a => Dict b)
```
`QuantifiedConstraints` suggests another version of `:`:
```hs
newtype Imp a b = Imp
{ unImp :: forall r. ((a => b) => r) > r}
```
We can write
```hs
fromImp :: Imp a b > a : b
fromImp (Imp f) = Sub (f Dict)
```
But ... there's no way to go the other way!
Let's try it:
```hs
toImp :: a : Dict b > a : b
toImp (Sub ab) = Imp $ \r > _
```
We get
```
* Found hole: _ :: r
* Relevant bindings include
r :: (a => b) => r
ab :: a => Dict b
```
There's no way to put these things together. But there's no terribly obvious reason they ''can't* be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that *contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:
```hs
implIntro
:: ((a => b) => q)
> (forall r. (b => r) > (a => r))
> q
```
In Core (modulo type abstraction and application), we could simply write
```hs
implIntro f g = f (g id)
```
Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implication introduction for quantified constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:\r\n\r\n{{{#!hs\r\ndata Dict a where\r\n Dict :: a => Dict a\r\n\r\nnewtype a : b = Sub (a => Dict b)\r\n}}}\r\n\r\n`QuantifiedConstraints` suggests another version of `:`:\r\n\r\n{{{#!hs\r\nnewtype Imp a b = Imp\r\n { unImp :: forall r. ((a => b) => r) > r}\r\n}}}\r\n\r\nWe can write\r\n\r\n{{{#!hs\r\nfromImp :: Imp a b > a : b\r\nfromImp (Imp f) = Sub (f Dict)\r\n}}}\r\n\r\nBut ... there's no way to go the other way!\r\n\r\nLet's try it:\r\n\r\n{{{#!hs\r\ntoImp :: a : Dict b > a : b\r\ntoImp (Sub ab) = Imp $ \\r > _\r\n}}}\r\n\r\nWe get\r\n\r\n{{{\r\n* Found hole: _ :: r\r\n* Relevant bindings include\r\n r :: (a => b) => r\r\n ab :: a => Dict b\r\n}}}\r\n\r\nThere's no way to put these things together. But there's no terribly obvious reason they ''can't'' be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that ''contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:\r\n\r\n{{{#!hs\r\nimplIntro\r\n :: ((a => b) => q)\r\n > (forall r. (b => r) > (a => r))\r\n > q\r\n}}}\r\n\r\nIn Core (modulo type abstraction and application), we could simply write\r\n\r\n{{{#!hs\r\nimplIntro f g = f (g id)\r\n}}}\r\n\r\nUnfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space.","type_of_failure":"OtherFailure","blocking":[]} >Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:
```hs
data Dict a where
Dict :: a => Dict a
newtype a : b = Sub (a => Dict b)
```
`QuantifiedConstraints` suggests another version of `:`:
```hs
newtype Imp a b = Imp
{ unImp :: forall r. ((a => b) => r) > r}
```
We can write
```hs
fromImp :: Imp a b > a : b
fromImp (Imp f) = Sub (f Dict)
```
But ... there's no way to go the other way!
Let's try it:
```hs
toImp :: a : Dict b > a : b
toImp (Sub ab) = Imp $ \r > _
```
We get
```
* Found hole: _ :: r
* Relevant bindings include
r :: (a => b) => r
ab :: a => Dict b
```
There's no way to put these things together. But there's no terribly obvious reason they ''can't* be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that *contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:
```hs
implIntro
:: ((a => b) => q)
> (forall r. (b => r) > (a => r))
> q
```
In Core (modulo type abstraction and application), we could simply write
```hs
implIntro f g = f (g id)
```
Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.1beta1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implication introduction for quantified constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:\r\n\r\n{{{#!hs\r\ndata Dict a where\r\n Dict :: a => Dict a\r\n\r\nnewtype a : b = Sub (a => Dict b)\r\n}}}\r\n\r\n`QuantifiedConstraints` suggests another version of `:`:\r\n\r\n{{{#!hs\r\nnewtype Imp a b = Imp\r\n { unImp :: forall r. ((a => b) => r) > r}\r\n}}}\r\n\r\nWe can write\r\n\r\n{{{#!hs\r\nfromImp :: Imp a b > a : b\r\nfromImp (Imp f) = Sub (f Dict)\r\n}}}\r\n\r\nBut ... there's no way to go the other way!\r\n\r\nLet's try it:\r\n\r\n{{{#!hs\r\ntoImp :: a : Dict b > a : b\r\ntoImp (Sub ab) = Imp $ \\r > _\r\n}}}\r\n\r\nWe get\r\n\r\n{{{\r\n* Found hole: _ :: r\r\n* Relevant bindings include\r\n r :: (a => b) => r\r\n ab :: a => Dict b\r\n}}}\r\n\r\nThere's no way to put these things together. But there's no terribly obvious reason they ''can't'' be combined. `a => b` is a function from an `a` dictionary to a `b` dictionary. `a => Dict b` is a function from an `a` dictionary to a value that ''contains'' a `b` dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:\r\n\r\n{{{#!hs\r\nimplIntro\r\n :: ((a => b) => q)\r\n > (forall r. (b => r) > (a => r))\r\n > q\r\n}}}\r\n\r\nIn Core (modulo type abstraction and application), we could simply write\r\n\r\n{{{#!hs\r\nimplIntro f g = f (g id)\r\n}}}\r\n\r\nUnfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space.","type_of_failure":"OtherFailure","blocking":[]} >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/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/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/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.1