Type inference non-determinism due to improvement

Here's an example that showed up in Iavor's test TcTypeNatSimple:

  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)

where alpha is the unification variable that instantiates x.

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.

Trac metadata

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