[GHC] #11534: Allow class associated types to reference functional dependencies

[GHC]

#11534: Allow class associated types to reference functional dependencies
-------------------------------------+-------------------------------------
        Reporter:  ekmett            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  FunctionalDependencies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by ekmett):

 > What type family do you need to partially apply?

 Given the single parameter `Functor` class, I would need to be able to
 supply something with kind `(i -> j) -> Constraint`, that says that its
 type argument is not just a Functor, but has a given `Dom` and a given
 `Cod`.

 {{{#!hs
 class (Functor f, Dom f ~ c, Cod f ~ d) => FunctorOf c d f | f -> c d
 instance (Functor f, Dom f ~ c, Cod f ~ d) => FunctorOf c d f
 }}}

 acts just like the type synonym

 {{{#!hs
 type FunctorOf c d f = (Functor f, Dom f ~ c, Cod f ~ d)
 }}}

 ''except'' it can be partially applied to the first two arguments to fix
 the Dom and Cod of its argument, whereas the type synonym version can't
 must be supplied all three arguments.

 Now I can answer

 > What type family do you need to partially apply?

 The answer is `FunctorOf c d`.


 This lets me write the line

 {{{#!hs
 instance (Category p, Category q) => Category (Nat p q) where
   type Ob (Nat p q) = FunctorOf p q
 }}}

 Because I can "partially apply" FunctorOf p q to get something of kind `(i
 -> j) -> Constraint`.

 Unfortunately, as noted with #11523 with `UndecidableSuperClasses` turned
 on, I spin forever trying to use the `FunctorOf` definition in this place.

 The "obvious" fix then is to go through and replace the class associated
 type `Ob f :: i -> Constraint` with `type Ob f a :: Constraint`, but take
 an extra argument fails because I ultimately wind up needing to claim that
 `Ob (Nat p q)` is a functor from `p` to the category of constraints and it
 can't be if it can't be partially applied in its own right.

 Similar issues arise forcing the class/instance trick to deal with
 constraints elsewhere:

 {{{#!hs
 class (p, q) => p & q
 instance (p, q) => p & q
 }}}

 let's me talk about `(&) :: Constraint -> Constraint -> Constraint` or
 `(&) (Eq a) :: Constraint -> Constraint)`, whereas only a fully applied
 pair at the type level can be spoken of due to the limitations of the
 syntactic / semantic hack that we have in place for products of
 constraints.

 > Can you give concrete examples?

 Every single definition in the `monads-tf` library has a significantly
 more verbose type signature than the ones in the `mtl`.

 {{{#!hs
 modify :: MonadState s m => (s -> s) -> m ()
 tell :: MonadWriter e m => e -> m ()
 ask :: MonadReader e m => m e
 local :: MonadReader e m => (e -> e) -> m a -> m a
 }}}

 vs.

 {{{#!hs
 modify :: MonadState m => (StateType m -> StateType m) -> m ()
 tell :: MonadWriter m => WriterType m -> m ()
 ask :: MonadReader m => m (EnvType m)
 local :: MonadReader m => (EnvType m -> EnvType m) -> m a -> m a
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11534#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler