Opened 14 months ago

Last modified 9 months ago

#15409 new bug

Quantified constraints half-work with equality constraints

Reported by: AntC Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.4.3
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: 15359 Differential Rev(s):
Wiki Page:

Description

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

Change History (3)

comment:1 Changed 14 months ago by Phyx-

Operating System: WindowsUnknown/Multiple

comment:2 Changed 14 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:3 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.