diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-01-31 13:05:13 +0000 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2018-01-31 22:12:46 -0500 |
commit | 77cdf60c8a68d2208cd8109d82b5f83b17bf0e91 (patch) | |
tree | d930a6139531808c2796bda898feda3dc7c4958a | |
parent | e6c147442fbeb161bbed209126186056f371d60c (diff) | |
download | haskell-77cdf60c8a68d2208cd8109d82b5f83b17bf0e91.tar.gz |
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 efba054640d3418d7477316ae0c1e992d0aa0f22)
-rw-r--r-- | compiler/typecheck/TcSMonad.hs | 93 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T14723.hs | 70 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T13651.hs | 21 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T13651.stderr | 16 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T13651a.hs | 16 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 3 |
7 files changed, 197 insertions, 23 deletions
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index b58ac06633..1ccbd79476 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -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 diff --git a/testsuite/tests/polykinds/T14723.hs b/testsuite/tests/polykinds/T14723.hs new file mode 100644 index 0000000000..9b2f3bf75e --- /dev/null +++ b/testsuite/tests/polykinds/T14723.hs @@ -0,0 +1,70 @@ +{-# 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 diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 75f85a337b..f101865527 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -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, ['']) diff --git a/testsuite/tests/typecheck/should_compile/T13651.hs b/testsuite/tests/typecheck/should_compile/T13651.hs index 43ae633534..63bd88eb5c 100644 --- a/testsuite/tests/typecheck/should_compile/T13651.hs +++ b/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) + +-} diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr new file mode 100644 index 0000000000..6b6c64302f --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T13651.stderr @@ -0,0 +1,16 @@ + +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) diff --git a/testsuite/tests/typecheck/should_compile/T13651a.hs b/testsuite/tests/typecheck/should_compile/T13651a.hs new file mode 100644 index 0000000000..482231b6f2 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T13651a.hs @@ -0,0 +1,16 @@ +{-# 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 diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 50592b307c..fd05c20f21 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -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, ['']) |