[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:20 simonpj]:

 > Not allowing functions in the instance head not to do with ambiguity;
 it's to do with coherence

 But is this an issue for QCs, which can't introduce incoherence? Does it
 matter if two QCs might overlap, as long as locally we can't tell that
 they do? Suppose we had:

 {{{#!hs
 type family F a = r | r -> a
 type family G a = r | r -> a

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

 While `F b` and `G b` might overlap for some particular `b`, locally only
 one instance can be used to solve `Eq (F b)`, since we don't know whether
 `G b ~ F b`. Since the two instances are guaranteed to be coherent,
 wouldn't it be fine to simply pick the one that matches? (If both were to
 match then the program would still be rejected).

 Likewise for the case with non-injective independent type families:

 {{{#!hs
 foo :: forall b. (forall t. C (F b) [t], forall t. C (G b) [t]) => Dict (C
 (F b) [Int])
 }}}

 The first instance should just be used, since it's the only one that
 matches given the knowledge available locally.

 How does the compiler currently deal with type families in non-quantified
 constraints? What makes it more difficult to allow them in QCs?

 > Can you distil a small example that shows the utility of having a
 function in the head?

 For now I have no use case for the injective type family case, and only
 really care about the independent family case. I'll try and come up with a
 simpler example than the category one.

 > So, maybe a quantified constraint with a function in the head is just
 "parked", but it wakes up if the function can be reduced.

 This is much less useful than what I want, though I suppose it might help
 in some small minority of cases.

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