#16252: QuantifiedConstraints: lack of inference really is a problem -------------------------------------+------------------------------------- Reporter: lightandlight | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I've been debugging an issue that boils down to: quantified constraints are completely ignored during type inference. For example, in this program: {{{#!hs {-# language QuantifiedConstraints #-} module QC where data A f = A (f Int) eqA :: forall f. (forall x. Eq x => Eq (f x)) => A f -> A f -> Bool eqA (A a) (A b) = a == b eqA' :: (forall x. Eq x => Eq (f x)) => A f -> A f -> Bool eqA' = let g = eqA in g }}} `eqA'` won't compile because `g` gets generalised to `forall f. A f -> A f -> Bool`. I know this has been discussed (and dismissed) in tickets such as #2256 and #14942, but I really think it's a problem. In my example, I can get the code compiling by turning on ScopedTypeVariables and giving `g` an annotation. But I don't always have this liberty. For example, in the `deriving-compat` library there's Template Haskell that generates definitions containing `let`s, and when a quantified constraint is present these splices don't type check for the same reason `eqA'` doesn't. The solution here involves a pull request to `deriving-compat` that uses ScopedTypeVariables to annotate the problematic `let`s. But I really think that none of this should be necessary. The reference implementation of QCs (https://github.com/gkaracha/quantcs-impl) doesn't seem to have this problem. Is there anything I'm missing? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16252 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler