Skip to content
GitLab
Commit bec932ef authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Some simplification and refactoring of FunDeps 

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.
parent 3992a6e2
Hide whitespace changes
Inline Side-by-side
compiler/typecheck/FunDeps.hs
View file @ bec932ef
......@@ -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
{-
************************************************************************
......
compiler/typecheck/TcInteract.hs
View file @ bec932ef
......@@ -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)
--------------------
......
Supports Markdown
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