## 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 `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?

## 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 |