Inconsistency in quantified constraint solving

Consider the following program:

{-# 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:

-- <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.

Trac metadata

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