From: simonpj Date: Tue, 30 Jan 2001 09:53:12 +0000 (+0000) Subject: [project @ 2001-01-30 09:53:11 by simonpj] X-Git-Tag: Approximately_9120_patches~2780 X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=ade2eac4257679a3ac152a39df87ce8567bd7766;p=ghc-hetmet.git [project @ 2001-01-30 09:53:11 by simonpj] More on functional dependencies My last commit allowed this: instance C a b => C [a] [b] where ... if we have class C a b | a -> b This commit completes the change, by making the improvement stages improve only the 'shape' of the second argument of C. I also had to change the iteration in TcSimplify -- see the comments in TcSimplify.inferLoop. --- diff --git a/ghc/compiler/typecheck/TcMonad.lhs b/ghc/compiler/typecheck/TcMonad.lhs index b25242c..504f5da 100644 --- a/ghc/compiler/typecheck/TcMonad.lhs +++ b/ghc/compiler/typecheck/TcMonad.lhs @@ -268,7 +268,9 @@ forkNF_Tc m down@(TcDown { tc_us = u_var }) env \begin{code} traceTc :: SDoc -> NF_TcM () -traceTc doc down env = printDump doc +traceTc doc (TcDown { tc_dflags=dflags }) env + | dopt Opt_D_dump_rn_trace dflags = printDump doc + | otherwise = return () ioToTc :: IO a -> NF_TcM a ioToTc io down env = io diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index b8db28d..e81409a 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -31,13 +31,13 @@ import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..), 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 ) @@ -50,7 +50,7 @@ import Type ( Type, ClassContext, mkTyVarTy, getTyVar, isTyVarTy, splitSigmaTy, tyVarsOfTypes ) -import Subst ( mkTopTyVarSubst, substClasses ) +import Subst ( mkTopTyVarSubst, substClasses, substTy ) import PprType ( pprClassPred ) import TysWiredIn ( unitTy ) import VarSet @@ -395,7 +395,7 @@ tcSimplifyInfer doc tau_tvs wanted_lie -- 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 @@ -418,9 +418,31 @@ inferLoop doc tau_tvs wanteds 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 @@ -454,7 +476,7 @@ tcSimplifyCheck doc qtvs givens wanted_lie complainCheck doc givens irreds `thenNF_Tc_` -- Done - returnTc (mkLIE frees, binds) + returnTc (frees, binds) checkLoop doc qtvs givens wanteds = -- Step 1 @@ -474,7 +496,8 @@ checkLoop doc qtvs givens wanteds 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' -> @@ -514,7 +537,7 @@ tcSimplifyInferCheck doc tau_tvs givens wanted complainCheck doc givens irreds `thenNF_Tc_` -- Done - returnTc (qtvs, mkLIE frees, binds) + returnTc (qtvs, frees, binds) inferCheckLoop doc tau_tvs givens wanteds = -- Step 1 @@ -550,7 +573,8 @@ inferCheckLoop doc tau_tvs givens wanteds 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} @@ -588,7 +612,7 @@ tcSimplifyToDicts wanted_lie = 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 @@ -622,7 +646,7 @@ tcSimplifyIPs ip_names wanted_lie -- 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 @@ -672,7 +696,7 @@ bindInstsOfLocalFuns init_lie local_ids | 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 @@ -740,7 +764,8 @@ data Avail 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 @@ -812,7 +837,7 @@ The "given" set is always empty. 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 @@ -822,7 +847,8 @@ simpleReduceLoop doc try_me wanteds 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} @@ -833,13 +859,13 @@ reduceContext :: SDoc -> [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, @@ -847,7 +873,6 @@ reduceContext doc try_me givens wanteds text "----------------------" ])) `thenNF_Tc_` --} -- Build the Avail mapping from "givens" foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state -> @@ -858,7 +883,6 @@ reduceContext doc try_me givens wanteds -- In particular, avails includes all superclasses of everything tcImprove avails `thenTc` \ no_improvement -> -{- traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", doc, @@ -870,11 +894,10 @@ reduceContext doc try_me givens wanteds 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 -> @@ -890,8 +913,14 @@ tcImprove avails 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. @@ -1143,7 +1172,7 @@ It's OK: the final zonking stage should zap y to (), which is fine. 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 @@ -1235,7 +1264,7 @@ disambigGroup dicts 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 diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs index f089e98..627db87 100644 --- a/ghc/compiler/types/FunDeps.lhs +++ b/ghc/compiler/types/FunDeps.lhs @@ -16,11 +16,12 @@ import Var ( TyVar ) 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} @@ -142,8 +143,16 @@ grow preds fixed_tvs \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 @@ -199,7 +208,7 @@ checkGroup :: InstEnv a -> [PredType] -> [Equation] 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 @@ -223,7 +232,7 @@ checkGroup inst_env clss@(Class cls tys : _) -- 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, @@ -231,7 +240,7 @@ checkGroup inst_env clss@(Class cls tys : _) 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, @@ -252,13 +261,16 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 -- 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 diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs index d535bb0..b284a6f 100644 --- a/ghc/compiler/types/Unify.lhs +++ b/ghc/compiler/types/Unify.lhs @@ -7,7 +7,8 @@ This module contains a unifier and a matcher, both of which use an explicit substitution \begin{code} -module Unify ( unifyTysX, unifyTyListsX, allDistinctTyVars, +module Unify ( unifyTysX, unifyTyListsX, unifyExtendTysX, + allDistinctTyVars, match, matchTy, matchTys, ) where @@ -84,6 +85,14 @@ unifyTysX :: TyVarSet -- Template tyvars unifyTysX tmpl_tyvars ty1 ty2 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv) +unifyExtendTysX :: TyVarSet -- Template tyvars + -> TyVarSubstEnv -- Substitution to start with + -> Type + -> Type + -> Maybe TyVarSubstEnv -- Extended substitution +unifyExtendTysX tmpl_tyvars subst ty1 ty2 + = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst) + unifyTyListsX :: TyVarSet -> [Type] -> [Type] -> Maybe TyVarSubstEnv unifyTyListsX tmpl_tyvars tys1 tys2