#16365: Inconsistency in quantified constraint solving

#16365: Inconsistency in quantified constraint solving
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16365>