getDictClassTys, getIPs, isTyVarDict,
instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
Inst, LIE, pprInsts, pprInstsInFull,
- mkLIE,
+ mkLIE, plusLIE, isEmptyLIE,
lieToList
)
import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-import TcType ( zonkTcTyVarsAndFV )
+import TcType ( zonkTcTyVarsAndFV, tcInstTyVars )
import TcUnify ( unifyTauTy )
import Id ( idType )
import Name ( Name )
mkTyVarTy, getTyVar,
isTyVarTy, splitSigmaTy, tyVarsOfTypes
)
-import Subst ( mkTopTyVarSubst, substClasses )
+import Subst ( mkTopTyVarSubst, substClasses, substTy )
import PprType ( pprClassPred )
import TysWiredIn ( unitTy )
import VarSet
-- Check for non-generalisable insts
mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
- returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
+ returnTc (qtvs, frees, binds, map instToId irreds)
inferLoop doc tau_tvs wanteds
= -- Step 1
if no_improvement then
returnTc (varSetElems qtvs, frees, binds, irreds)
else
- inferLoop doc tau_tvs wanteds
+ -- We start again with irreds, not wanteds
+ -- Using an instance decl might have introduced a fresh type variable
+ -- which might have been unified, so we'd get an infinite loop
+ -- if we started again with wanteds! See example [LOOP]
+ inferLoop doc tau_tvs irreds `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+ returnTc (qtvs1, frees1 `plusLIE` frees, binds `AndMonoBinds` binds1, irreds1)
\end{code}
+Example [LOOP]
+
+ class If b t e r | b t e -> r
+ instance If T t e t
+ instance If F t e e
+ class Lte a b c | a b -> c where lte :: a -> b -> c
+ instance Lte Z b T
+ instance (Lte a b l,If l b a c) => Max a b c
+
+Wanted: Max Z (S x) y
+
+Then we'll reduce using the Max instance to:
+ (Lte Z (S x) l, If l (S x) Z y)
+and improve by binding l->T, after which we can do some reduction
+on both the Lte and If constraints. What we *can't* do is start again
+with (Max Z (S x) y)!
+
\begin{code}
isFree qtvs inst
= not (tyVarsOfInst inst `intersectsVarSet` qtvs) -- Constrains no quantified vars
complainCheck doc givens irreds `thenNF_Tc_`
-- Done
- returnTc (mkLIE frees, binds)
+ returnTc (frees, binds)
checkLoop doc qtvs givens wanteds
= -- Step 1
if no_improvement then
returnTc (frees, binds, irreds)
else
- checkLoop doc qtvs givens wanteds
+ checkLoop doc qtvs givens irreds `thenTc` \ (frees1, binds1, irreds1) ->
+ returnTc (frees `plusLIE` frees1, binds `AndMonoBinds` binds1, irreds1)
complainCheck doc givens irreds
= mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
complainCheck doc givens irreds `thenNF_Tc_`
-- Done
- returnTc (qtvs, mkLIE frees, binds)
+ returnTc (qtvs, frees, binds)
inferCheckLoop doc tau_tvs givens wanteds
= -- Step 1
if no_improvement then
returnTc (varSetElems qtvs, frees, binds, irreds)
else
- inferCheckLoop doc tau_tvs givens wanteds
+ inferCheckLoop doc tau_tvs givens wanteds `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+ returnTc (qtvs1, frees1 `plusLIE` frees, binds `AndMonoBinds` binds1, irreds1)
\end{code}
= simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
-- Since try_me doesn't look at types, we don't need to
-- do any zonking, so it's safe to call reduceContext directly
- ASSERT( null frees )
+ ASSERT( isEmptyLIE frees )
returnTc (irreds, binds)
where
-- The irreducible ones should be a subset of the implicit
-- parameters we provided
ASSERT( all here_ip irreds )
- returnTc (mkLIE frees, binds)
+ returnTc (frees, binds)
where
doc = text "tcSimplifyIPs" <+> ppr ip_names
| otherwise
= simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
ASSERT( null irreds )
- returnTc (mkLIE frees, binds)
+ returnTc (frees, binds)
where
doc = text "bindInsts" <+> ppr local_ids
wanteds = lieToList init_lie
TcExpr -- The RHS
[Inst] -- Insts free in the RHS; we need these too
-pprAvails avails = vcat (map pprAvail (eltsFM avails))
+pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+ | (inst,avail) <- fmToList avails ]
instance Outputable Avail where
ppr = pprAvail
simpleReduceLoop :: SDoc
-> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
-> [Inst] -- Wanted
- -> TcM ([Inst], -- Free
+ -> TcM (LIE, -- Free
TcDictBinds,
[Inst]) -- Irreducible
if no_improvement then
returnTc (frees, binds, irreds)
else
- simpleReduceLoop doc try_me wanteds
+ simpleReduceLoop doc try_me irreds `thenTc` \ (frees1, binds1, irreds1) ->
+ returnTc (frees `plusLIE` frees1, binds `AndMonoBinds` binds1, irreds1)
\end{code}
-> [Inst] -- Given
-> [Inst] -- Wanted
-> NF_TcM (Bool, -- True <=> improve step did no unification
- [Inst], -- Free
+ LIE, -- Free
TcDictBinds, -- Dictionary bindings
[Inst]) -- Irreducible
reduceContext doc try_me givens wanteds
=
-{- traceTc (text "reduceContext" <+> (vcat [
+ traceTc (text "reduceContext" <+> (vcat [
text "----------------------",
doc,
text "given" <+> ppr givens,
text "----------------------"
])) `thenNF_Tc_`
--}
-- Build the Avail mapping from "givens"
foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
-- In particular, avails includes all superclasses of everything
tcImprove avails `thenTc` \ no_improvement ->
-{-
traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
doc,
text "no_improvement =" <+> ppr no_improvement,
text "----------------------"
])) `thenNF_Tc_`
--}
let
(binds, irreds) = bindsAndIrreds avails wanteds
in
- returnTc (no_improvement, frees, binds, irreds)
+ returnTc (no_improvement, mkLIE frees, binds, irreds)
tcImprove avails
= tcGetInstEnv `thenTc` \ inst_env ->
if null eqns then
returnTc True
else
- mapTc_ (\ (t1,t2) -> unifyTauTy t1 t2) eqns `thenTc_`
+ traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns)) `thenNF_Tc_`
+ mapTc_ unify eqns `thenTc_`
returnTc False
+ where
+ unify (qtvs, t1, t2) = tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
+ unifyTauTy (substTy tenv t1) (substTy tenv t2)
+ ppr_eqn (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) <+>
+ ppr t1 <+> equals <+> ppr t2
\end{code}
The main context-reduction function is @reduce@. Here's its game plan.
tcSimplifyTop :: LIE -> TcM TcDictBinds
tcSimplifyTop wanted_lie
= simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
- ASSERT( null frees )
+ ASSERT( isEmptyLIE frees )
let
-- All the non-std ones are definite errors
unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
simpleReduceLoop (text "disambig" <+> ppr dicts)
try_me dicts `thenTc` \ (frees, binds, ambigs) ->
- WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
+ WARN( not (isEmptyLIE frees && null ambigs), ppr frees $$ ppr ambigs )
warnDefault dicts chosen_default_ty `thenTc_`
returnTc binds
import Class ( Class, FunDep, classTvsFds )
import Type ( Type, ThetaType, PredType(..), predTyUnique, tyVarsOfTypes, tyVarsOfPred )
import Subst ( mkSubst, emptyInScopeSet, substTy )
-import Unify ( unifyTyListsX )
+import Unify ( unifyTyListsX, unifyExtendTysX )
import Outputable ( Outputable, SDoc, interppSP, ptext, empty, hsep, punctuate, comma )
import VarSet
import VarEnv
import List ( tails )
+import Maybes ( maybeToBool )
import ListSetOps ( equivClassesByUniq )
\end{code}
\begin{code}
----------
-type Equation = (Type,Type) -- These two types should be equal
- -- INVARIANT: they aren't already equal
+type Equation = (TyVarSet, Type,Type) -- These two types should be equal, for some
+ -- substitution of the tyvars in the tyvar set
+ -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
+ -- We unify z with Int, but since a and b are quantified we do nothing to them
+ -- We usually act on an equation by instantiating the quantified type varaibles
+ -- to fresh type variables, and then calling the standard unifier.
+ --
+ -- INVARIANT: they aren't already equal
+
+
----------
improve :: InstEnv a -- Gives instances for given class
checkGroup inst_env (IParam _ ty : ips)
= -- For implicit parameters, all the types must match
- [(ty, ty') | IParam _ ty' <- ips, ty /= ty']
+ [(emptyVarSet, ty, ty') | IParam _ ty' <- ips, ty /= ty']
checkGroup inst_env clss@(Class cls tys : _)
= -- For classes life is more complicated
-- NOTE that we iterate over the fds first; they are typically
-- empty, which aborts the rest of the loop.
- pairwise_eqns :: [(Type,Type)]
+ pairwise_eqns :: [Equation]
pairwise_eqns -- This group comes from pairwise comparison
= [ eqn | fd <- cls_fds,
Class _ tys1 : rest <- tails clss,
eqn <- checkClsFD emptyVarSet fd cls_tvs tys1 tys2
]
- instance_eqns :: [(Type,Type)]
+ instance_eqns :: [Equation]
instance_eqns -- This group comes from comparing with instance decls
= [ eqn | fd <- cls_fds,
(qtvs, tys1, _) <- cls_inst_env,
-- unifyTyListsX will only bind variables in qtvs, so it's OK!
= case unifyTyListsX qtvs ls1 ls2 of
Nothing -> []
- Just unif -> [(sr1, sr2) | (r1,r2) <- rs1 `zip` rs2,
- let sr1 = substTy full_unif r1,
- let sr2 = substTy full_unif r2,
- sr1 /= sr2]
+ Just unif -> [ (qtvs', substTy full_unif r1, substTy full_unif r2)
+ | (r1,r2) <- rs1 `zip` rs2,
+ not (maybeToBool (unifyExtendTysX qtvs unif r1 r2))]
where
full_unif = mkSubst emptyInScopeSet unif
-- No for-alls in sight; hmm
+
+ qtvs' = filterVarSet (\v -> not (v `elemSubstEnv` unif)) qtvs
+ -- qtvs' are the quantified type variables
+ -- that have not been substituted out
where
(ls1, rs1) = instFD fd clas_tvs tys1
(ls2, rs2) = instFD fd clas_tvs tys2
projects / ghc-hetmet.git / commitdiff