Type inference non-determinism due to improvement
Here's an example that showed up in Iavor's test
ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> () ti7 _ _ = ()
From the ambiguity check for
ti7 we get this constraint
forall x y. (x <= y, y <= x) => ( SomeFun x ~ SomeFun alpha , alpha <= y, y <= alpha)
alpha is the unification variable that instantiates
Now, from the givens, improvement gives a derived
[D] x~y, but we can't actually use that to rewrite anything; we have no evidence.
From the wanteds we can use improvement in two alternative ways:
1. (alpha <= y, y <= alpha) => [D] alpha ~ y 2. (x <= y, y <= alpha) => [D] x <= alpha (alpha <= y, y <= x) => [D] alpha <= x And combining the latter two we get [D] (alpha ~ x)
It is (2) that we want. But if we get (1) and fix
alpha := y, we get an error
Can't unify (SomeFun x ~ SomeFun y).
I think it's a fluke that this test has been working so far; in my new flatten-skolem work it has started failing, which is not unreasonable. What I HATE is that whether type checking succeeds or fails depends on some random choice about which constraint is processed first.
The real bug is that the derived Given has no evidence, and can't be used for rewriting. I think Iavor is fixing this deficiency for. I speculate that the same problem might also show up with ordinary type-class functional dependencies, but I have not found a concrete example.