[GHC] #9708: Type inference non-determinism due to improvement

[GHC]

#9708: Type inference non-determinism due to improvement
-------------------------------------+-------------------------------------
       Reporter:  simonpj            |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler           |                 Version:  7.8.3
       Keywords:                     |        Operating System:
   Architecture:  Unknown/Multiple   |  Unknown/Multiple
     Difficulty:  Unknown            |         Type of failure:
     Blocked By:                     |  None/Unknown
Related Tickets:                     |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9708>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler