[GHC] #16365: Inconsistency in quantified constraint solving

[GHC]

#16365: Inconsistency in quantified constraint solving
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
                                     |  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):

 Ah!  I had not focused on the fact that `F` only has arity 1. Good point.

 Avoiding the issues of superclasses for now, this fails:
 {{{
 fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b))
 fails2 _ = Dict
 }}}
 saying (quite helpfully)
 {{{
 T16365.hs:37:11: error:
     • Illegal type synonym family application ‘F a’ in instance:
         C (F a z)
     • In the quantified constraint ‘forall z. C (F a z)’
       In the type signature:
         fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a
 b))
    |
 37 | fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b))
    |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}
 You sneak around that by hiding it under a superclass.   I'm not sure how
 to stop you doing that :-).

 But this succeeds:
 {{{
 fails3 :: (F a ~ fa, forall z. C (fa z)) => Proxy (a, b) -> Dict (C (F a
 b))
 fails3 _ = Dict
 }}}
 Alas, I don't see how to use the same trick for `CF`, with its superclass.

 In other tickets we have wondered if this kind of floating could happen
 automatically.  I argued "no" because it's subtle and you can do it
 manually.  But with your superclass thing you can't do it manually (I
 thihik.  So maybe that's an argument in favour.

 Hmm.  Maybe we could elaboarate the matching process.  Usually we match
 {{{
   template:   forall a b.  [a] -> b
   target:     [(Int,Bool)] -> Char
 }}}
 and produce a substitution
 {{{
   a :-> (Int,Bool)
   b :-> Char
 }}}
 such that applying the substitution to the template yields the target.

 But we could instead additionally produce a list of wanted equalities, and
 treat a type-family application as a wildcard, something like this:
 {{{
   template:  forall a.  F a -> a -> Int
   target:    Char -> [Bool] -> Int
 }}}
 then we succeed in matching, thus:
 {{{
   Substitution:  a :-> Int
   Wanted equalities:  F a ~ [Bool]
 }}}
 I don't think this would be terribly useful at top level, but in these
 quantified constraints it really might be.

 Interesting.

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