[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:                    |
-------------------------------------+-------------------------------------

Comment (by aaronvargo):

 Replying to [comment:10 simonpj]:

 A few things:

 First, there's probably another way to do this without a free-variable
 analysis: float type families out when they appear in wanted constraints.
 E.g. in `foo`, the floating would happen because `F b` appears in the
 wanted constraint, not because it's independent of the forall'd variables
 in the given quantified constraint. Would something like that be more
 feasible?

 Second,

 > Consider this:
 > {{{
 > type family F a
 > type instance F Int = Bool
 >
 > instance Eq a => Eq (F a) where ...
 > }}}
 > Should we allow this?  Obviously not.  It's like allowing...

 Indeed, but this is an argument for disallowing ambiguity, not for
 disallowing type families. In your `Eq` example, `a` is ambiguous since
 `F` may not be injective. (likewise, `xs` and `ys` are ambiguous in the
 `map` example since `(++)` isn't injective). Not all uses of type families
 cause such ambiguity, and the compiler already has a perfectly good
 ambiguity check which can determine whether they do. Some cases where they
 don't are:

 1. The type family is independent of the quantified variables
 2. The type family is injective
 3. The type family can be reduced to an expression which is unambiguous
 (this is #13262)
 4. The quantified variables appear ambiguously in the type family, but are
 still made unambiguous by the rest of the instance head (e.g. `forall a. C
 (F a) a`)

 For top-level instances there may be coherence issues with allowing type
 families even when they don't cause ambiguity (though I'm not sure that
 there are), but such issues don't apply to QCs, which can't introduce
 incoherence.

 So why not allow type families in QCs, but require that the quantified
 variables be unambiguous?

 Third, working around this by manually floating out type families can be
 hugely painful, as it requires sacrificing one of the major benefits of
 type families, namely the ability to avoid passing around extra class
 parameters which are already determined by other parameters. The basic
 problem is this: suppose we have a class:

 {{{#!hs
 class (forall a. Eq a => Eq (f a)) => C f t | t -> f
 }}}

 Currently, the parameter `f` can never be instantiated with a type family
 without breaking the quantified constraint. This means the extra parameter
 needs to be repeated throughout the code for the QC to continue to work,
 despite the fact that `f` is already determined by `t`.

 Consider the following encoding of categories and functors, which makes
 use of type families:

 {{{#!hs
 type Hom k = k -> k -> Type

 -- Natural transformations
 data (==>) (p :: Hom i) (q :: Hom j) (f :: i -> j) (g :: i -> j)

 class ( Category (Op p)
       , Op (Op p) ~ p
       , Ob (Op p) ~ Ob p
       , FunctorOf' (Op p) (p ==> (->)) p
       , forall a. Ob p a => FunctorOf' p (->) (p a)
       ) => Category (p :: Hom k) where
   type Ob p :: k -> Constraint
   type Op p :: Hom k

 -- FunctorOf without superclasses, to work around issues with
 UndecidableSuperClasses
 class FunctorOf' p q (f :: i -> j) | f -> p q

 -- FunctorOf' with proper superclasses
 class ( FunctorOf' p q f
       , Category p
       , Category q
       , forall a. Ob p a => Ob q (f a)
       ) => FunctorOf p q f
 instance ( FunctorOf' p q f
          , Category p
          , Category q
          , forall a. Ob p a => Ob q (f a)
          ) => FunctorOf p q f
 }}}

 Note that `Category p` has a superclass `Category (Op p)`, which has a
 superclass:

 {{{#!hs
 -- noting that Ob (Op p) ~ Ob p
 forall a. Ob p a => FunctorOf' (Op p) (->) (Op p a)
 }}}

 and that the superclasses of `FunctorOf p q f` include:

 {{{#!hs
 forall a. Ob p a => Ob q (f a)
 forall a. Ob p a => FunctorOf' (Op p) (->) (Op p a)
 forall a. Ob q a => FunctorOf' (Op q) (->) (Op q a)
 }}}

 All of these have independent type families in the heads. Floating them
 out manually requires doubling the number of class parameters for both
 `Category` and `FunctorOf`:

 {{{#!hs
 class (..., op ~ Op p) => Category op p where ...

 class ( FunctorOf' p q f
       , Category opP p
       , Category opQ q
       , obQ ~ Ob q
       , forall a. Ob p a => obQ (f a)
       ) => FunctorOf opP p opQ q obQ f
 }}}

 These parameters will spread throughout all of the code. Subclasses will
 add yet more parameters, and will never be able to use type families for
 anything which is a functor or a category, without sacrificing some QCs.
 Types will be lost in a sea of parameters.

 This ends up being more painful than just using `Dict`s.

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