Inconsistency in quantified constraint solving
Consider the following program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
m :: a -> ()
data Dict c = c => Dict
-----
type family F a :: Type -> Type
class C (F a b) => CF a b
instance C (F a b) => CF a b
works1 :: (forall z. CF a z) => Proxy (a, b) -> Dict (CF a b)
works1 _ = Dict
works2 :: ( CF a b) => Proxy (a, b) -> Dict (C (F a b))
works2 _ = Dict
works3, fails :: (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))
works3 p | Dict <- works1 p = Dict
fails _ = Dict
```
`fails`, as its name suggests, fails to typecheck:
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:33:11: error:
• Could not deduce (C (F a b)) arising from a use of ‘Dict’
from the context: forall z. CF a z
bound by the type signature for:
fails :: forall a b.
(forall z. CF a z) =>
Proxy (a, b) -> Dict (C (F a b))
at Bug.hs:31:1-71
• In the expression: Dict
In an equation for ‘fails’: fails _ = Dict
|
33 | fails _ = Dict
| ^^^^
```
But I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)?
Note that something with the type `(forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit pattern-matching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary.
Moreover, in this variation of the program above:
```hs
-- <as above>
-----
data G a :: Type -> Type
class C (G a b) => CG a b
instance C (G a b) => CG a b
works1' :: (forall z. CG a z) => Proxy (a, b) -> Dict (CG a b)
works1' _ = Dict
works2' :: ( CG a b) => Proxy (a, b) -> Dict (C (G a b))
works2' _ = Dict
works3' :: (forall z. CG a z) => Proxy (a, b) -> Dict (C (G a b))
works3' _ = Dict
```
`works3'` needs no explicit `Dict` pattern-matching to typecheck.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.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":"Inconsistency in quantified constraint solving","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE QuantifiedConstraints #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n m :: a -> ()\r\n\r\ndata Dict c = c => Dict\r\n\r\n-----\r\n\r\ntype family F a :: Type -> Type\r\nclass C (F a b) => CF a b\r\ninstance C (F a b) => CF a b\r\n\r\nworks1 :: (forall z. CF a z) => Proxy (a, b) -> Dict (CF a b)\r\nworks1 _ = Dict\r\n\r\nworks2 :: ( CF a b) => Proxy (a, b) -> Dict (C (F a b))\r\nworks2 _ = Dict\r\n\r\nworks3, fails :: (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))\r\nworks3 p | Dict <- works1 p = Dict\r\nfails _ = Dict\r\n}}}\r\n\r\n`fails`, as its name suggests, fails to typecheck:\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:33:11: error:\r\n • Could not deduce (C (F a b)) arising from a use of ‘Dict’\r\n from the context: forall z. CF a z\r\n bound by the type signature for:\r\n fails :: forall a b.\r\n (forall z. CF a z) =>\r\n Proxy (a, b) -> Dict (C (F a b))\r\n at Bug.hs:31:1-71\r\n • In the expression: Dict\r\n In an equation for ‘fails’: fails _ = Dict\r\n |\r\n33 | fails _ = Dict\r\n | ^^^^\r\n}}}\r\n\r\nBut I see no reason why this shouldn't typecheck. After all, the fact that `works1` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)` implies `(CF a b)`, and the fact that `works2` typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)` implies that `(C (F a b))`. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)` implies `(C (F a b))` (in the type of `fails`)?\r\n\r\nNote that something with the type `(forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))` //can// be made to work if you explicitly guide GHC along with explicit pattern-matching on a `Dict`, as `works3` demonstrates. But I claim that this shouldn't be necessary.\r\n\r\nMoreover, in this variation of the program above:\r\n\r\n{{{#!hs\r\n-- <as above>\r\n-----\r\n\r\ndata G a :: Type -> Type\r\nclass C (G a b) => CG a b\r\ninstance C (G a b) => CG a b\r\n\r\nworks1' :: (forall z. CG a z) => Proxy (a, b) -> Dict (CG a b)\r\nworks1' _ = Dict\r\n\r\nworks2' :: ( CG a b) => Proxy (a, b) -> Dict (C (G a b))\r\nworks2' _ = Dict\r\n\r\nworks3' :: (forall z. CG a z) => Proxy (a, b) -> Dict (C (G a b))\r\nworks3' _ = Dict\r\n}}}\r\n\r\n`works3'` needs no explicit `Dict` pattern-matching to typecheck.","type_of_failure":"OtherFailure","blocking":[]} -->
issue