[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 simonpj):

 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
 {{{
 map f (xs ++ ys) = map f xs ++ map f ys
 map f []         = []
 }}}
 where we have a function call in the pattern match.
 All manner of overlaps a chaos would result.
 So generally GHC does not allow type family calls in
 the head of an instance declaration.  And I've made that same
 rule apply to quantified constraints, which are really just local
 instance declarations.

 But, you say, how are these two different?
 {{{
 foo :: forall a b.   (a => F b,        a) => Dict (F b)
 qux :: forall a b c. (a => c, c ~ F b, a) => Dict (F b)
 }}}
 Very different, I say!  Suppose that quantified constraint had looked
 like this
 {{
 foo :: forall a b.   (forall t. a => F t b,  ...) => Dict (F b)
 }}
 Notice that the locally-quantified `t` is one of the arguments to `F`.
 Now, all the bad things could happen.  What is different about your
 example is that '''the function call is independent of any of the
 forall'd variables of the quantified constraint'''.  You expressed
 that by floating it out of the quantified constraint with you `c ~ F b`.
 And because it is independent of the forall'd variables, it is really
 constant so far as the instance is concerned, and doesn't lead to
 problems.

 Here's another variant:
 {{{
 foo :: forall b. (forall t. C b t => C (F b) [t],  ...) => Dict (F b)
 }}}
 Now the head of the quantified constraint does mention the forall'd `t`,
 but the call to `F` does not, so we can float thus:
 {{{
 foo :: forall b c. (c ~ F b, forall t. C b t => C c [t],  ...) => Dict (F
 b)
 }}}
 This directly expresses the fact that the first parameter to `C` in the
 head
 of the quantified constraint is independent of `t`.

 Now, you want this floating business to happen automatically, but I think
 it is much too complicated to do behind the scenes.  If that's what you
 want, you can say it.  I would be reluctant to introduce a significant
 (and unprecedented) implicit translation, based on a free-variable
 analysis,
 without plenty of evidence that it was going to have major benefit for a
 significant constituency.  I don't think we are close to that point yet.

 But it ''is'' a nice observation that, by expressing the independence with
 an equality constraint, you can say just what you mean, and get just what
 you want.  (I doubt that fundeps would be any help here.)

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