QuantifiedConstraints: lack of inference really is a problem

I've been debugging an issue that boils down to: quantified constraints are completely ignored during type inference.

For example, in this program:

{-# 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 (closed) and #14942 (closed), 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 lets, 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 lets.

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?

Trac metadata

Trac field	Value
Version	8.6.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture