Prioritise equalities when solving, incl deriveds

We already prioritise equalities when solving, but
Trac #14723 showed that we were not doing so consistently
enough, and as a result the type checker could go into a loop.
Yikes.

See Note [Prioritise equalities] in TcSMonad.

Fixng this bug changed the solve order enough to demonstrate
a problem with fundeps: Trac #14745.

compiler/typecheck/TcSMonad.hs

@@ -189,16 +189,41 @@ Notice that each Ct now has a simplification depth. We may
 consider using this depth for prioritization as well in the future.
 
 As a simple form of priority queue, our worklist separates out
-equalities (wl_eqs) from the rest of the canonical constraints,
-so that it's easier to deal with them first, but the separation
-is not strictly necessary. Notice that non-canonical constraints
-are also parts of the worklist.
 
-Note [Process derived items last]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We can often solve all goals without processing *any* derived constraints.
-The derived constraints are just there to help us if we get stuck.  So
-we keep them in a separate list.
+* equalities (wl_eqs); see Note [Prioritise equalities]
+* non-equality deriveds (wl_derivs); see Note [Process derived items last]
+
+Note [Prioritise equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's very important to process equalities /first/:
+
+* (Efficiency)  The general reason to do so is that if we process a
+  class constraint first, we may end up putting it into the inert set
+  and then kicking it out later.  That's extra work compared to just
+  doing the equality first.
+
+* (Derived equalities) Notwithstanding Note [Process derived items
+  last], we want to process /Derived/ equalities eagerly, for the
+  (Efficiency) reason above.
+
+* (Avoiding fundep iteration) As Trac #14723 showed, it's possible to
+  get non-termination if we
+      - Emit the Derived fundep equalities for a class constraint,
+        generating some fresh unification variables.
+      - That leads to some unification
+      - Which kicks out the class constraint
+      - Which isn't solved (because there are still some more Derived
+        equalities in the work-list), but generates yet more fundeps
+  Solution: prioritise derived equalities over class constraints
+
+* (Class equalities) We need to prioritise equalities even if they are
+  hidden inside a class constraint; see Note [Prioritise class
+  equalities]
+
+* (Kick-out) We want to apply this priority scheme to kicked-out
+  constraints too (see the call to extendWorkListCt in kick_out_rewritable
+  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
+  homo-kinded when kicked out, and hence we want to priotitise it.
 
 Note [Prioritise class equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -216,20 +241,32 @@ So we arrange to put these particular class constraints in the wl_eqs.
   NB: since we do not currently apply the substitution to the
   inert_solved_dicts, the knot-tying still seems a bit fragile.
   But this makes it better.
+
+Note [Process derived items last]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We can often solve all goals without processing *any* derived constraints.
+The derived constraints are just there to help us if we get stuck.  So
+we keep them in a separate list.
+
 -}
 
 -- See Note [WorkList priorities]
 data WorkList
-  = WL { wl_eqs     :: [Ct]  -- Both equality constraints and their
-                             -- class-level variants (a~b) and (a~~b);
-                             -- See Note [Prioritise class equalities]
+  = WL { wl_eqs     :: [Ct]  -- CTyEqCan, CDictCan, CIrredCan
+                             -- Given, Wanted, and Derived
+                       -- Contains both equality constraints and their
+                       -- class-level variants (a~b) and (a~~b);
+                       -- See Note [Prioritise equalities]
+                       -- See Note [Prioritise class equalities]
 
-       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
+       , wl_funeqs  :: [Ct]
 
        , wl_rest    :: [Ct]
 
-       , wl_deriv   :: [CtEvidence]  -- Implicitly non-canonical
-                                     -- See Note [Process derived items last]
+       , wl_deriv   :: [CtEvidence]
+                       -- Implicitly non-canonical
+                       -- No equalities in here (they are in wl_eqs)
+                       -- See Note [Process derived items last]
 
        , wl_implics :: Bag Implication  -- See Note [Residual implications]
     }
@@ -321,6 +358,7 @@ emptyWorkList = WL { wl_eqs  = [], wl_rest = []
                    , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag }
 
 selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
+-- See Note [Prioritise equalities]
 selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs
                       , wl_rest = rest })
   | ct:cts <- eqs  = Just (ct, wl { wl_eqs    = cts })
@@ -338,6 +376,9 @@ selectDerivedWorkItem wl@(WL { wl_deriv = ders })
   | otherwise      = Nothing
 
 selectNextWorkItem :: TcS (Maybe Ct)
+-- Pick which work item to do next
+-- See Note [Prioritise equalities]
+-- See Note [Process derived items last]
 selectNextWorkItem
   = do { wl_var <- getTcSWorkListRef
        ; wl <- wrapTcS (TcM.readTcRef wl_var)
@@ -648,7 +689,7 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               -- Number of Wanted goals in
               --     inert_eqs, inert_dicts, inert_safehask, inert_irreds
               -- Does not include insolubles
-              -- When non-zero, keep trying to solved
+              -- When non-zero, keep trying to solve
        }
 
 type InertEqs    = DTyVarEnv EqualCtList
@@ -1522,11 +1563,17 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                        , inert_irreds   = irs_in
                        , inert_count    = n - workListWantedCount kicked_out }
 
-    kicked_out = WL { wl_eqs     = tv_eqs_out
-                    , wl_funeqs  = feqs_out
-                    , wl_deriv   = []
-                    , wl_rest    = bagToList (dicts_out `andCts` irs_out)
-                    , wl_implics = emptyBag }
+    kicked_out :: WorkList
+    -- NB: use extendWorkList to ensure that kicked-out equalities get priority
+    -- See Note [Prioritise equality constraints] (Kick-out).
+    -- The irreds may include non-canonical (hetero-kinded) equality
+    -- constraints, which perhaps may have become soluble after new_tv
+    -- is substituted; ditto the dictionaries, which may include (a~b)
+    -- or (a~~b) constraints.
+    kicked_out = foldrBag extendWorkListCt
+                          (emptyWorkList { wl_eqs    = tv_eqs_out
+                                         , wl_funeqs = feqs_out })
+                          (dicts_out `andCts` irs_out)
 
     (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
     (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_ct funeqmap
@@ -3158,7 +3205,9 @@ emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
 emitNewDerivedEq loc role ty1 ty2
   = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
        ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
-       ; updWorkListTcS (extendWorkListDerived loc ev) }
+       ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
+         -- Very important: put in the wl_eqs, /not/ wl_derivs
+         -- See Note [Prioritise equalities] (Avoiding fundep iteration)
 
 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
 newDerivedNC loc pred

testsuite/tests/polykinds/T14723.hs

+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14723 () where
+
+import Data.Coerce( coerce )
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import Data.String (fromString)
+import Data.Int (Int64)
+import GHC.Stack (HasCallStack)
+import GHC.TypeLits (Nat, Symbol)
+
+data JType = Iface Symbol
+
+data J (a :: JType)
+
+newIterator
+  :: IO (J ('Iface "java.util.Iterator"))
+newIterator = do
+    let tblPtr :: Int64
+        tblPtr = undefined
+    iterator <-
+         (qqMarker (Proxy :: Proxy "wuggle")
+                   (Proxy :: Proxy "waggle")
+                   (Proxy :: Proxy "tblPtr")
+                   (Proxy :: Proxy 106)
+                   (tblPtr, ())
+                   Proxy
+                   (undefined :: IO Int))
+    undefined
+
+class Coercible (a :: Type) where
+  type Ty a :: JType
+
+instance Coercible Int64 where
+  type Ty Int64 = Iface "Int64"
+instance Coercible Int where
+  type Ty Int = Iface "Int"
+
+class Coercibles xs (tys :: k) | xs -> tys
+instance Coercibles () ()
+instance (ty ~ Ty x, Coercible x, Coercibles xs tys) => Coercibles (x, xs) '(ty, tys)
+
+qqMarker
+  :: forall
+     -- k                -- the kind variable shows up in Core
+     (args_tys :: k)     -- JType's of arguments
+     tyres               -- JType of result
+     (input :: Symbol)   -- input string of the quasiquoter
+     (mname :: Symbol)   -- name of the method to generate
+     (antiqs :: Symbol)  -- antiquoted variables as a comma-separated list
+     (line :: Nat)       -- line number of the quasiquotation
+     args_tuple          -- uncoerced argument types
+     b.                  -- uncoerced result type
+     (tyres ~ Ty b, Coercibles args_tuple args_tys, Coercible b, HasCallStack)
+  => Proxy input
+  -> Proxy mname
+  -> Proxy antiqs
+  -> Proxy line
+  -> args_tuple
+  -> Proxy args_tys
+  -> IO b
+  -> IO b
+qqMarker = undefined

testsuite/tests/polykinds/all.T

@@ -183,4 +183,5 @@ test('T14563', normal, compile_fail, [''])
 test('T14561', normal, compile_fail, [''])
 test('T14580', normal, compile_fail, [''])
 test('T14515', normal, compile, [''])
+test('T14723', normal, compile, [''])
 

testsuite/tests/typecheck/should_compile/T13651.hs

@@ -12,3 +12,24 @@ foo :: (F cr cu ~ Bar h (Bar r u),
         F cu cs ~ Bar (Foo h) (Bar u s))
     => Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
 foo = undefined
+
+{-  Typechecking this program used to /just/ succeed in GHC 8.2,
+    (see Trac #14745 for why), but doesn't in 8.4.
+
+[G]  F cr cu ~ Bar h (Bar r u),
+     F cu cs ~ Bar (Foo h) (Bar u s))
+
+
+[W] F cr cu0 ~ Bar h (Bar r u)
+    --> (top-level fundeps)  cr ~ Bar h (Foo r)
+                             cu0 ~ Bar h (Foo u)
+        (local fundeps)      cu ~ cu0
+
+[W] F cu0 cs ~ Bar (Foo h) (Bar u s)
+    -->  (top-level fundeps)  cu0 ~ Bar (Foo h) (Foo u)
+                              cs  ~ Bar (Foo h) (Foo s)
+         (local fundeps)      cu0 ~ cu
+
+[W] F cr (Bar (Foo h) (Fo u)) ~ Bar h (Bar r u)
+
+-}

testsuite/tests/typecheck/should_compile/T13651.stderr

+
+T13651.hs:11:8: error:
+    • Could not deduce: F cr (Bar (Foo h) (Foo u)) ~ Bar h (Bar r u)
+      from the context: (F cr cu ~ Bar h (Bar r u),
+                         F cu cs ~ Bar (Foo h) (Bar u s))
+        bound by the type signature for:
+                   foo :: forall cr cu h r u cs s.
+                          (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
+                          Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
+        at T13651.hs:(11,8)-(13,65)
+    • In the ambiguity check for ‘foo’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        foo :: (F cr cu ~ Bar h (Bar r u),
+                F cu cs ~ Bar (Foo h) (Bar u s)) =>
+               Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)

testsuite/tests/typecheck/should_compile/T13651a.hs

+{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
+module T13651 where
+
+type family F r s = f | f -> r s
+
+type instance F (Bar h (Foo r)) (Bar h (Foo s)) = Bar h (Bar r s)
+
+data Bar s b
+data Foo a
+
+foo :: (F cr cu ~ Bar h (Bar r u),
+        F cu cs ~ Bar (Foo h) (Bar u s))
+    => Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> cu -> Foo (cr -> cs)
+    -- A variant of T13651 which fixes 'cu'
+    -- as well as the other type args
+foo = undefined

testsuite/tests/typecheck/should_compile/all.T

@@ -561,7 +561,8 @@ test('T13594', normal, compile_fail, [''])
 test('T13603', normal, compile, [''])
 test('T13333', normal, compile, [''])
 test('T13585', [extra_files(['T13585.hs', 'T13585a.hs', 'T13585b.hs'])], run_command, ['$MAKE -s --no-print-directory T13585'])
-test('T13651', normal, compile, [''])
+test('T13651', normal, compile_fail, [''])
+test('T13651a', normal, compile, [''])
 test('T13680', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])