Quantified constraints half-work with equality constraints

Experimenting from the comments in #15359 (closed) ... 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.

1. 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 ...

1. 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.

1. No surprise that replacing all the (~) with Coercible produces the same rejections.
2. 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".

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Windows
Architecture