[GHC] #15359: Quantified constraints do not work with equality constraints
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Feeling abusive toward GHC this morning, I tried this: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:1 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 `~`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) Comment: Redundant in what sense? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:6 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 [https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html 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) }}} (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 ... }}} 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:8 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:8 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 ...) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:11 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)? 2. In the 'FDs through CHRs' paper all of the improvement rules are in the form of a constraint implying an equality. 3. 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.
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
There's a risk of non-termination. But GHC entertains that already with `UndecidableInstances` and/or `UndecidableSuperClasses`. I think we could work up [https://github.com/ghc-proposals/ghc-proposals/pull/114 a proposal for that]. In the language of the 'FDs through CHRs' paper, we must make sure all quantification is 'range restricted'. these. Isn't "many ways" actually a problem here? Too many similar-but-subtly- different ways. And specifically Type Families are out of favour [https://github.com/ghc-proposals/ghc- proposals/pull/114#issuecomment-372124549 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
the last two instance always overlap looking only at the instance
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:11 goldfire]: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. * It keeps coming up: #15625 and #15593 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15359: Quantified constraints do not work with equality constraints
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| QuantifiedConstraints
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => quantified-constraints/T15359,T15359a * resolution: => fixed Comment: 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC