#15359 closed bug (fixed)

Quantified constraints do not work with equality constraints

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc: dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: quantified-constraints/T15359,T15359a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Feeling abusive toward GHC this morning, I tried this:

class C a b

data Dict c where
  Dict :: c => Dict c

foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
foo Dict x = x

I thought it wouldn't work, and I was right:

    • Class ‘~’ does not support user-specified instances
    • In the quantified constraint ‘forall (a :: k) (b :: k).
                                    C a b =>
                                    a ~ b’
      In the type signature:
        foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b

Good. But then I tried something more devious:

class C a b
class a ~ b => D a b

data Dict c where
  Dict :: c => Dict c

foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
foo Dict x = x

This also fails, with Couldn't match expected type ‘b’ with actual type ‘a’.

I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason -- like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.

Change History (17)

comment:1 Changed 14 months ago by RyanGlScott

It's very strange to me that we allow quantified Coercible constraints but not quantified (~) constraints. What is the rationale behind this decision choice?

comment:2 Changed 14 months ago by goldfire

Oh dear. I see trouble a-brewing.

I agree that Coercible and ~ should either both be allowed or both be rejected. But the implications in my OP are unimplementable, I think. So I'm lost as to how to specify this.

comment:3 in reply to:  1 Changed 14 months ago by AntC

Replying to RyanGlScott:

It's very strange to me that we allow quantified Coercible constraints but not quantified (~) constraints. What is the rationale behind this decision choice?

Yes, I'm gravely disappointed to learn that: I've been posting lots of suggestions using ~ inside quantified (implication) constraints.

    • Class ‘~’ does not support user-specified instances

Before there was ~, there were plenty of ways for a user to specify a unifiability constraint -- see for example TypeCast in the HList paper. (Using bi-directional FunDeps.) And other examples of Quantified Constraints are using FunDeps for type improvement. So just do that instead of ~?

comment:4 Changed 14 months ago by goldfire

Simon and I discussed this today. The lack of symmetry between Coercible and ~ here is by design. Essentially, any equality implication constraint is guaranteed to be redundant, because GHC can already deduce all equalities from whatever assumptions are at hand. On the other hand, Coercible implication constraints are quite useful, because coercibility is fundamentally incomplete.

So the trouble I saw isn't so bad. But I still think we should document the restriction and report a better error message here.

comment:5 Changed 14 months ago by dfeuer

Cc: dfeuer added

Redundant in what sense?

comment:6 Changed 14 months ago by simonpj

Redundant in what sense?

Well, can you show me a quantified constraint with an equality in the head that is not useless?

For example what about this (by analogy with Coercible)

f :: forall m.
     (forall a b. a ~ b => m a ~ m b)
   => blah

No, that redundant. If we have [W] t1 a ~ t2 b there is a built-in rule to decompose it to [W] t1 ~ t2 and [W] a ~ b. (There is no such rule in general for Coercible which is why we need to allow it.) So that quantified constraint wasn't useful.

Can you think of one that is? I can't.

comment:7 in reply to:  6 Changed 14 months ago by AntC

Replying to simonpj:

Well, can you show me a quantified constraint with an equality in the head that is not useless?

Remembering that this extension includes implication constraints, not only quantified, I can think of plenty. Here's one close to David's heart, per this message. "Reasoning backwards with type families". Suppose a class (rather than Type Family) for And over type-level Booleans: if we know the result is True, that gives an implication for the arguments:

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

(And further implications would apply, per David's message. So this is a general technique for injectivity or partial/quasi-injectivity. Doesn't Richard's "fundamentally incomplete" apply here: there is not complete injectivity from result to arguments. So the implication => says: if the lhs constraint/equality holds, then you can use the rhs constraint/equality; otherwise (i.e. the lhs doesn't hold) the => holds anyway.)

Richard says

any equality implication constraint is guaranteed to be redundant, because GHC can already deduce all equalities from whatever assumptions are at hand.

For And that would need taking the instances as assumptions, plus making an assumption those are the only instances.

Whereas my reading of the papers (seems I'm wrong) is that when QuantifiedConstraints sees those superclass constraints, it will assume them for type improvement, and verify they hold for each instance decl.

Can you think of one that is? I can't.

If you want an example with quantification:

class (forall b'. C a b' => b' ~ b)
      => C a b  where ...                                  -- no FunDep

ADDIT: or even

class (forall c'. And a b c' => c' ~ c)
      => And (a :: Bool) (b :: Bool) (c :: Bool)           -- no Fundep

Which is more-or-less verbatim from the textbooks as a FOPL definition of ... a Functional Dependency -- that is, in relational database textbooks. And appears more-or-less verbatim in Mark P Jones papers on FunDeps and in the 'FDs through CHRs' paper.

I'm talking about FOPL because the hs2017 paper (opening sentence) says

"Quantified class constraints have been proposed many years ago to raise the expressive power of type classes from Horn clauses to first-order logic."

That "proposed many years ago" cites your 2000 paper (with Ralf).

ADDIT2:

class (a ~ 'True => b ~ c, a ~ 'False => c ~ 'False)
      => And (a :: Bool) (b :: Bool) (c :: Bool)           -- no Fundep

If I can avoid FunctionalDependencies, then for trickier cases where currently I need OverlappingInstances and UndecidableInstances, perhaps I can write the instances more directly without needing to dive into that swamp. In effect I'm defining the laws for the class as (quantified) iimplications.

Last edited 14 months ago by AntC (previous) (diff)

comment:8 Changed 14 months ago by goldfire

All the examples in comment:7 involve superclass constraints, mostly on classes without any methods. This is interesting for type-level programming, but it's not clear where (even in type-level programming) the rubber is hitting the road here.

Can you give a concrete example of a function that usefully uses an equality constraint in the head of an implication? This should be a function that I can call (that is, the constraints are satisfiable).

comment:9 in reply to:  8 Changed 14 months ago by AntC

Replying to goldfire: [replying in two instalments]

All the examples in comment:7 involve superclass constraints,

... because your ticket:15351#comment:5 tells me I don't even need instances declared.

mostly on classes without any methods. This is interesting for type-level programming,

Yes the And example is for type-level programming. You haven't said those superclass constraints are redundant. Those implications/equalities can be derived from examining the instances; but a) needs reasoning from Bool being a closed type, b) needs reasoning from a closed set of instances.

but it's not clear where (even in type-level programming) the rubber is hitting the road here.

I don't expect GHC to be a general-purpose logic engine, so if we want type improvement per David's ghc-devs message "Reasoning backwards" -- which seem eminently sensible, and improvements not achievable by injective Type Families (yet), why can't I use QuantifiedConstraints superclass? I could use similar for "Reasoning backwards" in type-level arithmetic over Nat: if a sum is Z, both arguments must be Z.

As I said in comment:3, if it can't use ~, there's plenty of ways to user-define an equivalent.

comment:10 in reply to:  8 Changed 14 months ago by AntC

Replying to goldfire: [2 of 2]

Considering using quantified implications to emulate FunDeps -- because FunDeps are quantified implications.

it's not clear where ... the rubber is hitting the road here.

Seeing the analogy between type improvement/multi-param type classes and relational theory was a great insight. But FunDeps is a clumsy mechanism. FunDeps and OverlappingInstances do not live happily together -- as all the theory says (and often need UndecidableInstances). FunDeps and superclass constraints calling Closed Type Families needs clunky machinery to concoct a CTF, give equations disconnected from the class, and still you're liable to need instances that look to GHC like they're overlapping.

Then taking the hs2017 paper's "raise expressive power ... to first-order logic":

  • Superclass constraints with implications express more precisely the logic of the class.
  • Without an explicit FunDep, we avoid the 'FunDep consistency check', which is onerous and imprecise; and
  • anyway GHC's implementation is bogus -- as it needs to be, because FunDeps are imprecise.
  • Sometimes we can avoid UndecidableInstances or at least write instances that are less cluttered.

Can you give a concrete example of a function that usefully uses an equality constraint in the head of an implication? This should be a function that I can call (that is, the constraints are satisfiable).

The class C above is emulating a regular FunDep; no reason it couldn't have methods. Here's something more ambitious (a classic litmus test of expressivity):

data HNil = HNil;    data HCons e l = HCons e l

-- method to eliminate element 'e' from a heterogeneous list 'l'

class ElimElem e l l'''  | e l -> l'''  where   -- here's the classic definition, with FunDep and overlaps
  elimElem :: e -> l -> l'''                    -- because overlaps, I can't use an Associated Type in the class

instance ElimElem e HNil HNil  where
  elimElem _ HNil = HNil
instance {-# OVERLAPPING #-} (ElimElem e l' l''')
         => ElimElem e (HCons e l') l''' where
  elimElem _x (HCons _ l') = elimElem _x l'

-- instance (ElimElem e l' l''') => ElimElem e (HCons e' l') (HCons e' l''') where
                                                -- wrong! instance head not strictly more general

instance (ElimElem e l' l'', l''' ~ HCons e' ''')
         => ElimElem e (HCons e' l') l''' where
  elimElem _x (HCons y l') = HCons y (elimElem _x l')

I'd like to write that without FunDeps -- then can I use implications?

class (l ~ HNil => l''' ~ HNil,
       ( forall l'. l ~ HCons e l' => (ElimElem e l' l'''),
       ( forall e' l'. (l ~ HCons e' l', e /~ e') => (ElimElem e l' l'', l''' ~ HCons e' l'') )
      => ElimElem e l' l'''  where               -- no FunDep
        elimElem :: e -> l -> l'''

-- HNil and HCons matching instances as above, but no OVERLAPPING

instance (ElimElem e l' l'')
         => ElimElem e (HCons e' l') (HCons e' l'')  where
  elimElem _x (HCons y l') = HCons y (elimElem _x l')

Yes the two HCons instances might theoretically overlap (looking only at the instance heads) -- so again I can't use an Associated TF; but we never call elimElem at the intersection type, thanks to the type improvement applied from the superclass constraints. (I'd still prefer to make that explicit with an Apartness Guard ...)

comment:11 Changed 14 months ago by goldfire

As you point out, the last two instance always overlap looking only at the instance heads. So I think you'd still need {-# OVERLAPPING #-}.

Previously, Simon was worried that the equality constraints would always be redundant. I think that's still true in your examples, but with a key twist: the equality constraints can be used for improvement during type checking. That may indeed be correct.

As a practical matter though, I can't imagine how to implement them. And, given the fact that we have many ways of expressing these ideas already, without quantified equality constraints, (for example, your ElimElem could be implemented as a closed type family), I'm not yet motivated to start thinking about how to write a solver than can deal with these.

comment:12 in reply to:  11 Changed 14 months ago by AntC

Replying to goldfire:

... I neither know a good pithy way of explaining that

I can't see even a convoluted explanation: it seems an arbitrary restriction. (Perhaps Simon is just being conservative with a new feature?)

  1. Why is ~ banned, but not Coercible (or a user-written coercion class)?
  1. In the 'FDs through CHRs' paper all of the improvement rules are in the form of a constraint implying an equality.
  1. Richard's suggestion of a Closed Type Family (in a ~ superclass constraint -- which is a standard idiom) just is exactly what seems to be banned:
class (F a b ~ c)              -- there's the Eq constraint
      => D a b c  where ...

type family F a b  where
  F blah1 blah2 = blah3        -- take '=' from left to right, so it's an implication
  F a (T a b')  = (... b' ...) -- repeated tyvars on lhs is an '~' test
                               -- local-scoped tyvar b' is quantified

"just is"? Well, no: I've had to chop up the logic and find a name for it and spread it round the program text.

Previously, Simon was worried that the equality constraints would always be redundant.

Hmm. Maybe redundant in the sense if you draw all the bits back together, the type equalities are entailed. But in the general case (such as my And example) that needs closed-world reasoning: closed Kinds; closed sets of instances. Which I don't expect GHC to even try.

I think that's still true in your examples, but with a key twist: the equality constraints can be used for improvement during type checking. That may indeed be correct.

There's a risk of non-termination. But GHC entertains that already with UndecidableInstances and/or UndecidableSuperClasses. I think we could work up a proposal for that.

In the language of the 'FDs through CHRs' paper, we must make sure all quantification is 'range restricted'.

As a practical matter though, I can't imagine how to implement them. And, given the fact that we have many ways of expressing these ideas already, without quantified equality constraints, (for example, your ElimElem could be implemented as a closed type family), I'm not yet motivated to start thinking about how to write a solver than can deal with these.

Isn't "many ways" actually a problem here? Too many similar-but-subtly-different ways. And specifically Type Families are out of favour for certain purposes (see re 'lens example' -- chop up the program logic, repeat it around the program, find a name for it; I think that also swayed the decision on records/HasField class to use FunDeps rather than TFs).

Simon's (quite rightly) always looking for underpinning rationalisations that "allows us to simplify the language by (say) deprecating or removing features". Haskell has had a problem since at least 1997; didn't get fixed in H98; didn't get fixed in H2010; unlikely to get resolved for H2020: that we'd like to 'bless' MPTCs; but then we'd need to bless FunDeps and/or Type Families; but then we'd have to deal with overlaps/Closed TFs. All of them have an underlying type improvement logic, which is a 'local' implication constraint with equalities.

comment:13 in reply to:  11 Changed 14 months ago by AntC

Replying to goldfire:

the last two instance always overlap looking only at the instance heads. So I think you'd still need {-# OVERLAPPING #-}.

Yeah kinda; but no. GHC's overlap is a marvel of engineering compromise. So you're not squinting at the right angle.

  • The two instances are in no substitution order, so OVERLAPPING/OVERLAPPABLE would be rejected.
  • "It is fine for there to be a potential of overlap ...; an error is only reported if a particular constraint matches more than one." [Users guide] So I'm relying on type improvement to apply before instance selection: then GHC should never be looking for a Wanted that matches more than one instance.

comment:14 Changed 14 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:15 Changed 12 months ago by simonpj

I am repenting of my earlier claim that we should not allow (~) in the head of quantified constraints. Why

  • You can the same effect via a superclass
    class (a ~ b) => Equal a b
    
    f1 :: (forall a. blah => a ~ b) => stuff
    f2 :: (forall a. blah => Equal a b) => stuff
    
    If f1 is illegal, then f2 should be too.
  • It does seem odd to treat Coercible one way and (~) another
  • The rejection of (~) is, I think, pretty much accidental. The message comes from checkValidInstHead, in this equation
      -- For the most part we don't allow instances for Coercible;
      -- but we DO want to allow them in quantified constraints:
      --   f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
      | clas_nm == coercibleTyConName
      , not quantified_constraint
      = failWithTc rejected_class_msg
    
      -- Handwritten instances of other nonminal-equality classes
      -- is forbidden, except in the defining module to allow
      --    instance a ~~ b => a ~ b
      -- which occurs in Data.Type.Equality
      | clas_nm `elem` [ heqTyConName, eqTyConName]
      = failWithTc rejected_class_msg
    
    I'm not sure that I thought very deeply about Coercible vs (~) here.

However it's not just a question of lifting the restriction. As things stand, dictionary functions (from instance decls, or in quantified constraints) are always boxed, lifted things. But if we have

f :: (forall a. t1 ~ t2) => blah

the way superclasses work for quantifed constraints, we'll behave as if we also had (forall a. t1 ~# t2) and that is unboxed. Coercions, of type (t1 ~# t2) and (t1 ~R# t2) are handled rather separately by the constraint solver, not least because they can occur in types.

Still, I think it's not as hard as I thought.

comment:16 Changed 12 months ago by Simon Peyton Jones <simonpj@…>

In bd76875a/ghc:

Allow (~) in the head of a quantified constraints

Since the introduction of quantified constraints, GHC has rejected
a quantified constraint with (~) in the head, thus
  f :: (forall a. blah => a ~ ty) => stuff

I am frankly dubious that this is ever useful.  But /is/ necessary for
Coercible (representation equality version of (~)) and it does no harm
to allow it for (~) as well.  Plus, our users are asking for it
(Trac #15359, #15625).

It was really only excluded by accident, so
this patch lifts the restriction. See TcCanonical
Note [Equality superclasses in quantified constraints]

There are a number of wrinkles:

* If the context of the quantified constraint is empty, we
  can get trouble when we get down to unboxed equality (a ~# b)
  or (a ~R# b), as Trac #15625 showed. This is even more of
  a corner case, but it produced an outright crash, so I elaborated
  the superclass machinery in TcCanonical.makeStrictSuperClasses
  to add a void argument in this case.  See
  Note [Equality superclasses in quantified constraints]

* The restriction on (~) was in TcValidity.checkValidInstHead.
  In lifting the restriction I discovered an old special case for
  (~), namely
      | clas_nm `elem` [ heqTyConName, eqTyConName]
      , nameModule clas_nm /= this_mod
  This was (solely) to support the strange instance
      instance a ~~ b => a ~ b
  in Data.Type.Equality. But happily that is no longer
  with us, since
     commit f265008fb6f70830e7e92ce563f6d83833cef071
     Refactor (~) to reduce the suerpclass stack
  So I removed the special case.

* I found that the Core invariants on when we could have
       co = <expr>
  were entirely not written down. (Getting this wrong ws
  the proximate source of the crash in Trac #15625.  So

  - Documented them better in CoreSyn
      Note [CoreSyn type and coercion invariant],
  - Modified CoreOpt and CoreLint to match
  - Modified CoreUtils.bindNonRec to match
  - Made MkCore.mkCoreLet use bindNonRec, rather
    than duplicate its logic
  - Made Simplify.rebuildCase case-to-let respect
      Note [CoreSyn type and coercion invariant],

comment:17 Changed 12 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: quantified-constraints/T15359,T15359a

OK the examples in the Description both now work -- or at least typecheck and pass Lint.

I have not tried the more exotic stuff in the comments, but please to have a go!

Note: See TracTickets for help on using tickets.