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

changed weight to 5

added Tbug Trac import labels

Interesting! I can see what is happening.

Given a binding g = rhs, GHC infers all the constraints C from rhs and tries to generalise. Currently that works as follows (simplifyInfer)

1. approximateWC: find quant_pred_candidates, the subset of constraints in C over which we could conceivably quantify.
2. Pick a set of quant_pred_candidates to quantify over
3. Crucially, do not generalise over any type variable free in a constraint we decide not to generalise in Step 2. (If we generalise over that type variable, the constraint will probably become insoluble.)

The problem is that we don't account for constraints (such as implication constraints) that Step 1 discards! We do generalise over their type variables, and they duly become insoluble. That's why your definition of g is being generalised.

Solution: don't generalise over any type variable free in a constraint that we can't quantify.

I'm quite surprised this has not come up before. The fix will be a big fiddly but not really hard.

What does it mean to 'quantify over a constraint' here?

Okay, I've thought about this for a little bit:

Why shouldn't the implication constraint be considered part of quant_pred_candidates? It seems to me that the error is in discarding it as a candidate in the first place. In other words, I would expect g's inferred type to be (forall x. Eq x => Eq (f x)) => A f -> A f -> Bool.

I've tried to implement the advice as described: excluding variables from generalisation when they appear in un-quantifiable constraints (collecting said variables in approximateWC, and removing them from qtvs in simplifyInfer). I now have an escaped skolem error.

I think this is the relevant portion of the trace:

  {f1_a26[sk:1], f_a2c[sk:2]}
  g_ah :: forall (a :: (* -> *) -> *).
          a f_a2c[sk:2] -> a f_a2c[sk:2] -> Bool,
  eqA'_a28 :: a_a27[sk:1] f_a26[sk:1]
              -> a_a27[sk:1] f_a26[sk:1] -> Bool,
  eqA :: forall (f :: * -> *) (a :: (* -> *) -> *).
         (forall x. Eq x => Eq (f x)) =>
         a f -> a f -> Bool,

Is it likely that I've forgotten some important call?

Why shouldn't the implication constraint be considered part of quant_pred_candidates?

It's always sound to quantify over any constraints you can't solve. But in many cases that'll simply push type errors from the definition site to the call site of the function. There are many constraints we don't quantify over as you'll see in pickQuantifiableConstraints.

I think it's better (more explicit, more comprehensible) just to provide a type signature.

Okay. Do you have any advice regarding my current issue?

added Pnormal label

added type inference label