[GHC] #16252: QuantifiedConstraints: lack of inference really is a problem

[GHC]

#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