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 |