Commit 77cdf60c authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

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.

(cherry picked from commit efba0546)
parent e6c14744
......@@ -188,16 +188,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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -215,20 +240,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]
}
......@@ -320,6 +357,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 })
......@@ -337,6 +375,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)
......@@ -643,7 +684,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
......@@ -1517,11 +1558,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
......@@ -3146,7 +3193,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
......
{-# 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
......@@ -177,4 +177,5 @@ test('T14450', normal, compile_fail, [''])
test('T11203', normal, compile_fail, [''])
test('T14555', normal, compile_fail, [''])
test('T14563', normal, compile_fail, [''])
test('T14723', normal, compile, [''])
......@@ -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)
-}
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)
{-# 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
......@@ -560,7 +560,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, [''])
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment