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

[GHC]

#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