#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