Commit 296058a1 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

Equality constraint solver is now externally pure

- This patch changes the equality constraint solver such that it does not
  instantiate any type variables that occur in the constraints that are to be
  solved (or in the environment).  Instead, it returns a bag of type bindings.
- If these type bindings (together with the other results of the solver) are
  discarded, solver invocation has no effect (outside the solver) and can be
  repeated (that's imported for TcSimplifyRestricted).
- For the type bindings to take effect, the caller of the solver needs to 
  execute them. 
- The solver will still instantiate type variables thet were created during 
  solving (e.g., skolem flexibles used during type flattening).

  See also http://hackage.haskell.org/trac/ghc/wiki/TypeFunctionsSolving
parent 25b72d3e
......@@ -25,7 +25,7 @@ module CoreFVs (
exprFreeNames, exprsFreeNames,
-- * Free variables of Rules, Vars and Ids
idRuleVars, idFreeVars, varTypeTyVars,
idRuleVars, idFreeVars, varTypeTyVars, varTypeTcTyVars,
ruleRhsFreeVars, rulesFreeVars,
ruleLhsFreeNames, ruleLhsFreeIds,
......@@ -370,6 +370,13 @@ varTypeTyVars var
| isLocalId var || isCoVar var = tyVarsOfType (idType var)
| otherwise = emptyVarSet -- Global Ids and non-coercion TyVars
varTypeTcTyVars :: Var -> TyVarSet
-- Find the type variables free in the type of the variable
-- Remember, coercion variables can mention type variables...
varTypeTcTyVars var
| isLocalId var || isCoVar var = tcTyVarsOfType (idType var)
| otherwise = emptyVarSet -- Global Ids and non-coercion TyVars
idFreeVars :: Id -> VarSet
idFreeVars id = ASSERT( isId id) idRuleVars id `unionVarSet` varTypeTyVars id
......
......@@ -22,9 +22,9 @@ module Inst (
tcInstClassOp,
tcSyntaxName, isHsVar,
tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE,
ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
growInstsTyVars, getDictClassTys, dictPred,
tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, tcTyVarsOfInst,
tcTyVarsOfInsts, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst,
fdPredsOfInsts, growInstsTyVars, getDictClassTys, dictPred,
lookupSimpleInst, LookupInstResult(..),
tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
......@@ -193,22 +193,53 @@ ipNamesOfInst (Method {tci_theta = theta}) = [ipNameName n | IParam n _ <- the
ipNamesOfInst _ = []
---------------------------------
tyVarsOfInst :: Inst -> TcTyVarSet
-- |All free type variables (not including the coercion variables of
-- equalities)
--
tyVarsOfInst :: Inst -> TyVarSet
tyVarsOfInst (LitInst {tci_ty = ty}) = tyVarsOfType ty
tyVarsOfInst (Dict {tci_pred = pred}) = tyVarsOfPred pred
tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id
-- The id might have free type variables; in the case of
-- locally-overloaded class methods, for example
tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds})
tyVarsOfInst (Method {tci_oid = id, tci_tys = tys})
= tyVarsOfTypes tys `unionVarSet` varTypeTyVars id
-- The id might have free type variables; in the case of
-- locally-overloaded class methods, for example
tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens,
tci_wanted = wanteds})
= (tyVarsOfInsts givens `unionVarSet` tyVarsOfInsts wanteds)
`minusVarSet` mkVarSet tvs
`unionVarSet` unionVarSets (map varTypeTyVars tvs)
-- Remember the free tyvars of a coercion
tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2})
= tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
-- |All free meta type variables *including* the coercion variables of
-- equalities
--
tcTyVarsOfInst :: Inst -> TyVarSet
tcTyVarsOfInst (LitInst {tci_ty = ty}) = tcTyVarsOfType ty
tcTyVarsOfInst (Dict {tci_pred = pred}) = tcTyVarsOfPred pred
tcTyVarsOfInst (Method {tci_oid = id, tci_tys = tys})
= tcTyVarsOfTypes tys `unionVarSet` varTypeTcTyVars id
-- The id might have free type variables; in the case of
-- locally-overloaded class methods, for example
tcTyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens,
tci_wanted = wanteds})
= (tcTyVarsOfInsts givens `unionVarSet` tcTyVarsOfInsts wanteds)
`minusVarSet` mkVarSet tvs
`unionVarSet` unionVarSets (map varTypeTcTyVars tvs)
-- Remember the free tyvars of a coercion
tcTyVarsOfInst (EqInst {tci_co = co, tci_left = ty1, tci_right = ty2})
= either unitVarSet tcTyVarsOfType co `unionVarSet` -- include covars
tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
tyVarsOfInsts :: [Inst] -> VarSet
tyVarsOfInsts :: [Inst] -> TyVarSet
tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
tyVarsOfLIE :: Bag Inst -> VarSet
tcTyVarsOfInsts :: [Inst] -> TcTyVarSet
tcTyVarsOfInsts insts = foldr (unionVarSet . tcTyVarsOfInst) emptyVarSet insts
tyVarsOfLIE :: Bag Inst -> TyVarSet
tyVarsOfLIE lie = tyVarsOfInsts (lieToList lie)
......@@ -1029,7 +1060,7 @@ depending on whether a EqInstCo is for a wanted or local equality:
--
mkIdEqInstCo :: EqInstCo -> Type -> TcM ()
mkIdEqInstCo (Left cotv) t
= writeMetaTyVar cotv t
= bindMetaTyVar cotv t
mkIdEqInstCo (Right _) _
= return ()
......@@ -1038,7 +1069,7 @@ mkIdEqInstCo (Right _) _
mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo
mkSymEqInstCo (Left cotv) (ty1, ty2)
= do { cotv' <- newMetaCoVar ty1 ty2
; writeMetaTyVar cotv (mkSymCoercion (TyVarTy cotv'))
; bindMetaTyVar cotv (mkSymCoercion (TyVarTy cotv'))
; return $ Left cotv'
}
mkSymEqInstCo (Right co) _
......@@ -1049,7 +1080,7 @@ mkSymEqInstCo (Right co) _
mkLeftTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
mkLeftTransEqInstCo (Left cotv) given_co (ty1, ty2)
= do { cotv' <- newMetaCoVar ty1 ty2
; writeMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co)
; bindMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co)
; return $ Left cotv'
}
mkLeftTransEqInstCo (Right co) given_co _
......@@ -1060,7 +1091,7 @@ mkLeftTransEqInstCo (Right co) given_co _
mkRightTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
mkRightTransEqInstCo (Left cotv) given_co (ty1, ty2)
= do { cotv' <- newMetaCoVar ty1 ty2
; writeMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv')
; bindMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv')
; return $ Left cotv'
}
mkRightTransEqInstCo (Right co) given_co _
......@@ -1073,7 +1104,7 @@ mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
mkAppEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
= do { cotv_l <- newMetaCoVar ty1_l ty2_l
; cotv_r <- newMetaCoVar ty1_r ty2_r
; writeMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
; bindMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
; return (Left cotv_l, Left cotv_r)
}
mkAppEqInstCo (Right co) _ _
......@@ -1084,7 +1115,7 @@ mkAppEqInstCo (Right co) _ _
mkTyConEqInstCo :: EqInstCo -> TyCon -> [(Type, Type)] -> TcM ([EqInstCo])
mkTyConEqInstCo (Left cotv) con ty12s
= do { cotvs <- mapM (uncurry newMetaCoVar) ty12s
; writeMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs))
; bindMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs))
; return (map Left cotvs)
}
mkTyConEqInstCo (Right co) _ args
......@@ -1102,7 +1133,7 @@ mkFunEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
mkFunEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
= do { cotv_l <- newMetaCoVar ty1_l ty2_l
; cotv_r <- newMetaCoVar ty1_r ty2_r
; writeMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
; bindMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
; return (Left cotv_l, Left cotv_r)
}
mkFunEqInstCo (Right co) _ _
......
......@@ -35,14 +35,14 @@ module TcMType (
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
tcInstSigType,
tcInstSkolTyVars, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
tcSkolSigType, tcSkolSigTyVars, occurCheckErr, execTcTyVarBinds,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance,
checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkKinds,
checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
growPredTyVars, growTyVars, growThetaTyVars,
......@@ -78,6 +78,7 @@ import VarSet
import ErrUtils
import DynFlags
import Util
import Bag
import Maybes
import ListSetOps
import UniqSupply
......@@ -337,6 +338,27 @@ Rather, we should bind t to () (= non_var_ty2).
--------------
Execute a bag of type variable bindings.
\begin{code}
execTcTyVarBinds :: TcTyVarBinds -> TcM ()
execTcTyVarBinds = mapM_ execTcTyVarBind . bagToList
where
execTcTyVarBind (TcTyVarBind tv ty)
= do { ASSERTM2( do { details <- readMetaTyVar tv
; return (isFlexi details) }, ppr tv )
; ty' <- if isCoVar tv
then return ty
else do { maybe_ty <- checkTauTvUpdate tv ty
; case maybe_ty of
Nothing -> pprPanic "TcRnMonad.execTcTyBind"
(ppr tv <+> text ":=" <+> ppr ty)
Just ty' -> return ty'
}
; writeMetaTyVar tv ty'
}
\end{code}
Error mesages in case of kind mismatch.
\begin{code}
......@@ -522,19 +544,17 @@ writeMetaTyVar tyvar ty
return ()
| otherwise
= ASSERT( isMetaTyVar tyvar )
-- TOM: It should also work for coercions
-- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
ASSERT2( isCoVar tyvar || typeKind ty `isSubKind` tyVarKind tyvar,
(ppr tyvar <+> ppr (tyVarKind tyvar))
$$ (ppr ty <+> ppr (typeKind ty)) )
do { if debugIsOn then do { details <- readMetaTyVar tyvar;
-- FIXME ; ASSERT2( not (isFlexi details), ppr tyvar )
; WARN( not (isFlexi details), ppr tyvar )
return () }
else return ()
-- Temporarily make this a warning, until we fix Trac #2999
; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty)
; writeMutVar (metaTvRef tyvar) (Indirect ty) }
where
_k1 = tyVarKind tyvar
_k2 = typeKind ty
\end{code}
......
......@@ -9,6 +9,8 @@ module TcRnMonad(
module IOEnv
) where
#include "HsVersions.h"
import TcRnTypes -- Re-export all
import IOEnv -- Re-export all
......@@ -123,7 +125,9 @@ initTc hsc_env hsc_src keep_rn_syntax mod do_this
tcl_arrow_ctxt = NoArrowCtxt,
tcl_env = emptyNameEnv,
tcl_tyvars = tvs_var,
tcl_lie = panic "initTc:LIE" -- LIE only valid inside a getLIE
tcl_lie = panic "initTc:LIE", -- only valid inside getLIE
tcl_tybinds = panic "initTc:tybinds"
-- only valid inside a getTyBinds
} ;
} ;
......@@ -823,7 +827,7 @@ debugTc thing
| otherwise = return ()
\end{code}
%************************************************************************
%************************************************************************
%* *
Type constraints (the so-called LIE)
%* *
......@@ -879,6 +883,44 @@ setLclTypeEnv lcl_env thing_inside
\end{code}
%************************************************************************
%* *
Meta type variable bindings
%* *
%************************************************************************
\begin{code}
getTcTyVarBindsVar :: TcM (TcRef TcTyVarBinds)
getTcTyVarBindsVar = do { env <- getLclEnv; return (tcl_tybinds env) }
getTcTyVarBinds :: TcM a -> TcM (a, TcTyVarBinds)
getTcTyVarBinds thing_inside
= do { tybinds_var <- newMutVar emptyBag
; res <- updLclEnv (\ env -> env { tcl_tybinds = tybinds_var })
thing_inside
; tybinds <- readMutVar tybinds_var
; return (res, tybinds)
}
bindMetaTyVar :: TcTyVar -> TcType -> TcM ()
bindMetaTyVar tv ty
= do { ASSERTM2( do { details <- readMutVar (metaTvRef tv)
; return (isFlexi details) }, ppr tv )
; tybinds_var <- getTcTyVarBindsVar
; tybinds <- readMutVar tybinds_var
; writeMutVar tybinds_var (tybinds `snocBag` TcTyVarBind tv ty)
}
getTcTyVarBindsRelation :: TcM [(TcTyVar, TcTyVarSet)]
getTcTyVarBindsRelation
= do { tybinds_var <- getTcTyVarBindsVar
; tybinds <- readMutVar tybinds_var
; return $ map freeTvs (bagToList tybinds)
}
where
freeTvs (TcTyVarBind tv ty) = (tv, tyVarsOfType ty)
\end{code}
%************************************************************************
%* *
Template Haskell context
......
......@@ -34,7 +34,7 @@ module TcRnTypes(
plusLIEs, mkLIE, isEmptyLIE, lieToList, listToLIE,
-- Misc other types
TcId, TcIdSet, TcDictBinds,
TcId, TcIdSet, TcDictBinds, TcTyVarBind(..), TcTyVarBinds
) where
......@@ -98,6 +98,18 @@ type RnM a = TcRn a -- Historical
type TcM a = TcRn a -- Historical
\end{code}
Representation of type bindings to uninstantiated meta variables used during
constraint solving.
\begin{code}
data TcTyVarBind = TcTyVarBind TcTyVar TcType
type TcTyVarBinds = Bag TcTyVarBind
instance Outputable TcTyVarBind where
ppr (TcTyVarBind tv ty) = ppr tv <+> text ":=" <+> ppr ty
\end{code}
%************************************************************************
%* *
......@@ -343,15 +355,20 @@ data TcLclEnv -- Changes as we move inside an expression
-- We still need the unsullied global name env so that
-- we can look up record field names
tcl_env :: NameEnv TcTyThing, -- The local type environment: Ids and TyVars
-- defined in this module
tcl_env :: NameEnv TcTyThing, -- The local type environment: Ids and
-- TyVars defined in this module
tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
-- Namely, the in-scope TyVars bound in tcl_env,
-- plus the tyvars mentioned in the types of Ids bound in tcl_lenv
-- Why mutable? see notes with tcGetGlobalTyVars
-- plus the tyvars mentioned in the types of Ids bound
-- in tcl_lenv.
-- Why mutable? see notes with tcGetGlobalTyVars
tcl_lie :: TcRef LIE, -- Place to accumulate type constraints
tcl_lie :: TcRef LIE -- Place to accumulate type constraints
tcl_tybinds :: TcRef TcTyVarBinds -- Meta and coercion type variable
-- bindings accumulated during
-- constraint solving
}
......
......@@ -1115,7 +1115,9 @@ checkLoop env wanteds
; env' <- zonkRedEnv env
; wanteds' <- zonkInsts wanteds
; (improved, binds, irreds) <- reduceContext env' wanteds'
; (improved, tybinds, binds, irreds)
<- reduceContext env' wanteds'
; execTcTyVarBinds tybinds
; if null irreds || not improved then
return (irreds, binds)
......@@ -1450,7 +1452,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-- HOWEVER, some unification may take place, if we instantiate
-- a method Inst with an equality constraint
; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z
; (_imp, _tybinds, _binds, constrained_dicts)
<- reduceContext env wanteds_z
-- Next, figure out the tyvars we will quantify over
; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
......@@ -1478,13 +1481,6 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
ppr _binds,
ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
-- Zonk wanteds again! The first call to reduceContext may have
-- instantiated some variables.
-- FIXME: If red_improve would work, we could propagate that into
-- the equality solver, too, to prevent instantating any
-- variables.
; wanteds_zz <- zonkInsts wanteds_z
-- The first step may have squashed more methods than
-- necessary, so try again, this time more gently, knowing the exact
-- set of type variables to quantify over.
......@@ -1506,7 +1502,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
(is_nested_group || isDict inst) = Stop
| otherwise = ReduceMe
env = mkNoImproveRedEnv doc try_me
; (_imp, binds, irreds) <- reduceContext env wanteds_zz
; (_imp, tybinds, binds, irreds) <- reduceContext env wanteds_z
; execTcTyVarBinds tybinds
-- See "Notes on implicit parameters, Question 4: top level"
; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
......@@ -1683,7 +1680,8 @@ tcSimplifyIPs given_ips wanteds
-- Unusually for checking, we *must* zonk the given_ips
; let env = mkRedEnv doc try_me given_ips'
; (improved, binds, irreds) <- reduceContext env wanteds'
; (improved, tybinds, binds, irreds) <- reduceContext env wanteds'
; execTcTyVarBinds tybinds
; if null irreds || not improved then
ASSERT( all is_free irreds )
......@@ -1872,6 +1870,7 @@ discharge with the explicit instance.
reduceContext :: RedEnv
-> [Inst] -- Wanted
-> TcM (ImprovementDone,
TcTyVarBinds, -- Type variable bindings
TcDictBinds, -- Dictionary bindings
[Inst]) -- Irreducible
......@@ -1898,10 +1897,11 @@ reduceContext env wanteds0
givens = red_givens env
; (givens',
wanteds',
normalise_binds,
eq_improved) <- tcReduceEqs givens wanteds
tybinds,
normalise_binds) <- tcReduceEqs givens wanteds
; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
[ppr givens', ppr wanteds', ppr normalise_binds]
[ppr givens', ppr wanteds', ppr tybinds,
ppr normalise_binds]
-- Build the Avail mapping from "given_dicts"
; (init_state, _) <- getLIE $ do
......@@ -1941,7 +1941,7 @@ reduceContext env wanteds0
-- Collect all irreducible instances, and determine whether we should
-- go round again. We do so in either of two cases:
-- (1) If dictionary reduction or equality solving led to
-- improvement (i.e., instantiated type variables).
-- improvement (i.e., bindings for type variables).
-- (2) If we reduced dictionaries (i.e., got dictionary bindings),
-- they may have exposed further opportunities to normalise
-- family applications. See Note [Dictionary Improvement]
......@@ -1954,6 +1954,7 @@ reduceContext env wanteds0
; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
avails_improved = availsImproved avails
eq_improved = anyBag (not . isCoVarBind) tybinds
improvedFlexible = avails_improved || eq_improved
reduced_dicts = not (isEmptyBag dict_binds)
improved = improvedFlexible || reduced_dicts
......@@ -1967,6 +1968,7 @@ reduceContext env wanteds0
text "given" <+> ppr givens,
text "wanted" <+> ppr wanteds0,
text "----",
text "tybinds" <+> ppr tybinds,
text "avails" <+> pprAvails avails,
text "improved =" <+> ppr improved <+> text improvedHint,
text "(all) irreds = " <+> ppr all_irreds,
......@@ -1976,10 +1978,13 @@ reduceContext env wanteds0
]))
; return (improved,
tybinds,
normalise_binds `unionBags` dict_binds
`unionBags` implic_binds,
all_irreds)
}
where
isCoVarBind (TcTyVarBind tv _) = isCoVar tv
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
......
This diff is collapsed.
......@@ -124,7 +124,8 @@ module TcType (
typeKind, tidyKind,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
tcTyVarsOfType, tcTyVarsOfTypes, exactTyVarsOfType, exactTyVarsOfTypes,
tcTyVarsOfType, tcTyVarsOfTypes, tcTyVarsOfPred, exactTyVarsOfType,
exactTyVarsOfTypes,
pprKind, pprParendKind,
pprType, pprParendType, pprTypeApp, pprTyThingCategory,
......
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