QuantifiedConstraints: Can't quantify constraint involving type family
This program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Proxy
type family Apply (f :: * -> *) a
type instance Apply Proxy a = Proxy a
data ExTyFam f where
MkExTyFam :: Apply f a -> ExTyFam f
instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
show (MkExTyFam x) = show x
showsPrec = undefined -- Not defining these leads to the oddities observed in
showList = undefined -- https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32
test :: ExTyFam Proxy -> String
test = show
```
This fails with:
```
$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:24: error:
• Could not deduce (Show (Apply f a)) arising from a use of ‘show’
from the context: forall a. Show (Apply f a)
bound by the instance declaration at Bug.hs:16:10-57
• In the expression: show x
In an equation for ‘show’: show (MkExTyFam x) = show x
In the instance declaration for ‘Show (ExTyFam f)’
|
17 | show (MkExTyFam x) = show x
| ^^^^^^
```
I would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.
<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":"QuantifiedConstraints: Can't quantify constraint involving type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program fails to typecheck using the `wip/T2893` branch, to my surprise:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE QuantifiedConstraints #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\ntype family Apply (f :: * -> *) a\r\ntype instance Apply Proxy a = Proxy a\r\n\r\ndata ExTyFam f where\r\n MkExTyFam :: Apply f a -> ExTyFam f\r\n\r\ninstance (forall a. Show (Apply f a)) => Show (ExTyFam f) where\r\n show (MkExTyFam x) = show x\r\n showsPrec = undefined -- Not defining these leads to the oddities observed in\r\n showList = undefined -- https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32\r\n\r\ntest :: ExTyFam Proxy -> String\r\ntest = show\r\n}}}\r\n\r\nThis fails with:\r\n\r\n{{{\r\n$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:17:24: error:\r\n • Could not deduce (Show (Apply f a)) arising from a use of ‘show’\r\n from the context: forall a. Show (Apply f a)\r\n bound by the instance declaration at Bug.hs:16:10-57\r\n • In the expression: show x\r\n In an equation for ‘show’: show (MkExTyFam x) = show x\r\n In the instance declaration for ‘Show (ExTyFam f)’\r\n |\r\n17 | show (MkExTyFam x) = show x\r\n | ^^^^^^\r\n}}}\r\n\r\nI would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.","type_of_failure":"OtherFailure","blocking":[]} -->
issue