Fix bug in the short-cut solver
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 2 Oct 2017 14:58:46 +0000 (15:58 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 3 Oct 2017 08:52:39 +0000 (09:52 +0100)
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

compiler/typecheck/TcInteract.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
testsuite/tests/typecheck/should_compile/T13943.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 3d506f6..df15e46 100644 (file)
@@ -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 ()
index a1e3334..103c9cc 100644 (file)
@@ -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
index 712f9ad..232265d 100644 (file)
@@ -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
diff --git a/testsuite/tests/typecheck/should_compile/T13943.hs b/testsuite/tests/typecheck/should_compile/T13943.hs
new file mode 100644 (file)
index 0000000..f40ee23
--- /dev/null
@@ -0,0 +1,68 @@
+{-# 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 #-}
index ddf2376..a1062a2 100644 (file)
@@ -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'])