Refactor functional dependencies a bit
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 24 Nov 2016 13:47:02 +0000 (13:47 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 25 Nov 2016 17:46:50 +0000 (17:46 +0000)
* Rename CoAxiom.Eqn = Pair Type to TypeEqn,
  and use it for fundeps

* Use the FunDepEqn for injectivity, which lets us share a bit
  more code, and (more important) brain cells

* When generating fundeps, take the max depth of the two
  constraints.  This aimed at tackling the strange loop in
  Trac #12860, but there is more to come for that.

* Improve pretty-printing with -ddump-tc-trace

compiler/typecheck/FunDeps.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcTypeNats.hs
compiler/types/CoAxiom.hs

index 0ca22bd..058a971 100644 (file)
@@ -24,6 +24,7 @@ import Var
 import Class
 import Type
 import TcType( transSuperClasses )
+import CoAxiom( TypeEqn )
 import Unify
 import FamInst( injTyVarsOfTypes )
 import InstEnv
@@ -104,10 +105,10 @@ data FunDepEqn loc
                                  --   to fresh unification vars,
                                  -- Non-empty only for FunDepEqns arising from instance decls
 
-          , fd_eqs  :: [Pair Type]  -- Make these pairs of types equal
-          , fd_pred1 :: PredType    -- The FunDepEqn arose from
-          , fd_pred2 :: PredType    --  combining these two constraints
-          , fd_loc :: loc  }
+          , fd_eqs   :: [TypeEqn]  -- Make these pairs of types equal
+          , fd_pred1 :: PredType   -- The FunDepEqn arose from
+          , fd_pred2 :: PredType   --  combining these two constraints
+          , fd_loc   :: loc  }
 
 {-
 Given a bunch of predicates that must hold, such as
@@ -148,7 +149,7 @@ instFD (ls,rs) tvs tys
 
 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
                    -> [Type] -> [Type]
-                   -> [Pair Type]
+                   -> [TypeEqn]
 -- Create a list of (Type,Type) pairs from two lists of types,
 -- making sure that the types are not already equal
 zipAndComputeFDEqs discard (ty1:tys1) (ty2:tys2)
@@ -183,6 +184,9 @@ improveFromAnother _ _ _ = []
 -- Improve a class constraint from instance declarations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+instance Outputable (FunDepEqn a) where
+  ppr = pprEquation
+
 pprEquation :: FunDepEqn a -> SDoc
 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
   = vcat [text "forall" <+> braces (pprWithCommas ppr qtvs),
@@ -222,7 +226,7 @@ improveFromInstEnv _ _ _ = []
 improveClsFD :: [TyVar] -> FunDep TyVar    -- One functional dependency from the class
              -> ClsInst                    -- An instance template
              -> [Type] -> [Maybe Name]     -- Arguments of this (C tys) predicate
-             -> [([TyCoVar], [Pair Type])] -- Empty or singleton
+             -> [([TyCoVar], [TypeEqn])]   -- Empty or singleton
 
 improveClsFD clas_tvs fd
              (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
index cb0b44f..4d49ede 100644 (file)
@@ -30,7 +30,7 @@ import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
                     coercibleDataCon )
 import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
 import Id( idType )
-import CoAxiom ( Eqn, CoAxiom(..), CoAxBranch(..), fromBranches )
+import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
 import Class
 import TyCon
 import DataCon( dataConWrapId )
@@ -377,25 +377,24 @@ runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
 -- Run this item down the pipeline, leaving behind new work and inerts
 runSolverPipeline pipeline workItem
   = do { wl <- getWorkList
+       ; inerts <- getTcSInerts
+       ; traceTcS "----------------------------- " empty
        ; traceTcS "Start solver pipeline {" $
                   vcat [ text "work item =" <+> ppr workItem
+                       , text "inerts =" <+> ppr inerts
                        , text "rest of worklist =" <+> ppr wl ]
 
        ; bumpStepCountTcS    -- One step for each constraint processed
        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
+
        ; case final_res of
            Stop ev s       -> do { traceFireTcS ev s
-                                 ; final_is <- getTcSInerts
-                                 ; traceTcS "End solver pipeline (discharged) }"
-                                       (text "inerts =" <+> ppr final_is)
+                                 ; traceTcS "End solver pipeline (discharged) }" empty
                                  ; return () }
-           ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (text "Kept as inert")
-                                 ; addInertCan ct
-                                 ; final_is <- getTcSInerts
+           ContinueWith ct -> do { addInertCan ct
+                                 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
                                  ; traceTcS "End solver pipeline (kept as inert) }" $
-                                       vcat [ text "final_item =" <+> ppr ct
-                                            , pprTyVars $ tyCoVarsOfCtList ct
-                                            , text "inerts     =" <+> ppr final_is] }
+                                            (text "final_item =" <+> ppr ct) }
        }
   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
                      -> TcS (StopOrContinue Ct)
@@ -748,7 +747,9 @@ addFunDepWork inerts work_ev cls
       where
         inert_pred = ctPred inert_ct
         inert_loc  = ctLoc inert_ct
-        derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
+        derived_loc = work_loc { ctl_depth  = ctl_depth work_loc `maxSubGoalDepth`
+                                              ctl_depth inert_loc
+                               , ctl_origin = FunDepOrigin1 work_pred  work_loc
                                                             inert_pred inert_loc }
 
 {-
@@ -894,34 +895,31 @@ improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
 -- Generate derived improvement equalities, by comparing
 -- the current work item with inert CFunEqs
 -- E.g.   x + y ~ z,   x + y' ~ z   =>   [D] y ~ y'
---
--- See Note [FunDep and implicit parameter reactions]
-improveLocalFunEqs ev inerts fam_tc args fsk
-  | isGiven ev   -- See Note [No FunEq improvement for Givens]
+improveLocalFunEqs work_ev inerts fam_tc args fsk
+  | isGiven work_ev   -- See Note [No FunEq improvement for Givens]
   = return ()
 
-  | null improvement_eqns
-  = do { traceTcS "improveLocalFunEqs no improvements: " $
-         vcat [ text "Candidates:" <+> ppr funeqs_for_tc
-              , text "Inert eqs:" <+> ppr ieqs ]
-       ; return () }
-
-  | otherwise
-  = do { traceTcS "improveLocalFunEqs improvements: " $
+  | not (null improvement_eqns)
+  = do { traceTcS "interactFunEq improvements: " $
          vcat [ text "Eqns:" <+> ppr improvement_eqns
               , text "Candidates:" <+> ppr funeqs_for_tc
               , text "Inert eqs:" <+> ppr ieqs ]
-       ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
+       ; emitFunDepDeriveds improvement_eqns }
+
+  | otherwise
+  = return ()
 
   where
-    loc           = ctEvLoc ev
     ieqs          = inert_eqs inerts
     funeqs        = inert_funeqs inerts
     funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
     rhs           = lookupFlattenTyVar ieqs fsk
+    work_loc      = ctEvLoc work_ev
+    work_pred     = ctEvPred work_ev
     fam_inj_info  = familyTyConInjectivityInfo fam_tc
 
     --------------------
+    improvement_eqns :: [FunDepEqn CtLoc]
     improvement_eqns
       | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
       =    -- Try built-in families, notably for arithmethic
@@ -935,21 +933,38 @@ improveLocalFunEqs ev inerts fam_tc args fsk
       = []
 
     --------------------
-    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar ieqs ifsk)
+    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
+      = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
+                                             (lookupFlattenTyVar ieqs ifsk))
+
     do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
 
     --------------------
     -- See Note [Type inference for type families with injectivity]
-    do_one_injective inj_args (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
+    do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
+                                         , cc_fsk = ifsk, cc_ev = inert_ev })
       | rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
-      = [ Pair arg iarg
-        | (arg, iarg, True) <- zip3 args iargs inj_args ]
-
-      | otherwise = []
+      = mk_fd_eqns inert_ev $
+            [ Pair arg iarg
+            | (arg, iarg, True) <- zip3 args inert_args inj_args ]
+      | otherwise
+      = []
 
     do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
 
+    --------------------
+    mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
+    mk_fd_eqns inert_ev eqns
+      | null eqns  = []
+      | otherwise  = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
+                             , fd_pred1 = work_pred
+                             , fd_pred2 = ctEvPred inert_ev
+                             , fd_loc   = loc } ]
+      where
+        inert_loc = ctEvLoc inert_ev
+        loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
+                                      ctl_depth work_loc }
+
 -------------
 reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F args1 ~ fsk1
            -> CtEvidence -> TcTyVar    -- Solve this :: F args2 ~ fsk2
@@ -1337,9 +1352,11 @@ emitFunDepDeriveds fd_eqns
   where
     do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
      | null tvs  -- Common shortcut
-     = mapM_ (unifyDerived loc Nominal) eqs
+     = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs)
+          ; mapM_ (unifyDerived loc Nominal) eqs }
      | otherwise
-     = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
+     = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr eqs)
+          ; (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
           ; mapM_ (do_one_eq loc subst) eqs }
 
     do_one_eq loc subst (Pair ty1 ty2)
@@ -1459,7 +1476,7 @@ improveTopFunEqs ev fam_tc args fsk
 
 improve_top_fun_eqs :: FamInstEnvs
                     -> TyCon -> [TcType] -> TcType
-                    -> TcS [Eqn]
+                    -> TcS [TypeEqn]
 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
   | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
   = return (sfInteractTop ops args rhs_ty)
@@ -1506,7 +1523,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
 
       injImproveEqns :: [Bool]
                      -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
-                     -> TcS [Eqn]
+                     -> TcS [TypeEqn]
       injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
         (theta', _) <- instFlexiTcS unsubstTvs
         -- The use of deterministically ordered list for `unsubstTvs`
@@ -1786,7 +1803,7 @@ doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
 -- Try to use type-class instance declarations to simplify the constraint
 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
                                           , cc_tyargs = xis })
-  | isGiven fl
+  | isGiven fl   -- Never use instances for Given constraints
   = do { try_fundep_improvement
        ; continueWith work_item }
 
@@ -1794,34 +1811,18 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
   = do { setEvBindIfWanted fl (ctEvTerm ev)
        ; stopWith fl "Dict/Top (cached)" }
 
-  | isDerived fl  -- Use type-class instances for Deriveds, in the hope
-                  -- of generating some improvements
-                  -- C.f. Example 3 of Note [The improvement story]
-                  -- It's easy because no evidence is involved
-   = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst { lir_new_theta = preds
-                       , lir_safe_over = s } ->
-                 do { emitNewDeriveds dict_loc preds
-                    ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; stopWith fl "Dict/Top (solved)" }
-
-               NoInstance ->
-                 do { -- If there is no instance, try improvement
-                      try_fundep_improvement
-                    ; continueWith work_item } }
-
-  | otherwise  -- Wanted, but not cached
+  | otherwise  -- Wanted or Derived, but not cached
    = do { dflags <- getDynFlags
         ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
         ; case lkup_inst_res of
                GenInst { lir_new_theta = theta
                        , lir_mk_ev     = mk_ev
                        , lir_safe_over = s } ->
-                 do { addSolvedDict fl cls xis
+                 do { traceTcS "doTopReact/found instance for" $ ppr fl
+                    ; checkReductionDepth deeper_loc dict_pred
                     ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; solve_from_instance theta mk_ev }
+                    ; if isDerived fl then finish_derived theta
+                                      else finish_wanted  theta mk_ev }
                NoInstance ->
                  do { try_fundep_improvement
                     ; continueWith work_item } }
@@ -1838,21 +1839,23 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
        | otherwise
        = loc
 
-     solve_from_instance :: [TcPredType]
-                         -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
+     finish_wanted :: [TcPredType]
+                   -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
-     solve_from_instance theta mk_ev
-        | null theta
-        = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
-             ; setWantedEvBind (ctEvId fl) (mk_ev [])
-             ; stopWith fl "Dict/Top (solved, no new work)" }
-        | otherwise
-        = do { checkReductionDepth deeper_loc dict_pred
-             ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
+     finish_wanted theta mk_ev
+        = do { addSolvedDict fl cls xis
              ; evc_vars <- mapM (newWanted deeper_loc) theta
              ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
              ; emitWorkNC (freshGoals evc_vars)
-             ; stopWith fl "Dict/Top (solved, more work)" }
+             ; stopWith fl "Dict/Top (solved wanted)" }
+
+     finish_derived theta  -- Use type-class instances for Deriveds, in the hope
+       =                   -- of generating some improvements
+                           -- C.f. Example 3 of Note [The improvement story]
+                           -- It's easy because no evidence is involved
+         do { emitNewDeriveds deeper_loc theta
+            ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
+            ; stopWith fl "Dict/Top (solved derived)" }
 
      -- We didn't solve it; so try functional dependencies with
      -- the instance environment, and return
index fd6d74c..dc08a66 100644 (file)
@@ -88,7 +88,7 @@ module TcRnTypes(
         arisesFromGivens,
 
         Implication(..), ImplicStatus(..), isInsolubleStatus,
-        SubGoalDepth, initialSubGoalDepth,
+        SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
         bumpSubGoalDepth, subGoalDepthExceeded,
         CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
         ctLocTypeOrKind_maybe,
@@ -2385,7 +2385,11 @@ instance Outputable TcEvDest where
   ppr (EvVarDest ev) = ppr ev
 
 instance Outputable CtEvidence where
-  ppr ev = ppr (ctEvFlavour ev) <+> pp_ev <+> dcolon <+> ppr (ctEvPred ev)
+  ppr ev = ppr (ctEvFlavour ev)
+           <+> pp_ev
+           <+> braces (ppr (ctl_depth (ctEvLoc ev))) <> dcolon
+                  -- Show the sub-goal depth too
+           <+> ppr (ctEvPred ev)
     where
       pp_ev = case ev of
              CtGiven { ctev_evar = v } -> ppr v
@@ -2686,6 +2690,9 @@ initialSubGoalDepth = SubGoalDepth 0
 bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
 bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
 
+maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
+maxSubGoalDepth (SubGoalDepth n) (SubGoalDepth m) = SubGoalDepth (n `max` m)
+
 subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
 subGoalDepthExceeded dflags (SubGoalDepth d)
   = mkIntWithInf d > reductionDepth dflags
@@ -2973,7 +2980,7 @@ data CtOrigin
 
   | FunDepOrigin2       -- A functional dependency from combining
         PredType CtOrigin   -- This constraint arising from ...
-        PredType SrcSpan    -- and this instance
+        PredType SrcSpan    -- and this top-level instance
         -- We only need a CtOrigin on the first, because the location
         -- is pinned on the entire error message
 
index dd9a82b..7665e44 100644 (file)
@@ -402,7 +402,10 @@ data InertSet
 
 instance Outputable InertSet where
   ppr is = vcat [ ppr $ inert_cans is
-                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
+                , ppUnless (null dicts) $
+                  text "Solved dicts" <+> vcat (map ppr dicts) ]
+         where
+           dicts = bagToList (dictsToBag (inert_solved_dicts is))
 
 emptyInert :: InertSet
 emptyInert
@@ -2258,8 +2261,9 @@ traceFireTcS ev doc
   = TcS $ \env -> csTraceTcM $
     do { n <- TcM.readTcRef (tcs_count env)
        ; tclvl <- TcM.getTcLevel
-       ; return (hang (int n <> brackets (text "U:" <> ppr tclvl
-                                          <> ppr (ctLocDepth (ctEvLoc ev)))
+       ; return (hang (text "Step" <+> int n
+                       <> brackets (text "l:" <> ppr tclvl <> comma <>
+                                    text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
                        <+> doc <> colon)
                      4 (ppr ev)) }
 
index cececff..d01ffee 100644 (file)
@@ -21,7 +21,7 @@ import TyCon      ( TyCon, FamTyConFlav(..), mkFamilyTyCon
                   , Injectivity(..) )
 import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi )
-import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..), Eqn )
+import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn )
 import Name       ( Name, BuiltInSyntax(..) )
 import TysWiredIn
 import TysPrim    ( mkTemplateAnonTyConBinders )
@@ -359,7 +359,7 @@ mkBinAxiom str tc f =
 
 
 
-mkAxiom1 :: String -> (Eqn -> Eqn) -> CoAxiomRule
+mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
 mkAxiom1 str f =
   CoAxiomRule
     { coaxrName      = fsLit str
index 89d9bef..fcbf4e8 100644 (file)
@@ -25,7 +25,7 @@ module CoAxiom (
 
        Role(..), fsFromRole,
 
-       CoAxiomRule(..), Eqn,
+       CoAxiomRule(..), TypeEqn,
        BuiltInSynFamily(..), trivialBuiltInFamily
        ) where
 
@@ -464,14 +464,14 @@ as `CoAxiom` is the special case when there are no assumptions.
 -}
 
 -- | A more explicit representation for `t1 ~ t2`.
-type Eqn = Pair Type
+type TypeEqn = Pair Type
 
 -- | For now, we work only with nominal equality.
 data CoAxiomRule = CoAxiomRule
   { coaxrName      :: FastString
   , coaxrAsmpRoles :: [Role]    -- roles of parameter equations
   , coaxrRole      :: Role      -- role of resulting equation
-  , coaxrProves    :: [Eqn] -> Maybe Eqn
+  , coaxrProves    :: [TypeEqn] -> Maybe TypeEqn
         -- ^ coaxrProves returns @Nothing@ when it doesn't like
         -- the supplied arguments.  When this happens in a coercion
         -- that means that the coercion is ill-formed, and Core Lint
@@ -500,9 +500,9 @@ instance Outputable CoAxiomRule where
 -- Type checking of built-in families
 data BuiltInSynFamily = BuiltInSynFamily
   { sfMatchFam      :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
-  , sfInteractTop   :: [Type] -> Type -> [Eqn]
+  , sfInteractTop   :: [Type] -> Type -> [TypeEqn]
   , sfInteractInert :: [Type] -> Type ->
-                       [Type] -> Type -> [Eqn]
+                       [Type] -> Type -> [TypeEqn]
   }
 
 -- Provides default implementations that do nothing.