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:171
• 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 patternmatching 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
patternmatching 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 