Commit a8fde183 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix bug in the short-cut solver

Trac #13943 showed that the relatively-new short-cut solver
for class constraints (aka -fsolve-constant-dicts) was wrong.
In particular, see "Type families" under Note [Shortcut solving]
in TcInteract.

The short-cut solver recursively solves sub-goals, but it doesn't
flatten type-family applications, and as a result it erroneously
thought that C (F a) cannot possibly match (C 0), which is
simply untrue.  That led to an inifinte loop in the short-cut
solver.

The significant change is the one line

+                 , all isTyFamFree preds  -- See "Type families" in
+                                          -- Note [Shortcut solving]

but, as ever, I do some other refactoring.  (E.g. I changed the
name of the function to shortCutSolver rather than the more
generic trySolveFromInstance.)

I also made the short-cut solver respect the solver-depth limit,
so that if this happens again it won't just produce an infinite
loop.

A bit of other refactoring, notably moving isTyFamFree
from TcValidity to TcType
parent a1fc7ce3
......@@ -689,8 +689,8 @@ interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
* *
*********************************************************************************
Note [Solving from instances when interacting Dicts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Shortcut solving]
~~~~~~~~~~~~~~~~~~~~~~~
When we interact a [W] constraint with a [G] constraint that solves it, there is
a possibility that we could produce better code if instead we solved from a
top-level instance declaration (See #12791, #5835). For example:
......@@ -714,17 +714,23 @@ solution for `Num Int`. This would let us produce core like the following
eta1
A.f1
This is bad! We could do much better if we solved [W] `Num Int` directly from
the instance that we have in scope:
This is bad! We could do /much/ better if we solved [W] `Num Int` directly
from the instance that we have in scope:
f :: forall b. C Int b => b -> Int -> Int
f = \ (@ b) _ _ (x :: Int) ->
case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) }
However, there is a reason why the solver does not simply try to solve such
constraints with top-level instances. If the solver finds a relevant instance
declaration in scope, that instance may require a context that can't be solved
for. A good example of this is:
** NB: It is important to emphasize that all this is purely an optimization:
** exactly the same programs should typecheck with or without this
** procedure.
Solving fully
~~~~~~~~~~~~~
There is a reason why the solver does not simply try to solve such
constraints with top-level instances. If the solver finds a relevant
instance declaration in scope, that instance may require a context
that can't be solved for. A good example of this is:
f :: Ord [a] => ...
f x = ..Need Eq [a]...
......@@ -732,11 +738,14 @@ for. A good example of this is:
If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would
be left with the obligation to solve the constraint Eq a, which we cannot. So we
must be conservative in our attempt to use an instance declaration to solve the
[W] constraint we're interested in. Our rule is that we try to solve all of the
instance's subgoals recursively all at once. Precisely: We only attempt to
solve constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci are
themselves class constraints of the form `C1', ... Cm' => C' t1' ... tn'` and we
only succeed if the entire tree of constraints is solvable from instances.
[W] constraint we're interested in.
Our rule is that we try to solve all of the instance's subgoals
recursively all at once. Precisely: We only attempt to solve
constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci
are themselves class constraints of the form `C1', ... Cm' => C' t1'
... tn'` and we only succeed if the entire tree of constraints is
solvable from instances.
An example that succeeds:
......@@ -772,6 +781,26 @@ Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces:
(m @ [a] @ b $dC eta)
(GHC.Types.[] @ a)
Type families
~~~~~~~~~~~~~
Suppose we have (Trac #13943)
class Take (n :: Nat) where ...
instance {-# OVERLAPPING #-} Take 0 where ..
instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..
And we have [W] Take 3. That only matches one instance so we get
[W] Take (3-1). Really we should now flatten to reduce the (3-1) to 2, and
so on -- but that is reproducing yet more of the solver. Sigh. For now,
we just give up (remember all this is just an optimisation).
But we must not just naively try to lookup (Take (3-1)) in the
InstEnv, or it'll (wrongly appear not to match (Take 0) and get a
unique match on the (Take n) instance. That leads immediately to an
infinite loop. Hence the check that 'preds' have no type families
(isTyFamFree).
Incoherence
~~~~~~~~~~~
This optimization relies on coherence of dictionaries to be correct. When we
cannot assume coherence because of IncoherentInstances then this optimization
can change the behavior of the user's code.
......@@ -830,22 +859,16 @@ on whether we apply this optimization when IncoherentInstances is in effect:
The output of `main` if we avoid the optimization under the effect of
IncoherentInstances is `1`. If we were to do the optimization, the output of
`main` would be `2`.
It is important to emphasize that failure means that we don't produce more
efficient code, NOT that we fail to typecheck at all! This is purely an
an optimization: exactly the same programs should typecheck with or without this
procedure.
-}
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
| Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
= -- There is a matching dictionary in the inert set
do { -- First to try to solve it /completely/ from
-- top level instances
-- See Note [Solving from instances when interacting Dicts]
do { -- First to try to solve it /completely/ from top level instances
-- See Note [Shortcut solving]
dflags <- getDynFlags
; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
; try_inst_res <- shortCutSolver dflags ev_w ctev_i
; case try_inst_res of
Just evs -> do
{ flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
......@@ -877,28 +900,30 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
interactDict _ wi = pprPanic "interactDict" (ppr wi)
-- See Note [Solving from instances when interacting Dicts]
trySolveFromInstance :: DynFlags
-> CtEvidence -- Work item
-> CtEvidence -- Inert we want to try to replace
-> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
-- Everything we need to bind a solution for the work item
-- and add the solved Dict to the cache in the main solver.
trySolveFromInstance dflags ev_w ctev_i
-- See Note [Shortcut solving]
shortCutSolver :: DynFlags
-> CtEvidence -- Work item
-> CtEvidence -- Inert we want to try to replace
-> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
-- Everything we need to bind a solution for the work item
-- and add the solved Dict to the cache in the main solver.
shortCutSolver dflags ev_w ctev_i
| isWanted ev_w
&& isGiven ctev_i
-- We are about to solve a [W] constraint from a [G] constraint. We take
-- a moment to see if we can get a better solution using an instance.
-- Note that we only do this for the sake of performance. Exactly the same
-- programs should typecheck regardless of whether we take this step or
-- not. See Note [Solving from instances when interacting Dicts]
-- not. See Note [Shortcut solving]
&& not (xopt LangExt.IncoherentInstances dflags)
-- If IncoherentInstances is on then we cannot rely on coherence of proofs
-- in order to justify this optimization: The proof provided by the
-- [G] constraint's superclass may be different from the top-level proof.
&& gopt Opt_SolveConstantDicts dflags
-- Enabled by the -fsolve-constant-dicts flag
= runMaybeT $ try_solve_from_instance emptyDictMap ev_w
= runMaybeT $ try_solve_from_instance loc_w emptyDictMap ev_w
| otherwise = return Nothing
where
......@@ -927,29 +952,35 @@ trySolveFromInstance dflags ev_w ctev_i
-- cache ensures that we remember what we have already tried to
-- solve to avoid looping.
try_solve_from_instance
:: DictMap CtEvidence -> CtEvidence
:: CtLoc -> DictMap CtEvidence -> CtEvidence
-> MaybeT TcS [(EvTerm, CtEvidence, Class, [TcPredType])]
try_solve_from_instance cache ev
| ClassPred cls tys <- classifyPredType (ctEvPred ev) = do
try_solve_from_instance loc cache ev
| let pred = ctEvPred ev
, ClassPred cls tys <- classifyPredType pred
-- It is important that we add our goal to the cache before we solve!
-- Otherwise we may end up in a loop while solving recursive dictionaries.
{ let cache' = addDict cache cls tys ev
; inst_res <- lift $ match_class_inst dflags cls tys loc_w
; case inst_res of
GenInst { lir_new_theta = preds
, lir_mk_ev = mk_ev
, lir_safe_over = safeOverlap }
| safeOverlap -> do
-- emit work for subgoals but use our local cache so that we can
-- solve recursive dictionaries.
{ evc_vs <- mapM (new_wanted_cached cache') preds
; subgoalBinds <- mapM (try_solve_from_instance cache')
(freshGoals evc_vs)
; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds)
: concat subgoalBinds }
| otherwise -> mzero
_ -> mzero }
= do { let cache' = addDict cache cls tys ev
loc' = bumpCtLocDepth loc
; inst_res <- lift $ match_class_inst dflags cls tys loc_w
; case inst_res of
GenInst { lir_new_theta = preds
, lir_mk_ev = mk_ev
, lir_safe_over = safeOverlap }
| safeOverlap
, all isTyFamFree preds -- See "Type families" in
-- Note [Shortcut solving]
-> do { lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
; lift $ checkReductionDepth loc' pred
; evc_vs <- mapM (new_wanted_cached cache') preds
-- Emit work for subgoals but use our local cache
-- so we can solve recursive dictionaries.
; subgoalBinds <- mapM (try_solve_from_instance loc' cache')
(freshGoals evc_vs)
; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds)
: concat subgoalBinds }
| otherwise -> mzero
_ -> mzero }
| otherwise = mzero
addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
......
......@@ -100,7 +100,7 @@ module TcType (
isImprovementPred,
-- * Finding type instances
tcTyFamInsts,
tcTyFamInsts, isTyFamFree,
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
......@@ -823,6 +823,10 @@ tcTyFamInsts (CastTy ty _) = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _) = [] -- don't count tyfams in coercions,
-- as they never get normalized, anyway
isTyFamFree :: Type -> Bool
-- ^ Check that a type does not contain any type family applications.
isTyFamFree = null . tcTyFamInsts
{-
************************************************************************
* *
......@@ -1296,7 +1300,7 @@ mkInfSigmaTy tyvars theta ty = mkSigmaTy (mkTyVarBinders Inferred tyvars) theta
-- | Make a sigma ty where all type variables are "specified". That is,
-- they can be used with visible type application
mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
mkSpecSigmaTy tyvars ty = mkSigmaTy (mkTyVarBinders Specified tyvars) ty
mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyVarBinders Specified tyvars) preds ty
mkPhiTy :: [PredType] -> Type -> Type
mkPhiTy = mkFunTys
......
......@@ -1778,10 +1778,6 @@ checkValidTypePat pat_ty
; checkTc (isTyFamFree pat_ty) $
tyFamInstIllegalErr pat_ty }
isTyFamFree :: Type -> Bool
-- ^ Check that a type does not contain any type family applications.
isTyFamFree = null . tcTyFamInsts
-- Error messages
inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
......
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE GADTs #-}
module Data.List.Unrolled where
import GHC.TypeLits
-- | Drop @n@ elements from a list
class Drop (n :: Nat) where
drop :: [a] -> [a]
instance {-# OVERLAPPING #-} Drop 0 where
drop xs = xs
{-# INLINE drop #-}
instance {-# OVERLAPPABLE #-} (Drop (n - 1)) => Drop n where
drop [] = []
drop (_ : xs) = drop @(n - 1) xs
{-# INLINE drop #-}
-- | Take @n@ elements from a list
class Take (n :: Nat) where
take :: [a] -> [a]
instance {-# OVERLAPPING #-} Take 0 where
take _ = []
{-# INLINE take #-}
instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where
take [] = []
take (x : xs) = x : take @(n - 1) xs
{-# INLINE take #-}
-- | Split list at @n@-th element.
splitAt :: forall (n :: Nat) a. (Take n, Drop n) => [a] -> ([a], [a])
splitAt xs = (take @n xs, drop @n xs)
-- | Split list into chunks of the given length @c@. @n@ is length of the list.
class ChunksOf (n :: Nat) (c :: Nat) where
chunksOf :: [a] -> [[a]]
instance {-# OVERLAPPING #-} ChunksOf 0 0 where
chunksOf _ = []
{-# INLINE chunksOf #-}
instance {-# OVERLAPPABLE #-} ChunksOf 0 c where
chunksOf _ = []
{-# INLINE chunksOf #-}
instance {-# OVERLAPPABLE #-} ChunksOf n 0 where
chunksOf _ = []
{-# INLINE chunksOf #-}
instance {-# OVERLAPPABLE #-} (Take c, Drop c, ChunksOf (n - 1) c) => ChunksOf n c where
chunksOf xs =
let (l, r) = splitAt @c xs
in l : chunksOf @(n - 1) @c r
{-# INLINE chunksOf #-}
......@@ -575,3 +575,4 @@ test('T14128', normal, multimod_compile, ['T14128Main', '-v0'])
test('T14149', normal, compile, [''])
test('T14154', normal, compile, [''])
test('T14158', normal, compile, [''])
test('T13943', normal, compile, ['-fsolve-constant-dicts'])
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