[GHC] #14723: GHC 8.4.1-alpha loops infinitely when typechecking

[GHC]

#14723: GHC 8.4.1-alpha loops infinitely when typechecking
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.4.1-alpha1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  performance bug                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here's a diagnosis.  We have

 {{{
   class Coercibles k k1 (xs :: k) (tys :: k1) | xs -> tys

   instance forall k (ty :: JType) x xs (tys :: k).
            (ty ~ Ty x, Coercible x, Coercibles * k xs tys) =>
            Coercibles * (JType, k) (x, xs) '(ty, tys)
 }}}
 and a wanted constraint
 {{{
   [WD] $dCoercibles_a2K3 :: Coercibles *
                                        (JType, k_a2My[tau:1])
                                        (Int64, ())
                                        args_tys_a2JU[tau:1]
 where
   args_tys_a2JU :: (JType, kappa1)
 }}}
 Now, from the fundep `xs -> tys` we generate
 {{{
   [D] arg_tys_a2JU ~ (ty::JType, tys::kappa2)
 }}}
 where `ty`, `tys`, and `kappa2` are all ''fresh unification variables''.
 They are fresh because they they are not directly fixed by `(x,xs)` in
 the instance decl, but only indirectly via the context of the instance
 decl (so-called "liberal" fundeps).  This is legitimate.

 But this new derived equality is hetero-kinded, so we "park" it (as a
 `CIrredCan`) and
 emit a derived equality on the kinds
 {{{
   [D] (JType, kappa1) ~ (JType, kappa2)
 }}}
 We solve this, by `kappa1 := kappa2`.   That kicks out the two inert,
 unsolved constraints, both of which mention `kappa1`:
 {{{
   [WD] $dCoercibles_a2K3 :: Coercibles *
                                        (JType, k_a2My[tau:1])
                                        (Int64, ())
                                        args_tys_a2JU[tau:1]
   [D] arg_tys_a2JU ~ (ty::JType, tys::kappa2)
 }}}
 Alas, we choose the ''former'' to solve; and that simply repeats the
 entire
 process from the beginning.

 If instead we chose the derived equality constraint, the `kappa1 :=
 kappa2`
 would make the equality homo-kinded, so we'd solve with `args_tys_a2JU :=
 (ty,tys)`;
 and now the `Coercibles` constraint matches the instance and can be
 solved.

 And even if the `Coercibles` constraint doesn't (yet) match an instance,
 (maybe there's another parameter to the class that prevents the match)
 provided we've processed all the equalities coming from the fundeps first,
 we'll find that, if we generate fundeps again, they are all no-ops.

 Bottom line: one fix would be to prioritise equality constraints, even
 if they are Derived.  Currently we priorities Wanted constraints in
 the work-list over Derived, on the grounds that if we solve all the
 Wanted constraints we may never need to process those Derived ones at
 all.

 Another (possibly better) approach might be to remember when we have
 generated fundeps from a class constraint, and refrain from doing so a
 second time.  But that seems hard, because as we rewrite the class
 constraint we may learn more about some of its arguments, and therefore
 expose more possible fundeps.  So it's hard to say when we "have generated
 the fundeps" from a class constraint.

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