Some simplification and refactoring of FunDeps
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 20 Jan 2015 17:56:09 +0000 (17:56 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 20 Jan 2015 17:56:09 +0000 (17:56 +0000)
Nothing magical here, but the data types had grown more complicated
than we really needed, so there were some worthwhile simplifications
to be had.

No change in functionality.

compiler/typecheck/FunDeps.hs
compiler/typecheck/TcInteract.hs

index a55fa2e..2d0ac33 100644 (file)
@@ -11,8 +11,7 @@ It's better to read it as: "if we know these, then we're going to know these"
 {-# LANGUAGE CPP #-}
 
 module FunDeps (
-        FDEq (..),
-        Equation(..), pprEquation,
+        FunDepEqn(..), pprEquation,
         improveFromInstEnv, improveFromAnother,
         checkInstCoverage, checkFunDeps,
         pprFundeps
@@ -34,6 +33,7 @@ import SrcLoc
 import Util
 import FastString
 
+import Pair             ( Pair(..) )
 import Data.List        ( nubBy )
 import Data.Maybe       ( isJust )
 
@@ -49,21 +49,23 @@ Each functional dependency with one variable in the RHS is responsible
 for generating a single equality. For instance:
      class C a b | a -> b
 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
-     FDEq { fd_pos      = 1
-          , fd_ty_left  = Bool
-          , fd_ty_right = alpha }
+will generate the folloing FunDepEqn
+     FDEqn { fd_qtvs = []
+           , fd_eqs  = [Pair Bool alpha]
+           , fd_pred1 = C Int Bool
+           , fd_pred2 = C Int alpha
+           , fd_loc = ... }
 However notice that a functional dependency may have more than one variable
-in the RHS which will create more than one FDEq. Example:
+in the RHS which will create more than one pair of types in fd_eqs. Example:
      class C a b c | a -> b c
      [Wanted] C Int alpha alpha
      [Wanted] C Int Bool beta
 Will generate:
-        fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
-        fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
-
-We record the paremeter position so that can immediately rewrite a constraint
-using the produced FDEqs and remove it from our worklist.
-
+     FDEqn { fd_qtvs = []
+           , fd_eqs  = [Pair Bool alpha, Pair alpha beta]
+           , fd_pred1 = C Int Bool
+           , fd_pred2 = C Int alpha
+           , fd_loc = ... }
 
 INVARIANT: Corresponding types aren't already equal
 That is, there exists at least one non-identity equality in FDEqs.
@@ -95,19 +97,15 @@ unification variables when producing the FD constraints.
 Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
 -}
 
-data Equation loc
-   = FDEqn { fd_qtvs :: [TyVar]                 -- Instantiate these type and kind vars to fresh unification vars
-           , fd_eqs  :: [FDEq]                  --   and then make these equal
-           , fd_pred1, fd_pred2 :: PredType     -- The Equation arose from combining these two constraints
-           , fd_loc :: loc  }
-
-data FDEq = FDEq { fd_pos      :: Int -- We use '0' for the first position
-                 , fd_ty_left  :: Type
-                 , fd_ty_right :: Type }
+data FunDepEqn loc
+  = FDEqn { fd_qtvs :: [TyVar]   -- Instantiate these type and kind vars
+                                 --   to fresh unification vars,
+                                 -- Non-empty only for FunDepEqns arising from instance decls
 
-instance Outputable FDEq where
-  ppr (FDEq { fd_pos = p, fd_ty_left = tyl, fd_ty_right = tyr })
-    = parens (int p <> comma <+> ppr tyl <> comma <+> ppr tyr)
+          , 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  }
 
 {-
 Given a bunch of predicates that must hold, such as
@@ -139,84 +137,74 @@ NOTA BENE:
 -}
 
 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
--- A simpler version of instFD_WithPos to be used in checking instance coverage etc.
+-- (instFD fd tvs tys) returns fd instantiated with (tvs -> tys)
 instFD (ls,rs) tvs tys
   = (map lookup ls, map lookup rs)
   where
     env       = zipVarEnv tvs tys
     lookup tv = lookupVarEnv_NF env tv
 
-instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)])
--- Returns a FunDep between the types accompanied along with their
--- position (<=0) in the types argument list.
-instFD_WithPos (ls,rs) tvs tys
-  = (map (snd . lookup) ls, map lookup rs)
-  where
-    ind_tys   = zip [0..] tys
-    env       = zipVarEnv tvs ind_tys
-    lookup tv = lookupVarEnv_NF env tv
-
 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
-                   -> [Type]
-                   -> [(Int,Type)]
-                   -> [FDEq]
--- Create a list of FDEqs from two lists of types, making sure
--- that the types are not equal.
-zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
+                   -> [Type] -> [Type]
+                   -> [Pair Type]
+-- 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)
  | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
- | otherwise = FDEq { fd_pos      = i2
-                    , fd_ty_left  = ty1
-                    , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
+ | otherwise       = Pair ty1 ty2 : zipAndComputeFDEqs discard tys1 tys2
 zipAndComputeFDEqs _ _ _ = []
 
 -- Improve a class constraint from another class constraint
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-improveFromAnother :: PredType -- Template item (usually given, or inert)
+improveFromAnother :: loc
+                   -> PredType -- Template item (usually given, or inert)
                    -> PredType -- Workitem [that can be improved]
-                   -> [Equation ()]
+                   -> [FunDepEqn loc]
 -- Post: FDEqs always oriented from the other to the workitem
 --       Equations have empty quantified variables
-improveFromAnother pred1 pred2
+improveFromAnother loc pred1 pred2
   | Just (cls1, tys1) <- getClassPredTys_maybe pred1
   , Just (cls2, tys2) <- getClassPredTys_maybe pred2
   , tys1 `lengthAtLeast` 2 && cls1 == cls2
-  = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = () }
+  = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
     | let (cls_tvs, cls_fds) = classTvsFds cls1
     , fd <- cls_fds
-    , let (ltys1, rs1)  = instFD         fd cls_tvs tys1
-          (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
+    , let (ltys1, rs1) = instFD fd cls_tvs tys1
+          (ltys2, rs2) = instFD fd cls_tvs tys2
     , eqTypes ltys1 ltys2               -- The LHSs match
-    , let eqs = zipAndComputeFDEqs eqType rs1 irs2
+    , let eqs = zipAndComputeFDEqs eqType rs1 rs2
     , not (null eqs) ]
 
-improveFromAnother _ _ = []
+improveFromAnother _ _ = []
 
 
 -- Improve a class constraint from instance declarations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-pprEquation :: Equation a -> SDoc
+pprEquation :: FunDepEqn a -> SDoc
 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
-          nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
+          nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 
+                       | Pair t1 t2 <- pairs])]
 
 improveFromInstEnv :: InstEnvs
+                   -> (PredType -> SrcSpan -> loc)
                    -> PredType
-                   -> [Equation SrcSpan] -- Needs to be an Equation because
-                                         -- of quantified variables
+                   -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
+                                      -- of quantified variables
 -- Post: Equations oriented from the template (matching instance) to the workitem!
-improveFromInstEnv _inst_env pred
+improveFromInstEnv _inst_env pred
   | not (isClassPred pred)
   = panic "improveFromInstEnv: not a class predicate"
-improveFromInstEnv inst_env pred
+improveFromInstEnv inst_env mk_loc pred
   | Just (cls, tys) <- getClassPredTys_maybe pred
   , tys `lengthAtLeast` 2
   , let (cls_tvs, cls_fds) = classTvsFds cls
         instances          = classInstances inst_env cls
         rough_tcs          = roughMatchTcs tys
   = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
-            , fd_pred1 = p_inst, fd_pred2=pred
-            , fd_loc = getSrcSpan (is_dfun ispec) }
+            , fd_pred1 = p_inst, fd_pred2 = pred
+            , fd_loc = mk_loc p_inst (getSrcSpan (is_dfun ispec)) }
     | fd <- cls_fds             -- Iterate through the fundeps first,
                                 -- because there often are none!
     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
@@ -229,14 +217,14 @@ improveFromInstEnv inst_env pred
                                     emptyVarSet tys trimmed_tcs -- NB: orientation
     , let p_inst = mkClassPred cls (is_tys ispec)
     ]
-improveFromInstEnv _ _ = []
+improveFromInstEnv _ _ = []
 
 
 checkClsFD :: FunDep TyVar -> [TyVar]             -- One functional dependency from the class
            -> ClsInst                             -- An instance template
            -> TyVarSet -> [Type] -> [Maybe Name]  -- Arguments of this (C tys) predicate
                                                   -- TyVarSet are extra tyvars that can be instantiated
-           -> [([TyVar], [FDEq])]
+           -> [([TyVar], [Pair Type])]
 
 checkClsFD fd clas_tvs
            (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
@@ -302,10 +290,9 @@ checkClsFD fd clas_tvs
                         -- work of the ls1/ls2 unification leaving a smaller unification problem
                   where
                     rtys1' = map (substTy subst) rtys1
-                    irs2'  = map (\(i,x) -> (i,substTy subst x)) irs2
-                    rtys2' = map snd irs2'
+                    rtys2' = map (substTy subst) rtys2
 
-                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
+                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2'
                         -- Don't discard anything!
                         -- We could discard equal types but it's an overkill to call
                         -- eqType again, since we know for sure that /at least one/
@@ -335,8 +322,8 @@ checkClsFD fd clas_tvs
                | tv `elemVarSet` extra_qtvs = BindMe
                | otherwise                  = Skolem
 
-    (ltys1, rtys1) = instFD         fd clas_tvs tys_inst
-    (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys_actual
+    (ltys1, rtys1) = instFD fd clas_tvs tys_inst
+    (ltys2, rtys2) = instFD fd clas_tvs tys_actual
 
 {-
 ************************************************************************
index 3212710..18ca270 100644 (file)
@@ -38,7 +38,7 @@ import TcSMonad
 import Bag
 
 import Data.List( partition, foldl', deleteFirstsBy )
-
+import SrcLoc
 import VarEnv
 
 import Control.Monad
@@ -644,9 +644,13 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
   = interactGivenIP inerts workItem
 
   | otherwise
-  = do { mapBagM_ (addFunDepWork workItem) (findDictsByClass (inert_dicts inerts) cls)
-               -- Standard thing: create derived fds and keep on going. Importantly we don't
-               -- throw workitem back in the worklist because this can cause loops (see #5236)
+  = do { mapBagM_ (addFunDepWork workItem) 
+                  (findDictsByClass (inert_dicts inerts) cls)
+               -- Create derived fds and keep on going.
+               -- No need to check flavour; fundeps work between
+               -- any pair of constraints, regardless of flavour
+               -- Importantly we don't throw workitem back in the 
+               -- worklist bebcause this can cause loops (see #5236)
        ; continueWith workItem  }
 
 interactDict _ wi = pprPanic "interactDict" (ppr wi)
@@ -672,17 +676,15 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
 
 addFunDepWork :: Ct -> Ct -> TcS ()
+-- Add derived constraints from type-class functional dependencies.
 addFunDepWork work_ct inert_ct
-  = do {  let fd_eqns :: [Equation CtLoc]
-              fd_eqns = [ eqn { fd_loc = derived_loc }
-                        | eqn <- improveFromAnother inert_pred work_pred ]
-       ; rewriteWithFunDeps fd_eqns
+  = emitFunDepDeriveds $
+    improveFromAnother derived_loc inert_pred work_pred
                 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                 -- NB: We do create FDs for given to report insoluble equations that arise
                 -- from pairs of Givens, and also because of floating when we approximate
                 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
                 -- Also see Note [When improvement happens]
-    }
   where
     work_pred  = ctPred work_ct
     inert_pred = ctPred inert_ct
@@ -1214,19 +1216,18 @@ To achieve this required some refactoring of FunDeps.lhs (nicer
 now!).
 -}
 
-rewriteWithFunDeps :: [Equation CtLoc] -> TcS ()
--- NB: The returned constraints are all Derived
--- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
-rewriteWithFunDeps eqn_pred_locs
- = mapM_ instFunDepEqn eqn_pred_locs
-
-instFunDepEqn :: Equation CtLoc -> TcS ()
--- Post: Returns the position index as well as the corresponding FunDep equality
-instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
-  = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
-       ; mapM_ (do_one subst) eqs }
+emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
+emitFunDepDeriveds fd_eqns
+  = mapM_ do_one_FDEqn fd_eqns
   where
-    do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
+    do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
+     | null tvs  -- Common shortcut
+     = mapM_ (unifyDerived loc Nominal) eqs
+     | otherwise
+     = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
+          ; mapM_ (do_one_eq loc subst) eqs }
+
+    do_one_eq loc subst (Pair ty1 ty2)
        = unifyDerived loc Nominal $
          Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
 
@@ -1270,20 +1271,22 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
   | not (isWanted fl)   -- Never use instances for Given or Derived constraints
   = try_fundeps_and_return
 
-  | Just ev <- lookupSolvedDict inerts loc cls xis   -- Cached
+  | Just ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
   = do { setWantedEvBind dict_id (ctEvTerm ev);
        ; stopWith fl "Dict/Top (cached)" }
 
   | otherwise  -- Not cached
-   = do { lkup_inst_res <- matchClassInst inerts cls xis loc
+   = do { lkup_inst_res <- matchClassInst inerts cls xis dict_loc
          ; case lkup_inst_res of
                GenInst wtvs ev_term -> do { addSolvedDict fl cls xis
                                           ; solve_from_instance wtvs ev_term }
                NoInstance -> try_fundeps_and_return }
    where
      dict_id = ASSERT( isWanted fl ) ctEvId fl
-     pred = mkClassPred cls xis
-     loc = ctEvLoc fl
+     dict_pred = mkClassPred cls xis
+     dict_loc = ctEvLoc fl
+     dict_origin = ctLocOrigin dict_loc
+     deeper_loc = bumpCtLocDepth CountConstraints dict_loc
 
      solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
@@ -1298,7 +1301,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
                ppr dict_id
              ; setWantedEvBind dict_id ev_term
              ; let mk_new_wanted ev
-                       = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
+                     = mkNonCanonical (ev {ctev_loc = deeper_loc })
              ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
              ; stopWith fl "Dict/Top (solved, more work)" }
 
@@ -1309,14 +1312,17 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
      -- so we make sure we get on and solve it first. See Note [Weird fundeps]
      try_fundeps_and_return
        = do { instEnvs <- getInstEnvs
-            ; let fd_eqns :: [Equation CtLoc]
-                  fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
-                                                                             inst_pred inst_loc } }
-                            | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
-                            <- improveFromInstEnv instEnvs pred ]
-            ; rewriteWithFunDeps fd_eqns
+            ; emitFunDepDeriveds $
+              improveFromInstEnv instEnvs mk_ct_loc dict_pred
             ; continueWith work_item }
 
+     mk_ct_loc :: PredType   -- From instance decl
+               -> SrcSpan    -- also from instance deol
+               -> CtLoc
+     mk_ct_loc inst_pred inst_loc
+       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
+                                               inst_pred inst_loc }
+
 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
 --------------------