Re: [GHC] #15347: QuantifiedConstraints: Implication constraints with type families don't work

7 Jul 2018

      #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):

 Yes, that's what I wanted, but after thinking a bit, I think the current
 behavior may actually be broken anyway!

 Consider:

 {{{#!hs
 type family F a :: Constraint

 yikes :: forall a b fb.
   ( a => fb
   , fb ~ F b
   )
   => Dict (Eq Int)
 yikes = Dict
 }}}

 The above compiles, but with the current behavior, it actually violates
 the open world assumption! Consider what happens if we now add:

 {{{#!hs
 type instance F a = Eq Int
 }}}

 {{{
 • Could not deduce: a arising from a use of ‘Dict’
   from the context: (a => fb, fb ~ F b)
     bound by the type signature for:
                 yikes :: forall (a :: Constraint) b (fb :: Constraint).
                         (a => fb, fb ~ F b) =>
                         Dict (Eq Int)

 • In the expression: Dict
   In an equation for ‘yikes’: yikes = Dict
 }}}

 The problem is that since `fb ~ F b`, the `a => fb` constraint can overlap
 if `F b` can be reduced further.

 A possible solution is to always first reduce the heads of given
 quantified constraints using given equalities. Then `a => fb` will become
 `a => F b`, and won't be usable since `F b` isn't a valid instance head.
 `qux` would then no longer compile, while `yikes` would continue to
 compile even after the type instance is added.

 My trick of floating out type families shouldn't even work!

 I'm not sure that that even completely solves the problem
 though...Consider:

 {{{#!hs
 type family F a :: Constraint

 type instance F String = ()

 whatAboutThis :: forall a b.
   ( F String => (b ~ Int)
   , a => Eq b
   ) => Dict (Eq Int)
 whatAboutThis = Dict
 }}}

 Currently this compiles. Should it?

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