#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