[GHC] #14860: QuantifiedConstraints: Can't quantify constraint involving type family

[GHC]

#14860: QuantifiedConstraints: Can't quantify constraint involving type family
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:  wontfix           |  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):

 This is tricky in an interesting way.

 What is the problem with quantified constraints with a type-function in
 the head?
 Consider
 {{{
 f :: (forall a. C a => C (F a)) => ...
 }}}
 where `F` is a type family.   We really, really can't handle this.
 Suppose we have
 {{{
 type instance F [b] = (b,b)
 }}}
 and we are trying to solve `C (t,t)` in `f`'s RHS.  Well that's the same
 as `C (F [t])` and lo,
 now the quantified constraint matches.

 It would be utterly different if we had
 {{{
 f :: C (F a) => ...
 f = ...needs (C (F a))...
 }}}
 where the two constraints are patently equal; and it'd be equally fine if
 we
 had an enclosing constraint (from a GADT, say) telling us `a ~ [b]`.  Then
 we'd rewrite both the "given" and the "wanted" to `C (F [b])`, and if that
 in turn rewrites to `C (b,b)` then both will so rewrite. It's all fine.

 The trouble in the earlier example comes because `F` is applied to a
 quantified variable.  Here's another example it is, by comparison, fine:
 {{{
 type family F2 a :: * -> *
 f2 :: (forall b. C b => C (F2 x b)) => blah
 }}}
 Notice that `F2` has arity 1. And notice that the saturated application
 `(F2 x)` does not mention the quantified variable `b`.  So we could
 rewrite
 the signature thus:
 {{{
 f2a :: (y ~ F2 x, forall b. C b => C (y b)) => blah
 }}}
 This is fine, and it is accepted today.  By binding `F2 x` to `y`
 ''outside'' the
 quantification we have shown that the problems described above (about F)
 can't happen.

 Alas, `f2` is ''not'' accepted today.  Until today I thought that once
 could
 always rewrite in the `f2a` style, and that it would be positively good to
 do so.
 That's what comment:1 says.

 But today you have shown me a counter example.  I cannot apply that trick
 to
 {{{
 class (forall b. Show b => Show (T a b)) => C a where
   type family T a :: * -> *
 }}}
 I might try
 {{{
 class (y ~ T a, forall b. Show b => Show (y b)) => C a where
   type family T a :: * -> *
 }}}
 But now `y` is not bound in the class head, and we just don't allow that.
 (Why not?  Because a class turns into a data type declaration
 {{{
 data C a = MkC (..superclass1..)
                (..superclass2..)  etc
                (..method1..)
                (..method2..)  etc
 }}}
 so the superclass types can't mention variables not bound on the left.
 No we do not want existentials here.)

 So I am driven to the conclusion:

 * Perhaps we should allow type-family applications in the head of a
 quantified constraint, provided that the saturated application of the
 family does not mention any of the quantified variables.

 The flattener would have to work a bit harder.  Richard, what do you
 think?

 Thanks for the example.

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