[GHC] #15409: Quantified constraints half-work with equality constraints

[GHC]

#15409: Quantified constraints half-work with equality constraints
-------------------------------------+-------------------------------------
           Reporter:  AntC           |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Windows
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  15359
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Experimenting from the comments in ticket:15359 ... This is using
 8.6.0.alpha2 20180714

 {{{
 {-# LANGUAGE QuantifiedConstraints                       #-}
              -- plus the usual suspects

 -- And over type-level Booleans

 class ((c ~ 'True) => (a ~ 'True),                 -- Surprise 1
        (c ~ 'True) => (b ~ 'True))
       => And' (a :: Bool) (b :: Bool) (c :: Bool)  | a b -> c

 instance ()                                        -- Surprise 2
          => And' 'True b b
 instance (('False ~ 'True) => (b ~ 'True))         -- Surprise 3
          => And' 'False b 'False

 y :: (And' a b 'True) => ()                        -- Surprise 4
 y = ()

 }}}

 1. Those superclass constraints are accepted, with equalities in the
 implications.

 2. The `And 'True b b` instance is accepted without needing further
 constraints.
    ?So GHC can figure the implications hold from looking at the instance
 head.

 3. For the `And' 'False b 'False` instance, GHC can't figure the `(c ~
 'True) => (b ~ 'True)` superclass constraint holds.
    Just substituting into the implication from the instance head seems to
 satisfy it.
    So now we have a never-satisfiable antecedent.
    Rejection message if instance constraints omitted is

 {{{
     * Could not deduce: b ~ 'True
         arising from the superclasses of an instance declaration
       from the context: 'False ~ 'True
         bound by a quantified context at ...
 }}}

 4. The signature for `y` is rejected `Could not deduce (And' a0 b0
 'True)`.
    (The message suggests `AllowAmbiguousTypes`, but that just postpones
 the error.)

 I was hoping the superclass constraints would spot that `c ~ 'True` and
 improve `a, b` from the implications.

 5. No surprise that replacing all the `(~)` with `Coercible` produces the
 same rejections.

 6. I did try putting the whole `And` logic in a class without FunDeps.
 This was accepted:

 {{{
 class (( a ~ 'True)  => (b ~ c),
        ( a ~ 'False) => (c ~ 'False),
        ( c ~ 'True)  => (a ~ 'True),
        ( c ~ 'True)  => (b ~ 'True)   )
       => And3 (a :: Bool) (b :: Bool) (c :: Bool)    -- no FunDep

 }}}

    But attempts to write instances and or/use the class evinced only a
 torrent of obscure messages, including

 {{{
     * Overlapping instances for b ~ 'True
         arising from the superclasses of an instance declaration
       Matching givens (or their superclasses):
         c ~ 'True
           bound by a quantified context at ...
       Matching instances:
         instance [incoherent] forall k (a :: k) (b :: k). (a ~ b) => a ~ b
           -- Defined in `Data.Type.Equality'
 }}}

    So GHC is creating instances for `(~)` on the fly?

    (I can supply more details if that would help.)

 Chiefly I'm thinking that if allowing `(~)` in `QuantifiedConstraints` is
 only teasing and never effective, there should be a clear rejection
 message.

 ''pace'' Simon's comments, I don't see any of those `(~)` implications for
 `And` as "useless" or "redundant".

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