Re: [GHC] #15347: QuantifiedConstraints: Implication constraints with type families don't work

5 Jul 2018

      #15347: QuantifiedConstraints: Implication constraints with type families don't
work
-------------------------------------+-------------------------------------
        Reporter:  aaronvargo        |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:                    |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Old description:
...
This may be related to #14860, but I think it's different.
The following code fails to compile:
{{{#!hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
import Prelude()
import Data.Kind
data Dict c = c => Dict
type family F a :: Constraint
foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
}}}
{{{
• Could not deduce: F b arising from a use of ‘Dict’
  from the context: (a => F b, a)
}}}
Yet the following all do compile:
{{{#!hs
bar :: forall a. F a => Dict (F a)
bar = Dict
baz :: forall a b. (a => b, a) => Dict b
baz = Dict
qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict
}}}
It seems that a wanted `F b` can be solved with a given `F b`, but not
with a given `a => F b`, which is bizarre. The fact that `qux` still
works is also strange, as it means that you get a different result if you
first simplify by substituting `c = F b`.
As a more practical example, the following similarly fails to compile,
due to the `Cod f` type family:
{{{#!hs
-- in addition to the above extensions
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
class Ob p a
class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
  type Dom f
  type Cod f
liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f
a))
liftOb = Dict
}}}
While a version which uses fundeps instead does compile:
{{{#!hs
class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f ->
dom cod
liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob
cod (f a))
liftOb = Dict
}}}
New description:

 This may be related to #14860, but I think it's different.

 The following code fails to compile:

 {{{#!hs
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ConstraintKinds #-}

 import Prelude()
 import Data.Kind

 data Dict c = c => Dict

 type family F a :: Constraint

 foo :: forall a b. (a => F b, a) => Dict (F b)
 foo = Dict
 }}}

 {{{
 • Could not deduce: F b arising from a use of ‘Dict’
   from the context: (a => F b, a)
 }}}

 Yet the following all do compile:

 {{{#!hs
 bar :: forall a. F a => Dict (F a)
 bar = Dict

 baz :: forall a b. (a => b, a) => Dict b
 baz = Dict

 qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
 qux = Dict
 }}}

 It seems that a wanted `F b` can be solved with a given `F b`, but not
 with a given `a => F b`, which is bizarre. The fact that `qux` still works
 is also strange, as it means that you get a different result if you first
 simplify by substituting `c = F b`.

 As a more practical example, the following similarly fails to compile, due
 to the `Cod f` type family:

 {{{#!hs
 -- in addition to the above extensions
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}

 class Ob p a

 class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
   type Dom f
   type Cod f

 liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
 liftOb = Dict
 }}}

 While a version which uses fundeps instead does compile:

 {{{#!hs
 class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f -> dom
 cod

 liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob
 cod (f a))
 liftOb = Dict
 }}}

--

Comment (by aaronvargo):

 Actually, the `Functor` example with type families can be fixed by
 replacing:

 {{{#!hs
 forall a. Ob (Dom f) a => Ob (Cod f) (f a)
 }}}

 with

 {{{#!hs
 forall a cod. (Ob (Dom f) a, cod ~ Cod f) => Ob cod (f a)
 }}}

 Perhaps the compiler could do this rewrite automatically? It rightly
 doesn't in the case of instance declarations, but perhaps it's fine for
 quantified constraints.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler