From c45a0ac5fdc6a931c3bc1a45fd4967f54c2983ca Mon Sep 17 00:00:00 2001 From: simonpj Date: Mon, 20 Dec 2004 17:17:10 +0000 Subject: [PATCH] [project @ 2004-12-20 17:16:24 by simonpj] -------------------------------- Deal properly with dual-renaming -------------------------------- When comparing types and terms, and during matching, we are faced with \x.e1 ~ \y.e2 There are many pitfalls here, and GHC has never done the job properly. Now, at last it does, using a new abstraction VarEnv.RnEnv2. See comments there for how it works. There are lots of consequential changes to use the new stuff, especially in types/Type (type comparison), types/Unify (matching on types) coreSyn/CoreUtils (equality on expressions), specialise/Rules (matching). I'm not 100% certain of that I've covered all the bases, so let me know if something unexpected happens after you update. Maybe wait until a nightly build has worked ok first! --- ghc/compiler/basicTypes/VarEnv.lhs | 126 +++++++++- ghc/compiler/coreSyn/CoreLint.lhs | 4 +- ghc/compiler/coreSyn/CoreUtils.lhs | 102 ++++---- ghc/compiler/coreSyn/Subst.lhs | 5 +- ghc/compiler/deSugar/DsForeign.lhs | 6 +- ghc/compiler/prelude/PrelRules.lhs | 4 +- ghc/compiler/simplCore/Simplify.lhs | 4 +- ghc/compiler/specialise/Rules.lhs | 429 +++++++++++++------------------- ghc/compiler/specialise/SpecConstr.lhs | 4 +- ghc/compiler/stranal/DmdAnal.lhs | 4 +- ghc/compiler/typecheck/TcBinds.lhs | 10 +- ghc/compiler/typecheck/TcSimplify.lhs | 2 +- ghc/compiler/typecheck/TcType.lhs | 98 +------- ghc/compiler/types/Type.lhs | 149 ++++++++--- ghc/compiler/types/Unify.lhs | 319 +++++++++++++++--------- ghc/compiler/utils/Maybes.lhs | 29 +-- ghc/compiler/utils/Util.lhs | 18 +- 17 files changed, 714 insertions(+), 599 deletions(-) diff --git a/ghc/compiler/basicTypes/VarEnv.lhs b/ghc/compiler/basicTypes/VarEnv.lhs index 3c7f7f0..f29b940 100644 --- a/ghc/compiler/basicTypes/VarEnv.lhs +++ b/ghc/compiler/basicTypes/VarEnv.lhs @@ -23,6 +23,10 @@ module VarEnv ( extendInScopeSet, extendInScopeSetList, modifyInScopeSet, getInScopeVars, lookupInScope, elemInScopeSet, uniqAway, + -- RnEnv2 and its operations + RnEnv2, mkRnEnv2, rnBndr2, rnBndrs2, rnOccL, rnOccR, inRnEnvL, inRnEnvR, + rnBndrL, rnBndrR, nukeRnEnvL, nukeRnEnvR, + -- TidyEnvs TidyEnv, emptyTidyEnv ) where @@ -34,7 +38,8 @@ import Var ( Var, setVarUnique ) import VarSet import UniqFM import Unique ( Unique, deriveUnique, getUnique ) -import Util ( zipEqual ) +import Util ( zipEqual, foldl2 ) +import Maybes ( orElse, isJust ) import CmdLineOpts ( opt_PprStyle_Debug ) import Outputable import FastTypes @@ -105,9 +110,14 @@ uniqAway :: InScopeSet -> Var -> Var -- in-scope set, and gives that to v. It starts with v's current unique, of course, -- in the hope that it won't have to change it, and thereafter uses a combination -- of that and the hash-code found in the in-scope set -uniqAway (InScope set n) var - | not (var `elemVarSet` set) = var -- Nothing to do - | otherwise = try 1# +uniqAway in_scope var + | var `elemInScopeSet` in_scope = uniqAway' in_scope var -- Make a new one + | otherwise = var -- Nothing to do + +uniqAway' :: InScopeSet -> Var -> Var +-- This one *always* makes up a new variable +uniqAway' (InScope set n) var + = try 1# where orig_unique = getUnique var try k @@ -129,6 +139,110 @@ uniqAway (InScope set n) var %************************************************************************ %* * + Dual renaming +%* * +%************************************************************************ + +When we are comparing (or matching) types or terms, we are faced with +"going under" corresponding binders. E.g. when comparing + \x. e1 ~ \y. e2 + +Basically we want to rename [x->y] or [y->x], but there are lots of +things we must be careful of. In particular, x might be free in e2, or +y in e1. So the idea is that we come up with a fresh binder that is free +in neither, and rename x and y respectively. That means we must maintain + a) a renaming for the left-hand expression + b) a renaming for the right-hand expressions + c) an in-scope set + +Furthermore, when matching, we want to be able to have an 'occurs check', +to prevent + \x. f ~ \y. y +matching with f->y. So for each expression we want to know that set of +locally-bound variables. That is precisely the domain of the mappings (a) +and (b), but we must ensure that we always extend the mappings as we go in. + + +\begin{code} +data RnEnv2 + = RV2 { envL :: VarEnv Var -- Renaming for Left term + , envR :: VarEnv Var -- Renaming for Right term + , in_scope :: InScopeSet } -- In scope in left or right terms + +-- The renamings envL and envR are *guaranteed* to contain a binding +-- for every variable bound as we go into the term, even if it is not +-- renamed. That way we can ask what variables are locally bound +-- (inRnEnvL, inRnEnvR) + +mkRnEnv2 :: InScopeSet -> RnEnv2 +mkRnEnv2 vars = RV2 { envL = emptyVarEnv + , envR = emptyVarEnv + , in_scope = vars } + +rnBndrs2 :: RnEnv2 -> [Var] -> [Var] -> RnEnv2 +-- Arg lists must be of equal length +rnBndrs2 env bsL bsR = foldl2 rnBndr2 env bsL bsR + +rnBndr2 :: RnEnv2 -> Var -> Var -> RnEnv2 +-- (rnBndr2 env bL bR) go under a binder bL in the Left term 1, +-- and binder bR in the Right term +-- It finds a new binder, new_b, +-- and returns an environment mapping bL->new_b and bR->new_b resp. +rnBndr2 (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bL bR + = RV2 { envL = extendVarEnv envL bL new_b -- See Note + , envR = extendVarEnv envR bR new_b -- [Rebinding] + , in_scope = extendInScopeSet in_scope new_b } + where + -- Find a new binder not in scope in either term + new_b | not (bL `elemInScopeSet` in_scope) = bL + | not (bR `elemInScopeSet` in_scope) = bR + | otherwise = uniqAway' in_scope bL + + -- Note [Rebinding] + -- If the new var is the same as the old one, note that + -- the extendVarEnv *deletes* any current renaming + -- E.g. (\x. \x. ...) ~ (\y. \z. ...) + -- + -- Inside \x \y { [x->y], [y->y], {y} } + -- \x \z { [x->x], [y->y, z->x], {y,x} } + +rnBndrL, rnBndrR :: RnEnv2 -> Var -> (RnEnv2, Var) +-- Used when there's a binder on one side or the other only +-- Useful when eta-expanding +rnBndrL (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bL + = (RV2 { envL = extendVarEnv envL bL new_b + , envR = envR + , in_scope = extendInScopeSet in_scope new_b }, new_b) + where + new_b | not (bL `elemInScopeSet` in_scope) = bL + | otherwise = uniqAway' in_scope bL + +rnBndrR (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bR + = (RV2 { envL = envL + , envR = extendVarEnv envR bR new_b + , in_scope = extendInScopeSet in_scope new_b }, new_b) + where + new_b | not (bR `elemInScopeSet` in_scope) = bR + | otherwise = uniqAway' in_scope bR + +rnOccL, rnOccR :: RnEnv2 -> Var -> Var +-- Look up the renaming of an occurrence in the left or right term +rnOccL (RV2 { envL = env }) v = lookupVarEnv env v `orElse` v +rnOccR (RV2 { envR = env }) v = lookupVarEnv env v `orElse` v + +inRnEnvL, inRnEnvR :: RnEnv2 -> Var -> Bool +-- Tells whether a variable is locally bound +inRnEnvL (RV2 { envL = env }) v = isJust (lookupVarEnv env v) +inRnEnvR (RV2 { envR = env }) v = isJust (lookupVarEnv env v) + +nukeRnEnvL, nukeRnEnvR :: RnEnv2 -> RnEnv2 +nukeRnEnvL env = env { envL = emptyVarEnv } +nukeRnEnvR env = env { envR = emptyVarEnv } +\end{code} + + +%************************************************************************ +%* * Tidying %* * %************************************************************************ @@ -202,8 +316,8 @@ foldVarEnv = foldUFM lookupVarEnv_Directly = lookupUFM_Directly filterVarEnv_Directly = filterUFM_Directly -zipVarEnv tyvars tys = mkVarEnv (zipEqual "zipVarEnv" tyvars tys) -lookupVarEnv_NF env id = case (lookupVarEnv env id) of { Just xx -> xx } +zipVarEnv tyvars tys = mkVarEnv (zipEqual "zipVarEnv" tyvars tys) +lookupVarEnv_NF env id = case (lookupVarEnv env id) of { Just xx -> xx } \end{code} @modifyVarEnv@: Look up a thing in the VarEnv, diff --git a/ghc/compiler/coreSyn/CoreLint.lhs b/ghc/compiler/coreSyn/CoreLint.lhs index dfc6fe8..5783a7f 100644 --- a/ghc/compiler/coreSyn/CoreLint.lhs +++ b/ghc/compiler/coreSyn/CoreLint.lhs @@ -27,7 +27,7 @@ import PprCore import ErrUtils ( dumpIfSet_core, ghcExit, Message, showPass, mkLocMessage, debugTraceMsg ) import SrcLoc ( SrcLoc, noSrcLoc, mkSrcSpan ) -import Type ( Type, tyVarsOfType, eqType, +import Type ( Type, tyVarsOfType, coreEqType, splitFunTy_maybe, mkTyVarTys, splitForAllTy_maybe, splitTyConApp_maybe, isUnLiftedType, typeKind, @@ -615,7 +615,7 @@ checkTys :: Type -> Type -> Message -> LintM () -- check ty2 is subtype of ty1 (ie, has same structure but usage -- annotations need only be consistent, not equal) -- Assumes ty1,ty2 are have alrady had the substitution applied -checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg +checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg \end{code} %************************************************************************ diff --git a/ghc/compiler/coreSyn/CoreUtils.lhs b/ghc/compiler/coreSyn/CoreUtils.lhs index 043be8e..77f2156 100644 --- a/ghc/compiler/coreSyn/CoreUtils.lhs +++ b/ghc/compiler/coreSyn/CoreUtils.lhs @@ -31,7 +31,7 @@ module CoreUtils ( hashExpr, -- Equality - cheapEqExpr, eqExpr, applyTypeToArgs, applyTypeToArg + cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg ) where #include "HsVersions.h" @@ -40,8 +40,10 @@ module CoreUtils ( import GLAEXTS -- For `xori` import CoreSyn +import CoreFVs ( exprFreeVars ) import PprCore ( pprCoreExpr ) import Var ( Var ) +import VarSet ( unionVarSet ) import VarEnv import Name ( hashName ) import Packages ( isDllName ) @@ -59,10 +61,10 @@ import Id ( Id, idType, globalIdDetails, idNewStrictness, import IdInfo ( GlobalIdDetails(..), megaSeqIdInfo ) import NewDemand ( appIsBottom ) import Type ( Type, mkFunTy, mkForAllTy, splitFunTy_maybe, - splitFunTy, + splitFunTy, tcEqTypeX, applyTys, isUnLiftedType, seqType, mkTyVarTy, splitForAllTy_maybe, isForAllTy, splitRecNewType_maybe, - splitTyConApp_maybe, eqType, funResultTy, applyTy + splitTyConApp_maybe, coreEqType, funResultTy, applyTy ) import TyCon ( tyConArity ) -- gaw 2004 @@ -72,7 +74,7 @@ import BasicTypes ( Arity ) import Unique ( Unique ) import Outputable import TysPrim ( alphaTy ) -- Debugging only -import Util ( equalLength, lengthAtLeast ) +import Util ( equalLength, lengthAtLeast, foldl2 ) \end{code} @@ -205,12 +207,12 @@ mkCoerce to_ty expr = mkCoerce2 to_ty (exprType expr) expr mkCoerce2 :: Type -> Type -> CoreExpr -> CoreExpr mkCoerce2 to_ty from_ty (Note (Coerce to_ty2 from_ty2) expr) - = ASSERT( from_ty `eqType` to_ty2 ) + = ASSERT( from_ty `coreEqType` to_ty2 ) mkCoerce2 to_ty from_ty2 expr mkCoerce2 to_ty from_ty expr - | to_ty `eqType` from_ty = expr - | otherwise = ASSERT( from_ty `eqType` exprType expr ) + | to_ty `coreEqType` from_ty = expr + | otherwise = ASSERT( from_ty `coreEqType` exprType expr ) Note (Coerce to_ty from_ty) expr \end{code} @@ -1003,7 +1005,7 @@ cheapEqExpr :: Expr b -> Expr b -> Bool cheapEqExpr (Var v1) (Var v2) = v1==v2 cheapEqExpr (Lit lit1) (Lit lit2) = lit1 == lit2 -cheapEqExpr (Type t1) (Type t2) = t1 `eqType` t2 +cheapEqExpr (Type t1) (Type t2) = t1 `coreEqType` t2 cheapEqExpr (App f1 a1) (App f2 a2) = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2 @@ -1021,57 +1023,49 @@ exprIsBig other = True \begin{code} -eqExpr :: CoreExpr -> CoreExpr -> Bool - -- Works ok at more general type, but only needed at CoreExpr - -- Used in rule matching, so when we find a type we use - -- eqTcType, which doesn't look through newtypes - -- [And it doesn't risk falling into a black hole either.] -eqExpr e1 e2 - = eq emptyVarEnv e1 e2 +tcEqExpr :: CoreExpr -> CoreExpr -> Bool +-- Used in rule matching, so does *not* look through +-- newtypes, predicate types; hence tcEqExpr + +tcEqExpr e1 e2 = tcEqExprX rn_env e1 e2 where - -- The "env" maps variables in e1 to variables in ty2 - -- So when comparing lambdas etc, - -- we in effect substitute v2 for v1 in e1 before continuing - eq env (Var v1) (Var v2) = case lookupVarEnv env v1 of - Just v1' -> v1' == v2 - Nothing -> v1 == v2 - - eq env (Lit lit1) (Lit lit2) = lit1 == lit2 - eq env (App f1 a1) (App f2 a2) = eq env f1 f2 && eq env a1 a2 - eq env (Lam v1 e1) (Lam v2 e2) = eq (extendVarEnv env v1 v2) e1 e2 - eq env (Let (NonRec v1 r1) e1) - (Let (NonRec v2 r2) e2) = eq env r1 r2 && eq (extendVarEnv env v1 v2) e1 e2 - eq env (Let (Rec ps1) e1) - (Let (Rec ps2) e2) = equalLength ps1 ps2 && - and (zipWith eq_rhs ps1 ps2) && - eq env' e1 e2 + rn_env = mkRnEnv2 (mkInScopeSet (exprFreeVars e1 `unionVarSet` exprFreeVars e2)) + +tcEqExprX :: RnEnv2 -> CoreExpr -> CoreExpr -> Bool +tcEqExprX env (Var v1) (Var v2) = rnOccL env v1 == rnOccR env v2 +tcEqExprX env (Lit lit1) (Lit lit2) = lit1 == lit2 +tcEqExprX env (App f1 a1) (App f2 a2) = tcEqExprX env f1 f2 && tcEqExprX env a1 a2 +tcEqExprX env (Lam v1 e1) (Lam v2 e2) = tcEqExprX (rnBndr2 env v1 v2) e1 e2 +tcEqExprX env (Let (NonRec v1 r1) e1) + (Let (NonRec v2 r2) e2) = tcEqExprX env r1 r2 + && tcEqExprX (rnBndr2 env v1 v2) e1 e2 +tcEqExprX env (Let (Rec ps1) e1) + (Let (Rec ps2) e2) = equalLength ps1 ps2 + && and (zipWith eq_rhs ps1 ps2) + && tcEqExprX env' e1 e2 where - env' = extendVarEnvList env [(v1,v2) | ((v1,_),(v2,_)) <- zip ps1 ps2] - eq_rhs (_,r1) (_,r2) = eq env' r1 r2 - eq env (Case e1 v1 t1 a1) - (Case e2 v2 t2 a2) = eq env e1 e2 && - t1 `eqType` t2 && - equalLength a1 a2 && - and (zipWith (eq_alt env') a1 a2) + env' = foldl2 rn_bndr2 env ps2 ps2 + rn_bndr2 env (b1,_) (b2,_) = rnBndr2 env b1 b2 + eq_rhs (_,r1) (_,r2) = tcEqExprX env' r1 r2 +tcEqExprX env (Case e1 v1 t1 a1) + (Case e2 v2 t2 a2) = tcEqExprX env e1 e2 + && tcEqTypeX env t1 t2 + && equalLength a1 a2 + && and (zipWith (eq_alt env') a1 a2) where - env' = extendVarEnv env v1 v2 + env' = rnBndr2 env v1 v2 - eq env (Note n1 e1) (Note n2 e2) = eq_note env n1 n2 && eq env e1 e2 - eq env (Type t1) (Type t2) = t1 `eqType` t2 - eq env e1 e2 = False +tcEqExprX env (Note n1 e1) (Note n2 e2) = eq_note env n1 n2 && tcEqExprX env e1 e2 +tcEqExprX env (Type t1) (Type t2) = tcEqTypeX env t1 t2 +tcEqExprX env e1 e2 = False - eq_list env [] [] = True - eq_list env (e1:es1) (e2:es2) = eq env e1 e2 && eq_list env es1 es2 - eq_list env es1 es2 = False - - eq_alt env (c1,vs1,r1) (c2,vs2,r2) = c1==c2 && - eq (extendVarEnvList env (vs1 `zip` vs2)) r1 r2 - - eq_note env (SCC cc1) (SCC cc2) = cc1 == cc2 - eq_note env (Coerce t1 f1) (Coerce t2 f2) = t1 `eqType` t2 && f1 `eqType` f2 - eq_note env InlineCall InlineCall = True - eq_note env (CoreNote s1) (CoreNote s2) = s1 == s2 - eq_note env other1 other2 = False +eq_alt env (c1,vs1,r1) (c2,vs2,r2) = c1==c2 && tcEqExprX (rnBndrs2 env vs1 vs2) r1 r2 + +eq_note env (SCC cc1) (SCC cc2) = cc1 == cc2 +eq_note env (Coerce t1 f1) (Coerce t2 f2) = tcEqTypeX env t1 t2 && tcEqTypeX env f1 f2 +eq_note env InlineCall InlineCall = True +eq_note env (CoreNote s1) (CoreNote s2) = s1 == s2 +eq_note env other1 other2 = False \end{code} diff --git a/ghc/compiler/coreSyn/Subst.lhs b/ghc/compiler/coreSyn/Subst.lhs index 36b5de8..8a7d9dd 100644 --- a/ghc/compiler/coreSyn/Subst.lhs +++ b/ghc/compiler/coreSyn/Subst.lhs @@ -6,8 +6,9 @@ \begin{code} module Subst ( -- Substitution stuff - Subst, SubstResult(..), - emptySubst, mkSubst, substInScope, substTy, + IdSubstEnv, SubstResult(..), + + Subst, emptySubst, mkSubst, substInScope, substTy, lookupIdSubst, lookupTvSubst, isEmptySubst, extendIdSubst, extendIdSubstList, extendTvSubst, extendTvSubstList, zapSubstEnv, setSubstEnv, diff --git a/ghc/compiler/deSugar/DsForeign.lhs b/ghc/compiler/deSugar/DsForeign.lhs index 4b2c1de..8af821c 100644 --- a/ghc/compiler/deSugar/DsForeign.lhs +++ b/ghc/compiler/deSugar/DsForeign.lhs @@ -26,7 +26,7 @@ import Literal ( Literal(..) ) import Module ( moduleString ) import Name ( getOccString, NamedThing(..) ) import OccName ( encodeFS ) -import Type ( repType, eqType, typePrimRep ) +import Type ( repType, coreEqType, typePrimRep ) import TcType ( Type, mkFunTys, mkForAllTys, mkTyConApp, mkFunTy, tcSplitTyConApp_maybe, tcSplitForAllTys, tcSplitFunTys, tcTyConAppArgs, @@ -156,7 +156,7 @@ dsCImport :: Id -> DsM ([Binding], SDoc, SDoc) dsCImport id (CLabel cid) _ _ no_hdrs = resultWrapper (idType id) `thenDs` \ (resTy, foRhs) -> - ASSERT(fromJust resTy `eqType` addrPrimTy) -- typechecker ensures this + ASSERT(fromJust resTy `coreEqType` addrPrimTy) -- typechecker ensures this let rhs = foRhs (mkLit (MachLabel cid Nothing)) in returnDs ([(setImpInline no_hdrs id, rhs)], empty, empty) dsCImport id (CFunction target) cconv safety no_hdrs @@ -465,7 +465,7 @@ mkFExportCBits c_nm maybe_target arg_htys res_hty is_IO_res_ty cc = map snd extra_cnames_and_tys ++ arg_htys -- stuff to do with the return type of the C function - res_hty_is_unit = res_hty `eqType` unitTy -- Look through any newtypes + res_hty_is_unit = res_hty `coreEqType` unitTy -- Look through any newtypes cResType | res_hty_is_unit = text "void" | otherwise = showStgType res_hty diff --git a/ghc/compiler/prelude/PrelRules.lhs b/ghc/compiler/prelude/PrelRules.lhs index 5cbcdb3..4fdec53 100644 --- a/ghc/compiler/prelude/PrelRules.lhs +++ b/ghc/compiler/prelude/PrelRules.lhs @@ -36,7 +36,7 @@ import TysWiredIn ( boolTy, trueDataConId, falseDataConId ) import TyCon ( tyConDataCons_maybe, isEnumerationTyCon, isNewTyCon ) import DataCon ( dataConTag, dataConTyCon, dataConWorkId, fIRST_TAG ) import CoreUtils ( cheapEqExpr, exprIsConApp_maybe ) -import Type ( tyConAppTyCon, eqType ) +import Type ( tyConAppTyCon, coreEqType ) import OccName ( occNameUserString) import PrelNames ( unpackCStringFoldrName, unpackCStringFoldrIdKey, hasKey, eqStringName, unpackCStringIdKey ) @@ -420,7 +420,7 @@ match_append_lit [Type ty1, ] | unpk `hasKey` unpackCStringFoldrIdKey && c1 `cheapEqExpr` c2 - = ASSERT( ty1 `eqType` ty2 ) + = ASSERT( ty1 `coreEqType` ty2 ) Just (Var unpk `App` Type ty1 `App` Lit (MachStr (s1 `appendFS` s2)) `App` c1 diff --git a/ghc/compiler/simplCore/Simplify.lhs b/ghc/compiler/simplCore/Simplify.lhs index 3ccdedf..15bd612 100644 --- a/ghc/compiler/simplCore/Simplify.lhs +++ b/ghc/compiler/simplCore/Simplify.lhs @@ -49,7 +49,7 @@ import Rules ( lookupRule ) import BasicTypes ( isMarkedStrict ) import CostCentre ( currentCCS ) import Type ( TvSubstEnv, isUnLiftedType, seqType, tyConAppArgs, funArgTy, - splitFunTy_maybe, splitFunTy, eqType, substTy, + splitFunTy_maybe, splitFunTy, coreEqType, substTy, mkTyVarTys, mkTyConApp ) import VarEnv ( elemVarEnv ) @@ -846,7 +846,7 @@ simplNote env (Coerce to from) body cont -- we may find (coerce T (coerce S (\x.e))) y -- and we'd like it to simplify to e[y/x] in one round -- of simplification - | t1 `eqType` k1 = cont -- The coerces cancel out + | t1 `coreEqType` k1 = cont -- The coerces cancel out | otherwise = CoerceIt t1 cont -- They don't cancel, but -- the inner one is redundant diff --git a/ghc/compiler/specialise/Rules.lhs b/ghc/compiler/specialise/Rules.lhs index f627d46..f344d9a 100644 --- a/ghc/compiler/specialise/Rules.lhs +++ b/ghc/compiler/specialise/Rules.lhs @@ -16,26 +16,22 @@ module Rules ( import CoreSyn -- All of it import OccurAnal ( occurAnalyseRule ) -import CoreFVs ( exprFreeVars, ruleRhsFreeVars ) +import CoreFVs ( exprFreeVars, exprsFreeVars, ruleRhsFreeVars ) import CoreUnfold ( isCheapUnfolding, unfoldingTemplate ) -import CoreUtils ( eqExpr ) +import CoreUtils ( tcEqExprX ) import CoreTidy ( pprTidyIdRules ) -import Subst ( Subst, SubstResult(..), extendIdSubst, - getTvSubstEnv, setTvSubstEnv, - emptySubst, isInScope, lookupIdSubst, lookupTvSubst, - bindSubstList, unBindSubstList, substInScope - ) +import Subst ( IdSubstEnv, SubstResult(..) ) import Id ( Id, idUnfolding, idSpecialisation, setIdSpecialisation ) -import Var ( Var, isId ) +import Var ( Var ) import VarSet import VarEnv -import TcType ( mkTyVarTy ) -import qualified Unify ( matchTyX ) +import TcType ( TvSubstEnv ) +import Unify ( matchTyX, MatchEnv(..) ) import BasicTypes ( Activation, CompilerPhase, isActive ) import Outputable import FastString -import Maybe ( isJust, isNothing, fromMaybe ) +import Maybe ( isJust, fromMaybe ) import Util ( sortLe ) import Bag import List ( isPrefixOf ) @@ -120,27 +116,6 @@ matchRule :: (Activation -> Bool) -> InScopeSet -- -- Any 'surplus' arguments in the input are simply put on the end -- of the output. --- --- ASSUMPTION (A): --- A1. No top-level variable is bound in the target --- A2. No template variable is bound in the target --- A3. No lambda bound template variable is free in any subexpression of the target --- --- To see why A1 is necessary, consider matching --- \x->f against \f->f --- When we meet the lambdas we substitute [f/x] in the template (a no-op), --- and then erroneously succeed in matching f against f. --- --- To see why A2 is needed consider matching --- forall a. \b->b against \a->3 --- When we meet the lambdas we substitute [a/b] in the template, and then --- erroneously succeed in matching what looks like the template variable 'a' against 3. --- --- A3 is needed to validate the rule that says --- (\x->E) matches F --- if --- (\x->E) matches (\x->F x) - matchRule is_active in_scope rule@(BuiltinRule name match_fn) args = case match_fn args of @@ -151,251 +126,193 @@ matchRule is_active in_scope rule@(Rule rn act tpl_vars tpl_args rhs) args | not (is_active act) = Nothing | otherwise - = go tpl_args args emptySubst - -- We used to use the in_scope set, but I don't think that's necessary - -- After all, the result is going to be simplified again with that in_scope set - where - tpl_var_set = mkVarSet tpl_vars - - ----------------------- - -- Do the business - go (tpl_arg:tpl_args) (arg:args) subst = match tpl_arg arg tpl_var_set (go tpl_args args) subst - - -- Two easy ways to terminate - go [] [] subst = Just (rn, app_match subst (mkLams tpl_vars rhs) tpl_vars) - go [] args subst = Just (rn, app_match subst (mkLams tpl_vars rhs) tpl_vars `mkApps` args) - - -- One tiresome way to terminate: check for excess unmatched - -- template arguments - go tpl_args [] subst = Nothing -- Failure - - - ----------------------- - app_match subst fn vs = foldl go fn vs - where - go fn v = case lookupVar subst v of - Just e -> fn `App` e - Nothing -> pprPanic "app_match: unbound tpl" (ppr v) - -lookupVar :: Subst -> Var -> Maybe CoreExpr -lookupVar subst v - | isId v = case lookupIdSubst subst v of - Just (DoneEx ex) -> Just ex - other -> Nothing - | otherwise = case lookupTvSubst subst v of - Just ty -> Just (Type ty) - Nothing -> Nothing - - ----------------------- -{- The code below tries to match even if there are more - template args than real args. - - I now think this is probably a bad idea. - Should the template (map f xs) match (map g)? I think not. - For a start, in general eta expansion wastes work. - SLPJ July 99 - - = case eta_complete tpl_args (mkVarSet leftovers) of - Just leftovers' -> Just (rn, mkLams done (mkLams leftovers' rhs), - mk_result_args subst done) - Nothing -> Nothing -- Failure - where - (done, leftovers) = partition (\v -> isJust (lookupSubstEnv subst_env v)) - (map zapOccInfo tpl_vars) - -- Zap the occ info - subst_env = substEnv subst - - ----------------------- - eta_complete [] vars = ASSERT( isEmptyVarSet vars ) - Just [] - eta_complete (Type ty:tpl_args) vars - = case getTyVar_maybe ty of - Just tv | tv `elemVarSet` vars - -> case eta_complete tpl_args (vars `delVarSet` tv) of - Just vars' -> Just (tv:vars') - Nothing -> Nothing - other -> Nothing - - eta_complete (Var v:tpl_args) vars - | v `elemVarSet` vars - = case eta_complete tpl_args (vars `delVarSet` v) of - Just vars' -> Just (v:vars') - Nothing -> Nothing - - eta_complete other vars = Nothing - - -zapOccInfo bndr | isTyVar bndr = bndr - | otherwise = zapLamIdInfo bndr --} + = case matchN in_scope tpl_vars tpl_args args of + Just (tpl_vals, leftovers) -> Just (rn, mkLams tpl_vars rhs `mkApps` tpl_vals `mkApps` leftovers) + Nothing -> Nothing \end{code} \begin{code} -type Matcher result = VarSet -- Template variables - -> (Subst -> Maybe result) -- Continuation if success - -> Subst -> Maybe result -- Substitution so far -> result --- The *SubstEnv* in these Substs apply to the TEMPLATE only - --- The *InScopeSet* in these Substs is HIJACKED, --- to give the set of variables bound so far in the --- target term. So when matching forall a. (\x. a x) against (\y. y y) --- while processing the body of the lambdas, the in-scope set will be {y}. --- That lets us do the occurs-check when matching 'a' against 'y' --- --- It starts off empty - -match :: CoreExpr -- Template +matchN :: InScopeSet + -> [Var] -- Template tyvars + -> [CoreExpr] -- Template + -> [CoreExpr] -- Target; can have more elts than template + -> Maybe ([CoreExpr], -- What is substituted for each template var + [CoreExpr]) -- Leftover target exprs + +matchN in_scope tmpl_vars tmpl_es target_es + = do { (subst, leftover_es) <- go init_menv emptySubstEnv tmpl_es target_es + ; return (map (lookup_tmpl subst) tmpl_vars, leftover_es) } + where + init_menv = ME { me_tmpls = mkVarSet tmpl_vars, me_env = init_rn_env } + init_rn_env = mkRnEnv2 (extendInScopeSetList in_scope tmpl_vars) + + go menv subst [] es = Just (subst, es) + go menv subst ts [] = Nothing -- Fail if too few actual args + go menv subst (t:ts) (e:es) = do { subst1 <- match menv subst t e + ; go menv subst1 ts es } + + lookup_tmpl :: (TvSubstEnv, IdSubstEnv) -> Var -> CoreExpr + lookup_tmpl (tv_subst, id_subst) tmpl_var + | isTyVar tmpl_var = case lookupVarEnv tv_subst tmpl_var of + Just ty -> Type ty + Nothing -> unbound tmpl_var + | otherwise = case lookupVarEnv id_subst tmpl_var of + Just (DoneEx e) -> e + other -> unbound tmpl_var + + unbound var = pprPanic "Template variable unbound in rewrite rule" (ppr var) + +emptySubstEnv :: (TvSubstEnv, IdSubstEnv) +emptySubstEnv = (emptyVarEnv, emptyVarEnv) + + +-- At one stage I tried to match even if there are more +-- template args than real args. + +-- I now think this is probably a bad idea. +-- Should the template (map f xs) match (map g)? I think not. +-- For a start, in general eta expansion wastes work. +-- SLPJ July 99 + + +match :: MatchEnv + -> (TvSubstEnv, IdSubstEnv) + -> CoreExpr -- Template -> CoreExpr -- Target - -> Matcher result - -match_fail = Nothing - --- ToDo: remove this debugging junk --- match e1 e2 tpls kont subst = pprTrace "match" (ppr e1 <+> ppr e2 <+> ppr subst) $ match_ e1 e2 tpls kont subst -match = match_ - -match_ (Var v1) e2 tpl_vars kont subst - = case lookupIdSubst subst v1 of - Nothing | v1 `elemVarSet` tpl_vars -- v1 is a template variable - -> if (any (`isInScope` subst) (varSetElems (exprFreeVars e2))) then - match_fail -- Occurs check failure - -- e.g. match forall a. (\x-> a x) against (\y. y y) - else - kont (extendIdSubst subst v1 (DoneEx e2)) + -> Maybe (TvSubstEnv, IdSubstEnv) +-- See the notes with Unify.match, which matches types +-- Everything is very similar for terms - | eqExpr (Var v1) e2 -> kont subst - -- v1 is not a template variable, so it must be a global constant - - Just (DoneEx e2') | eqExpr e2' e2 -> kont subst +-- Interesting examples: +-- Consider matching +-- \x->f against \f->f +-- When we meet the lambdas we must remember to rename f to f' in the +-- second expresion. The RnEnv2 does that. +-- +-- Consider matching +-- forall a. \b->b against \a->3 +-- We must rename the \a. Otherwise when we meet the lambdas we +-- might substitute [a/b] in the template, and then erroneously +-- succeed in matching what looks like the template variable 'a' against 3. + +-- The Var case follows closely what happens in Unify.match +match menv subst@(tv_subst, id_subst) (Var v1) e2 + | v1 `elemVarSet` me_tmpls menv + = case lookupVarEnv id_subst v1' of + Nothing | any (inRnEnvR rn_env) (varSetElems (exprFreeVars e2)) + -> Nothing -- Occurs check failure + -- e.g. match forall a. (\x-> a x) against (\y. y y) + + | otherwise + -> Just (tv_subst, extendVarEnv id_subst v1 (DoneEx e2)) + + Just (DoneEx e2') | tcEqExprX (nukeRnEnvL rn_env) e2' e2 + -> Just subst + + other -> Nothing + + | otherwise -- v1 is not a template variable + = case e2 of + Var v2 | v1' == rnOccR rn_env v2 -> Just subst + other -> Nothing + where + rn_env = me_env menv + v1' = rnOccL rn_env v1 - other -> match_fail +-- Here is another important rule: if the term being matched is a +-- variable, we expand it so long as its unfolding is a WHNF +-- (Its occurrence information is not necessarily up to date, +-- so we don't use it.) +match menv subst e1 (Var v2) + | isCheapUnfolding unfolding + = match menv subst e1 (unfoldingTemplate unfolding) + where + unfolding = idUnfolding v2 -match_ (Lit lit1) (Lit lit2) tpl_vars kont subst +match menv subst (Lit lit1) (Lit lit2) | lit1 == lit2 - = kont subst + = Just subst -match_ (App f1 a1) (App f2 a2) tpl_vars kont subst - = match f1 f2 tpl_vars (match a1 a2 tpl_vars kont) subst +match menv subst (App f1 a1) (App f2 a2) + = do { subst' <- match menv subst f1 f2 + ; match menv subst' a1 a2 } -match_ (Lam x1 e1) (Lam x2 e2) tpl_vars kont subst - = bind [x1] [x2] (match e1 e2) tpl_vars kont subst +match menv subst (Lam x1 e1) (Lam x2 e2) + = match menv' subst e1 e2 + where + menv' = menv { me_env = rnBndr2 (me_env menv) x1 x2 } -- This rule does eta expansion -- (\x.M) ~ N iff M ~ N x --- See assumption A3 -match_ (Lam x1 e1) e2 tpl_vars kont subst - = bind [x1] [x1] (match e1 (App e2 (mkVarArg x1))) tpl_vars kont subst - --- Eta expansion the other way --- M ~ (\y.N) iff \y.M y ~ \y.N --- iff M y ~ N --- Remembering that by (A), y can't be free in M, we get this -match_ e1 (Lam x2 e2) tpl_vars kont subst - | new_id == x2 -- If the two are equal, don't bind, else we get - -- a substitution looking like x->x, and that sends - -- Unify.matchTy into a loop - = match (App e1 (mkVarArg new_id)) e2 tpl_vars kont subst - | otherwise - = bind [new_id] [x2] (match (App e1 (mkVarArg new_id)) e2) tpl_vars kont subst +match menv subst (Lam x1 e1) e2 + = match menv' subst e1 (App e2 (varToCoreExpr new_x)) where - new_id = uniqAway (substInScope subst) x2 - -- This uniqAway is actually needed. Here's the example: - -- rule: foldr (mapFB (:) f) [] = mapList - -- target: foldr (\x. mapFB k f x) [] - -- where - -- k = \x. mapFB ... x - -- The first \x is ok, but when we inline k, hoping it might - -- match (:) we find a second \x. + (rn_env', new_x) = rnBndrL (me_env menv) x1 + menv' = menv { me_env = rn_env' } --- gaw 2004 -match_ (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2) tpl_vars kont subst - = (match_ty ty1 ty2 tpl_vars $ - match e1 e2 tpl_vars case_kont) subst +-- Eta expansion the other way +-- M ~ (\y.N) iff M y ~ N +match menv subst e1 (Lam x2 e2) + = match menv' subst (App e1 (varToCoreExpr new_x)) e2 where - case_kont subst = bind [x1] [x2] (match_alts alts1 (sortLe le_alt alts2)) - tpl_vars kont subst - -match_ (Type ty1) (Type ty2) tpl_vars kont subst - = match_ty ty1 ty2 tpl_vars kont subst + (rn_env', new_x) = rnBndrR (me_env menv) x2 + menv' = menv { me_env = rn_env' } -match_ (Note (Coerce to1 from1) e1) (Note (Coerce to2 from2) e2) - tpl_vars kont subst - = (match_ty to1 to2 tpl_vars $ - match_ty from1 from2 tpl_vars $ - match e1 e2 tpl_vars kont) subst +match menv subst (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2) + = do { subst1 <- match_ty menv subst ty1 ty2 + ; subst2 <- match menv subst1 e1 e2 + ; let menv' = menv { me_env = rnBndr2 (me_env menv) x2 x2 } + ; match_alts menv' subst2 (sortLe le_alt alts1) (sortLe le_alt alts2) + } +match menv subst (Type ty1) (Type ty2) + = match_ty menv subst ty1 ty2 -{- I don't buy this let-rule any more - The let rule fails on matching - forall f,x,xs. f (x:xs) - against - f (let y = e in (y:[])) - because we just get x->y, which is bogus. +match menv subst (Note (Coerce to1 from1) e1) (Note (Coerce to2 from2) e2) + = do { subst1 <- match_ty menv subst to1 to2 + ; subst2 <- match_ty menv subst1 from1 from2 + ; match menv subst2 e1 e2 } -- This is an interesting rule: we simply ignore lets in the -- term being matched against! The unfolding inside it is (by assumption) -- already inside any occurrences of the bound variables, so we'll expand --- them when we encounter them. Meanwhile, we can't get false matches because --- (also by assumption) the term being matched has no shadowing. -match e1 (Let bind e2) tpl_vars kont subst - = match e1 e2 tpl_vars kont subst --} - --- Here is another important rule: if the term being matched is a --- variable, we expand it so long as its unfolding is a WHNF --- (Its occurrence information is not necessarily up to date, --- so we don't use it.) -match_ e1 (Var v2) tpl_vars kont subst - | isCheapUnfolding unfolding - = match e1 (unfoldingTemplate unfolding) tpl_vars kont subst +-- them when we encounter them. +match menv subst e1 (Let (NonRec x2 r2) e2) + = match menv' subst e1 e2 where - unfolding = idUnfolding v2 - - --- We can't cope with lets in the template - -match_ e1 e2 tpl_vars kont subst = match_fail - + menv' = menv { me_env = fst (rnBndrR (me_env menv) x2) } + -- It's important to do this renaming. For example: + -- Matching + -- forall f,x,xs. f (x:xs) + -- against + -- f (let y = e in (y:[])) + -- We must not get success with x->y! Instead, we + -- need an occurs check. + +-- Everything else fails +match menv subst e1 e2 = Nothing ------------------------------------------ -match_alts [] [] tpl_vars kont subst - = kont subst -match_alts ((c1,vs1,r1):alts1) ((c2,vs2,r2):alts2) tpl_vars kont subst +match_alts :: MatchEnv + -> (TvSubstEnv, IdSubstEnv) + -> [CoreAlt] -- Template + -> [CoreAlt] -- Target + -> Maybe (TvSubstEnv, IdSubstEnv) +match_alts menv subst [] [] + = return subst +match_alts menv subst ((c1,vs1,r1):alts1) ((c2,vs2,r2):alts2) | c1 == c2 - = bind vs1 vs2 (match r1 r2) tpl_vars - (match_alts alts1 alts2 tpl_vars kont) - subst -match_alts alts1 alts2 tpl_vars kont subst = match_fail - -le_alt (con1, _, _) (con2, _, _) = con1 <= con2 - ----------------------------------------- -bind :: [CoreBndr] -- Template binders - -> [CoreBndr] -- Target binders - -> Matcher result - -> Matcher result --- This makes uses of assumption (A) above. For example, --- this would fail: --- Template: (\x.y) (y is free) --- Target : (\y.y) (y is bound) --- We rename x to y in the template... but then erroneously --- match y against y. But this can't happen because of (A) -bind vs1 vs2 matcher tpl_vars kont subst - = WARN( not (all not_in_subst vs1), bug_msg ) - matcher tpl_vars kont' subst' + = do { subst1 <- match menv' subst r1 r2 + ; match_alts menv subst1 alts1 alts2 } where - kont' subst'' = kont (unBindSubstList subst'' vs1 vs2) - subst' = bindSubstList subst vs1 vs2 + menv' :: MatchEnv + menv' = menv { me_env = rnBndrs2 (me_env menv) vs1 vs2 } - -- The unBindSubst relies on no shadowing in the template - not_in_subst v = isNothing (lookupVar subst v) - bug_msg = sep [ppr vs1, ppr vs2] +match_alts menv subst alts1 alts2 + = Nothing ----------------------------------------- -mkVarArg :: CoreBndr -> CoreArg -mkVarArg v | isId v = Var v - | otherwise = Type (mkTyVarTy v) +le_alt (con1, _, _) (con2, _, _) = con1 <= con2 \end{code} Matching Core types: use the matcher in TcType. @@ -405,15 +322,13 @@ we have a specialised version of a function at a newtype, say We only want to replace (f T) with f', not (f Int). \begin{code} ----------------------------------------- -match_ty ty1 ty2 tpl_vars kont subst - = case Unify.matchTyX tpl_vars (getTvSubstEnv subst) ty1 ty2 of - Just tv_env' -> kont (setTvSubstEnv subst tv_env') - Nothing -> match_fail +------------------------------------------ +match_ty menv (tv_subst, id_subst) ty1 ty2 + = do { tv_subst' <- Unify.matchTyX menv tv_subst ty1 ty2 + ; return (tv_subst', id_subst) } \end{code} - %************************************************************************ %* * \subsection{Adding a new rule} @@ -583,7 +498,7 @@ ruleAppCheck_help phase fn args rules | not (isActive phase act) = text "active only in later phase" | n_args < n_rule_args = text "too few arguments" | n_mismatches == n_rule_args = text "no arguments match" - | n_mismatches == 0 = text "all arguments match (considered individually), but the rule as a whole does not" + | n_mismatches == 0 = text "all arguments match (considered individually), but rule as a whole does not" | otherwise = text "arguments" <+> ppr mismatches <+> text "do not match (1-indexing)" where n_rule_args = length rule_args @@ -591,8 +506,12 @@ ruleAppCheck_help phase fn args rules mismatches = [i | (rule_arg, (arg,i)) <- rule_args `zip` i_args, not (isJust (match_fn rule_arg arg))] - bndr_set = mkVarSet rule_bndrs - match_fn rule_arg arg = match rule_arg arg bndr_set (\s -> Just ()) emptySubst + lhs_fvs = exprsFreeVars rule_args -- Includes template tyvars + match_fn rule_arg arg = match menv emptySubstEnv rule_arg arg + where + in_scope = lhs_fvs `unionVarSet` exprFreeVars arg + menv = ME { me_env = mkRnEnv2 (mkInScopeSet in_scope) + , me_tmpls = mkVarSet rule_bndrs } \end{code} diff --git a/ghc/compiler/specialise/SpecConstr.lhs b/ghc/compiler/specialise/SpecConstr.lhs index c7824ca..e07470b 100644 --- a/ghc/compiler/specialise/SpecConstr.lhs +++ b/ghc/compiler/specialise/SpecConstr.lhs @@ -12,7 +12,7 @@ module SpecConstr( import CoreSyn import CoreLint ( showPass, endPass ) -import CoreUtils ( exprType, eqExpr, mkPiTypes ) +import CoreUtils ( exprType, tcEqExpr, mkPiTypes ) import CoreFVs ( exprsFreeVars ) import CoreTidy ( pprTidyIdRules ) import WwLib ( mkWorkerArgs ) @@ -444,7 +444,7 @@ specialise env fn bndrs body (SCU {calls=calls, occs=occs}) (nubBy same_call good_calls `zip` [1..]) where n_bndrs = length bndrs - same_call as1 as2 = and (zipWith eqExpr as1 as2) + same_call as1 as2 = and (zipWith tcEqExpr as1 as2) --------------------- good_arg :: ConstrEnv -> IdEnv ArgOcc -> (CoreBndr, CoreArg) -> Bool diff --git a/ghc/compiler/stranal/DmdAnal.lhs b/ghc/compiler/stranal/DmdAnal.lhs index 12b25bc..903cff2 100644 --- a/ghc/compiler/stranal/DmdAnal.lhs +++ b/ghc/compiler/stranal/DmdAnal.lhs @@ -39,7 +39,7 @@ import TysWiredIn ( unboxedPairDataCon ) import TysPrim ( realWorldStatePrimTy ) import UniqFM ( plusUFM_C, addToUFM_Directly, lookupUFM_Directly, keysUFM, minusUFM, ufmToList, filterUFM ) -import Type ( isUnLiftedType, eqType ) +import Type ( isUnLiftedType, coreEqType ) import CoreLint ( showPass, endPass ) import Util ( mapAndUnzip, mapAccumL, mapAccumR, lengthIs ) import BasicTypes ( Arity, TopLevelFlag(..), isTopLevel, isNeverActive, @@ -329,7 +329,7 @@ dmdAnalAlt sigs dmd (con,bndrs,rhs) -- ; print len } io_hack_reqd = con == DataAlt unboxedPairDataCon && - idType (head bndrs) `eqType` realWorldStatePrimTy + idType (head bndrs) `coreEqType` realWorldStatePrimTy in (final_alt_ty, (con, bndrs', rhs')) \end{code} diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index 9db0b3a..ad5060b 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -50,6 +50,7 @@ import VarSet import SrcLoc ( Located(..), unLoc, noLoc, getLoc ) import Bag import Util ( isIn ) +import Maybes ( orElse ) import BasicTypes ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec, isNotTopLevel, isAlwaysActive ) import FiniteMap ( listToFM, lookupFM ) @@ -567,7 +568,7 @@ tcTySig sig1 (L span (Sig (L _ name) ty)) -- Try to match the context of this signature with -- that of the first signature - ; case tcMatchPreds tvs (sig_theta sig1) theta of { + ; case tcMatchPreds tvs theta (sig_theta sig1) of { Nothing -> bale_out ; Just tenv -> do ; case check_tvs tenv tvs of @@ -593,15 +594,12 @@ tcTySig sig1 (L span (Sig (L _ name) ty)) check_tvs :: TvSubstEnv -> [TcTyVar] -> Maybe [TcTyVar] check_tvs tenv [] = Just [] check_tvs tenv (tv:tvs) - | Just ty <- lookupVarEnv tenv tv - = do { tv' <- tcGetTyVar_maybe ty + = do { let ty = lookupVarEnv tenv tv `orElse` mkTyVarTy tv + ; tv' <- tcGetTyVar_maybe ty ; tvs' <- check_tvs tenv tvs ; if tv' `elem` tvs' then Nothing else Just (tv':tvs') } - | otherwise - = do { tvs' <- check_tvs tenv tvs - ; Just (tv:tvs') } \end{code} \begin{code} diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index beecfb4..98f89d3 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -2302,7 +2302,7 @@ addNoInstanceErrs mb_what givens dicts = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") <+> pprPred (dictPred dict))), sep [ptext SLIT("Matching instances") <> colon, - nest 2 (pprDFuns (dfuns ++ unifiers))], + nest 2 (vcat [pprDFuns dfuns, text "---", pprDFuns unifiers])], ASSERT( not (null matches) ) if not (isSingleton matches) then -- Two or more matches diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 5dcac23..187ac27 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -43,7 +43,7 @@ module TcType ( --------------------------------- -- Predicates. -- Again, newtypes are opaque - tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, + tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX, isSigmaTy, isOverloadedTy, isDoubleTy, isFloatTy, isIntTy, isIntegerTy, isAddrTy, isBoolTy, isUnitTy, @@ -140,6 +140,10 @@ import Type ( -- Re-exports tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, isSubKind, + + tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, + tcEqPred, tcCmpPred, tcEqTypeX, + TvSubst(..), TvSubstEnv, emptyTvSubst, mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst, @@ -157,7 +161,6 @@ import DataCon ( DataCon ) import Class ( Class ) import Var ( TyVar, Id, isTcTyVar, tcTyVarDetails ) import ForeignCall ( Safety, playSafe, DNType(..) ) -import VarEnv import VarSet -- others: @@ -169,7 +172,7 @@ import PrelNames -- Lots (e.g. in isFFIArgumentTy) import TysWiredIn ( unitTyCon, charTyCon, listTyCon ) import BasicTypes ( IPName(..), ipNameName ) import SrcLoc ( SrcLoc, SrcSpan ) -import Util ( cmpList, thenCmp, snocView ) +import Util ( snocView ) import Maybes ( maybeToBool, expectJust ) import Outputable import DATA_IOREF @@ -567,95 +570,6 @@ isLinearPred other = False %************************************************************************ %* * -\subsection{Comparison} -%* * -%************************************************************************ - -Comparison, taking note of newtypes, predicates, etc, - -\begin{code} -tcEqType :: Type -> Type -> Bool -tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False } - -tcEqTypes :: [Type] -> [Type] -> Bool -tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False } - -tcEqPred :: PredType -> PredType -> Bool -tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False } - -------------- -tcCmpType :: Type -> Type -> Ordering -tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2 - -tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2 - -tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2 -------------- -cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2 - -------------- -cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering - -- The "env" maps type variables in ty1 to type variables in ty2 - -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2) - -- we in effect substitute tv2 for tv1 in t1 before continuing - - -- Look through NoteTy -cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2 -cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2 - - -- Deal with equal constructors -cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of - Just tv1a -> tv1a `compare` tv2 - Nothing -> tv1 `compare` tv2 - -cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2 -cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2 -cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2 -cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2) -cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2 - - -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy -cmpTy env (AppTy _ _) (TyVarTy _) = GT - -cmpTy env (FunTy _ _) (TyVarTy _) = GT -cmpTy env (FunTy _ _) (AppTy _ _) = GT - -cmpTy env (TyConApp _ _) (TyVarTy _) = GT -cmpTy env (TyConApp _ _) (AppTy _ _) = GT -cmpTy env (TyConApp _ _) (FunTy _ _) = GT - -cmpTy env (ForAllTy _ _) (TyVarTy _) = GT -cmpTy env (ForAllTy _ _) (AppTy _ _) = GT -cmpTy env (ForAllTy _ _) (FunTy _ _) = GT -cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT - -cmpTy env (PredTy _) t2 = GT - -cmpTy env _ _ = LT -\end{code} - -\begin{code} -cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering -cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2) - -- Compare types as well as names for implicit parameters - -- This comparison is used exclusively (I think) for the - -- finite map built in TcSimplify -cmpPredTy env (IParam _ _) (ClassP _ _) = LT -cmpPredTy env (ClassP _ _) (IParam _ _) = GT -cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2) -\end{code} - -PredTypes are used as a FM key in TcSimplify, -so we take the easy path and make them an instance of Ord - -\begin{code} -instance Eq PredType where { (==) = tcEqPred } -instance Ord PredType where { compare = tcCmpPred } -\end{code} - - -%************************************************************************ -%* * \subsection{Predicates} %* * %************************************************************************ diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs index 9bad29d..d7fa64d 100644 --- a/ghc/compiler/types/Type.lhs +++ b/ghc/compiler/types/Type.lhs @@ -29,7 +29,7 @@ module Type ( mkSynTy, - repType, typePrimRep, coreView, + repType, typePrimRep, coreView, deepCoreView, mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, applyTy, applyTys, isForAllTy, dropForAlls, @@ -56,7 +56,8 @@ module Type ( tidyTopType, tidyPred, -- Comparison - eqType, + coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, + tcEqPred, tcCmpPred, tcEqTypeX, -- Seq seqType, seqTypes, @@ -103,7 +104,7 @@ import TyCon ( TyCon, isRecursiveTyCon, isPrimTyCon, import CmdLineOpts ( opt_DictsStrict ) import SrcLoc ( noSrcLoc ) import Unique ( Uniquable(..) ) -import Util ( mapAccumL, seqList, lengthIs, snocView ) +import Util ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual ) import Outputable import UniqSet ( sizeUniqSet ) -- Should come via VarSet import Maybe ( isJust ) @@ -132,6 +133,17 @@ coreView (PredTy p) = Just (predTypeRep p) coreView (TyConApp tc tys) = expandNewTcApp tc tys coreView ty = Nothing +deepCoreView :: Type -> Type +-- Apply coreView recursively +deepCoreView ty + | Just ty' <- coreView ty = deepCoreView ty' +deepCoreView (TyVarTy tv) = TyVarTy tv +deepCoreView (TyConApp tc tys) = TyConApp tc (map deepCoreView tys) +deepCoreView (AppTy t1 t2) = AppTy (deepCoreView t1) (deepCoreView t2) +deepCoreView (FunTy t1 t2) = FunTy (deepCoreView t1) (deepCoreView t2) +deepCoreView (ForAllTy tv ty) = ForAllTy tv (deepCoreView ty) + -- No NoteTy, no PredTy + expandNewTcApp :: TyCon -> [Type] -> Maybe Type -- A local helper function (not exported) -- Expands *the outermoset level of* a newtype application to @@ -835,33 +847,75 @@ seqPred (IParam n ty) = n `seq` seqType ty %************************************************************************ %* * -\subsection{Equality on types} + Comparison of types + (We don't use instances so that we know where it happens) %* * %************************************************************************ -Comparison; don't use instances so that we know where it happens. -Look through newtypes but not usage types. +Two flavours: + +* tcEqType, tcCmpType do *not* look through newtypes, PredTypes +* coreEqType *does* look through them Note that eqType can respond 'False' for partial applications of newtypes. Consider newtype Parser m a = MkParser (Foogle m a) - Does Monad (Parser m) `eqType` Monad (Foogle m) - Well, yes, but eqType won't see that they are the same. I don't think this is harmful, but it's soemthing to watch out for. +First, the external interface + +\begin{code} +coreEqType :: Type -> Type -> Bool +coreEqType t1 t2 = isEqual $ cmpType (deepCoreView t1) (deepCoreView t2) + +tcEqType :: Type -> Type -> Bool +tcEqType t1 t2 = isEqual $ cmpType t1 t2 + +tcEqTypes :: [Type] -> [Type] -> Bool +tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2 + +tcCmpType :: Type -> Type -> Ordering +tcCmpType t1 t2 = cmpType t1 t2 + +tcCmpTypes :: [Type] -> [Type] -> Ordering +tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2 + +tcEqPred :: PredType -> PredType -> Bool +tcEqPred p1 p2 = isEqual $ cmpPred p1 p2 + +tcCmpPred :: PredType -> PredType -> Ordering +tcCmpPred p1 p2 = cmpPred p1 p2 + +tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool +tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2 +\end{code} + +Now here comes the real worker + \begin{code} -eqType t1 t2 = eq_ty emptyVarEnv t1 t2 +cmpType :: Type -> Type -> Ordering +cmpType t1 t2 = cmpTypeX rn_env t1 t2 + where + rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2)) + +cmpTypes :: [Type] -> [Type] -> Ordering +cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2 + where + rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2)) + +cmpPred :: PredType -> PredType -> Ordering +cmpPred p1 p2 = cmpPredX rn_env p1 p2 + where + rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2)) --- Look through Notes, PredTy, newtype applications -eq_ty env t1 t2 | Just t1' <- coreView t1 = eq_ty env t1' t2 -eq_ty env t1 t2 | Just t2' <- coreView t2 = eq_ty env t1 t2' +cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse -- NB: we *cannot* short-cut the newtype comparison thus: --- eq_ty env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) --- | (tc1 == tc2) = (eq_tys env tys1 tys2) +-- eqTypeX env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) +-- | (tc1 == tc2) = (eqTypeXs env tys1 tys2) -- -- Consider: -- newtype T a = MkT [a] @@ -876,21 +930,58 @@ eq_ty env t1 t2 | Just t2' <- coreView t2 = eq_ty env t1 t2' -- but we can only expand saturated newtypes, so just comparing -- T with [] won't do. --- The rest is plain sailing -eq_ty env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of - Just tv1a -> tv1a == tv2 - Nothing -> tv1 == tv2 -eq_ty env (ForAllTy tv1 t1) (ForAllTy tv2 t2) - | tv1 == tv2 = eq_ty (delVarEnv env tv1) t1 t2 - | otherwise = eq_ty (extendVarEnv env tv1 tv2) t1 t2 -eq_ty env (AppTy s1 t1) (AppTy s2 t2) = (eq_ty env s1 s2) && (eq_ty env t1 t2) -eq_ty env (FunTy s1 t1) (FunTy s2 t2) = (eq_ty env s1 s2) && (eq_ty env t1 t2) -eq_ty env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 == tc2) && (eq_tys env tys1 tys2) -eq_ty env t1 t2 = False - -eq_tys env [] [] = True -eq_tys env (t1:tys1) (t2:tys2) = (eq_ty env t1 t2) && (eq_tys env tys1 tys2) -eq_tys env tys1 tys2 = False +cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2 +cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2 +cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2 +cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2 +cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2 +cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2 +cmpTypeX env (NoteTy _ t1) t2 = cmpTypeX env t1 t2 +cmpTypeX env t1 (NoteTy _ t2) = cmpTypeX env t1 t2 + + -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy +cmpTypeX env (AppTy _ _) (TyVarTy _) = GT + +cmpTypeX env (FunTy _ _) (TyVarTy _) = GT +cmpTypeX env (FunTy _ _) (AppTy _ _) = GT + +cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT +cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT +cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT + +cmpTypeX env (ForAllTy _ _) (TyVarTy _) = GT +cmpTypeX env (ForAllTy _ _) (AppTy _ _) = GT +cmpTypeX env (ForAllTy _ _) (FunTy _ _) = GT +cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT + +cmpTypeX env (PredTy _) t2 = GT + +cmpTypeX env _ _ = LT + +------------- +cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering +cmpTypesX env [] [] = EQ +cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `compare` cmpTypesX env tys1 tys2 +cmpTypesX env [] tys = LT +cmpTypesX env ty [] = GT + +------------- +cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering +cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2 + -- Compare types as well as names for implicit parameters + -- This comparison is used exclusively (I think) for the + -- finite map built in TcSimplify +cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2 +cmpPredX env (IParam _ _) (ClassP _ _) = LT +cmpPredX env (ClassP _ _) (IParam _ _) = GT +\end{code} + +PredTypes are used as a FM key in TcSimplify, +so we take the easy path and make them an instance of Ord + +\begin{code} +instance Eq PredType where { (==) = tcEqPred } +instance Ord PredType where { compare = tcCmpPred } \end{code} diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs index 8d5f070..f1bc487 100644 --- a/ghc/compiler/types/Unify.lhs +++ b/ghc/compiler/types/Unify.lhs @@ -1,10 +1,11 @@ \begin{code} module Unify ( -- Matching and unification - matchTys, matchTyX, matchTysX, + matchTys, matchTyX, tcMatchPreds, MatchEnv(..), + unifyTys, unifyTysX, - tcRefineTys, tcMatchTys, tcMatchPreds, coreRefineTys, + tcRefineTys, tcMatchTys, coreRefineTys, -- Re-export MaybeErr(..) @@ -16,9 +17,8 @@ import Var ( Var, TyVar, tyVarKind ) import VarEnv import VarSet import Kind ( isSubKind ) -import Type ( predTypeRep, typeKind, - tyVarsOfType, tyVarsOfTypes, coreView, - TvSubstEnv, TvSubst(..), substTy ) +import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, + TvSubstEnv, TvSubst(..), substTy, tcEqTypeX ) import TypeRep ( Type(..), PredType(..), funTyCon ) import Util ( snocView ) import ErrUtils ( Message ) @@ -29,32 +29,171 @@ import Maybes %************************************************************************ %* * - External interface + Matching +%* * +%************************************************************************ + + +Matching is much tricker than you might think. + +1. The substitution we generate binds the *template type variables* + which are given to us explicitly. + +2. We want to match in the presence of foralls; + e.g (forall a. t1) ~ (forall b. t2) + + That is what the RnEnv2 is for; it does the alpha-renaming + that makes it as if a and b were the same variable. + Initialising the RnEnv2, so that it can generate a fresh + binder when necessary, entails knowing the free variables of + both types. + +3. We must be careful not to bind a template type variable to a + locally bound variable. E.g. + (forall a. x) ~ (forall b. b) + where x is the template type variable. Then we do not want to + bind x to a/b! This is a kind of occurs check. + The necessary locals accumulate in the RnEnv2. + + +\begin{code} +data MatchEnv + = ME { me_tmpls :: VarSet -- Template tyvars + , me_env :: RnEnv2 -- Renaming envt for nested foralls + } -- In-scope set includes template tyvars + +matchTys :: TyVarSet -- Template tyvars + -> [Type] -- Template + -> [Type] -- Target + -> Maybe TvSubstEnv -- One-shot; in principle the template + -- variables could be free in the target + +matchTys tmpls tys1 tys2 + = match_tys (ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope_tyvars}) + emptyTvSubstEnv + tys1 tys2 + where + in_scope_tyvars = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2) + -- We're assuming that all the interesting + -- tyvars in tys1 are in tmpls + +tcMatchPreds + :: [TyVar] -- Bind these + -> [PredType] -> [PredType] + -> Maybe TvSubstEnv +tcMatchPreds tmpls ps1 ps2 + = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2 + where + menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars } + in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2) + +matchTyX :: MatchEnv + -> TvSubstEnv -- Substitution to extend + -> Type -- Template + -> Type -- Target + -> Maybe TvSubstEnv + +matchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export +\end{code} + +Now the internals of matching + +\begin{code} +match :: MatchEnv -- For the ost part this is pushed downwards + -> TvSubstEnv -- Substitution so far: + -- Domain is subset of template tyvars + -- Free vars of range is subset of + -- in-scope set of the RnEnv2 + -> Type -> Type -- Template and target respectively + -> Maybe TvSubstEnv +-- This matcher works on source types; that is, +-- it respects NewTypes and PredType + +match menv subst (NoteTy _ ty1) ty2 = match menv subst ty1 ty2 +match menv subst ty1 (NoteTy _ ty2) = match menv subst ty1 ty2 + +match menv subst (TyVarTy tv1) ty2 + | tv1 `elemVarSet` me_tmpls menv + = case lookupVarEnv subst tv1' of + Nothing | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2)) + -> Nothing -- Occurs check + | otherwise + -> Just (extendVarEnv subst tv1 ty2) + + Just ty1' | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2 + -- ty1 has no locally-bound variables, hence nukeRnEnvL + -- Note tcEqType...we are doing source-type matching here + -> Just subst + + other -> Nothing + + | otherwise -- tv1 is not a template tyvar + = case ty2 of + TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst + other -> Nothing + where + rn_env = me_env menv + tv1' = rnOccL rn_env tv1 + +match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) + = match menv' subst ty1 ty2 + where -- Use the magic of rnBndr2 to go under the binders + menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 } + +match menv subst (PredTy p1) (PredTy p2) + = match_pred menv subst p1 p2 +match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) + | tc1 == tc2 = match_tys menv subst tys1 tys2 +match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) + = do { subst' <- match menv subst ty1a ty2a + ; match menv subst' ty1b ty2b } +match menv subst (AppTy ty1a ty1b) ty2 + | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2 + = do { subst' <- match menv subst ty1a ty2a + ; match menv subst' ty1b ty2b } + +match menv subst ty1 ty2 + = Nothing + +-------------- +match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2 + +-------------- +match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv) + -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv +match_list fn subst [] [] = Just subst +match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2 + ; match_list fn subst' tys1 tys2 } +match_list fn subst tys1 tys2 = Nothing + +-------------- +match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2) + | c1 == c2 = match_tys menv subst tys1 tys2 +match_pred menv subst (IParam n1 t1) (IParam n2 t2) + | n1 == n2 = match menv subst t1 t2 +match_pred menv subst p1 p2 = Nothing +\end{code} + + +%************************************************************************ +%* * + The workhorse %* * %************************************************************************ \begin{code} ----------------------------- tcRefineTys, tcMatchTys :: [TyVar] -- Try to unify these -> TvSubstEnv -- Not idempotent -> [Type] -> [Type] - -> MaybeErr TvSubstEnv Message -- Not idempotent + -> MaybeErr Message TvSubstEnv -- Not idempotent -- This one is used by the type checker. Neither the input nor result -- substitition is idempotent tcRefineTys ex_tvs subst tys1 tys2 - = initUM (tryToBind (mkVarSet ex_tvs)) (unify_tys Src subst tys1 tys2) + = initUM (tryToBind (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2) tcMatchTys ex_tvs subst tys1 tys2 - = initUM (bindOnly (mkVarSet ex_tvs)) (unify_tys Src subst tys1 tys2) - -tcMatchPreds - :: [TyVar] -- Bind these - -> [PredType] -> [PredType] - -> Maybe TvSubstEnv -tcMatchPreds tvs preds1 preds2 - = maybeErrToMaybe $ initUM (bindOnly (mkVarSet tvs)) $ - unify_preds Src emptyVarEnv preds1 preds2 + = initUM (bindOnly (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2) ---------------------------- coreRefineTys :: [TyVar] -- Try to unify these @@ -70,7 +209,7 @@ coreRefineTys ex_tvs subst@(TvSubst in_scope orig_env) ty1 ty2 do { -- Apply the input substitution; nothing int ty2 let ty1' = substTy subst ty1 -- Run the unifier, starting with an empty env - ; extra_env <- unify Src emptyTvSubstEnv ty1' ty2 + ; extra_env <- unify emptyTvSubstEnv ty1' ty2 -- Find the fixed point of the resulting non-idempotent -- substitution, and apply it to the @@ -81,53 +220,15 @@ coreRefineTys ex_tvs subst@(TvSubst in_scope orig_env) ty1 ty2 ---------------------------- -matchTys :: TyVarSet -- Template tyvars - -> [Type] -- Template - -> [Type] -- Target - -> Maybe TvSubstEnv -- Idempotent, because when matching - -- the range and domain are distinct - --- PRE-CONDITION for matching: template variables are not free in the target - -matchTys tmpls tys1 tys2 - = ASSERT2( not (intersectsVarSet tmpls (tyVarsOfTypes tys2)), - ppr tmpls $$ ppr tys1 $$ ppr tys2 ) - maybeErrToMaybe $ initUM (bindOnly tmpls) - (unify_tys Src emptyTvSubstEnv tys1 tys2) - -matchTyX :: TyVarSet -- Template tyvars - -> TvSubstEnv -- Idempotent substitution to extend - -> Type -- Template - -> Type -- Target - -> Maybe TvSubstEnv -- Idempotent - -matchTyX tmpls env ty1 ty2 - = ASSERT( not (intersectsVarSet tmpls (tyVarsOfType ty2)) ) - maybeErrToMaybe $ initUM (bindOnly tmpls) - (unify Src env ty1 ty2) - -matchTysX :: TyVarSet -- Template tyvars - -> TvSubstEnv -- Idempotent substitution to extend - -> [Type] -- Template - -> [Type] -- Target - -> Maybe TvSubstEnv -- Idempotent - -matchTysX tmpls env tys1 tys2 - = ASSERT( not (intersectsVarSet tmpls (tyVarsOfTypes tys2)) ) - maybeErrToMaybe $ initUM (bindOnly tmpls) - (unify_tys Src env tys1 tys2) - - ----------------------------- unifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv unifyTys bind_these tys1 tys2 = maybeErrToMaybe $ initUM (bindOnly bind_these) $ - unify_tys Src emptyTvSubstEnv tys1 tys2 + unify_tys emptyTvSubstEnv tys1 tys2 unifyTysX :: TyVarSet -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv unifyTysX bind_these subst tys1 tys2 = maybeErrToMaybe $ initUM (bindOnly bind_these) $ - unify_tys Src subst tys1 tys2 + unify_tys subst tys1 tys2 ---------------------------- tryToBind, bindOnly :: TyVarSet -> TyVar -> BindFlag @@ -149,8 +250,7 @@ emptyTvSubstEnv = emptyVarEnv %************************************************************************ \begin{code} -unify :: SrcFlag -- True, unifying source types, false core types. - -> TvSubstEnv -- An existing substitution to extend +unify :: TvSubstEnv -- An existing substitution to extend -> Type -> Type -- Types to be unified -> UM TvSubstEnv -- Just the extended substitution, -- Nothing if unification failed @@ -158,64 +258,47 @@ unify :: SrcFlag -- True, unifying source types, false core types -- nor guarantee that the outgoing one is. That's fixed up by -- the wrappers. -unify s subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $ - unify_ s subst (rep s ty1) (rep s ty2) - -rep :: SrcFlag -> Type -> Type -- Strip off the clutter -rep Src (NoteTy _ ty) = rep Src ty -rep Core ty | Just ty' <- coreView ty = rep Core ty' -rep s ty = ty +unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $ + unify_ subst ty1 ty2 -- in unify_, any NewTcApps/Preds should be taken at face value -unify_ s subst (TyVarTy tv1) ty2 = uVar s False subst tv1 ty2 -unify_ s subst ty1 (TyVarTy tv2) = uVar s True subst tv2 ty1 +unify_ subst (TyVarTy tv1) ty2 = uVar False subst tv1 ty2 +unify_ subst ty1 (TyVarTy tv2) = uVar True subst tv2 ty1 -unify_ s subst (PredTy p1) (PredTy p2) = unify_pred s subst p1 p2 +unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2 -unify_ s subst t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) - | tyc1 == tyc2 = unify_tys s subst tys1 tys2 +unify_ subst t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) + | tyc1 == tyc2 = unify_tys subst tys1 tys2 -unify_ s subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) - = do { subst' <- unify s subst ty1a ty2a - ; unify s subst' ty1b ty2b } +unify_ subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) + = do { subst' <- unify subst ty1a ty2a + ; unify subst' ty1b ty2b } -- Applications need a bit of care! -- They can match FunTy and TyConApp, so use splitAppTy_maybe -- NB: we've already dealt with type variables and Notes, -- so if one type is an App the other one jolly well better be too -unify_ s subst (AppTy ty1a ty1b) ty2 - | Just (ty2a, ty2b) <- unifySplitAppTy_maybe ty2 - = do { subst' <- unify s subst ty1a ty2a - ; unify s subst' ty1b ty2b } +unify_ subst (AppTy ty1a ty1b) ty2 + | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2 + = do { subst' <- unify subst ty1a ty2a + ; unify subst' ty1b ty2b } -unify_ s subst ty1 (AppTy ty2a ty2b) - | Just (ty1a, ty1b) <- unifySplitAppTy_maybe ty1 - = do { subst' <- unify s subst ty1a ty2a - ; unify s subst' ty1b ty2b } +unify_ subst ty1 (AppTy ty2a ty2b) + | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1 + = do { subst' <- unify subst ty1a ty2a + ; unify subst' ty1b ty2b } -unify_ s subst ty1 ty2 = failWith (misMatch ty1 ty2) +unify_ subst ty1 ty2 = failWith (misMatch ty1 ty2) ------------------------------ -unify_pred s subst (ClassP c1 tys1) (ClassP c2 tys2) - | c1 == c2 = unify_tys s subst tys1 tys2 -unify_pred s subst (IParam n1 t1) (IParam n2 t2) - | n1 == n2 = unify s subst t1 t2 +unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2) + | c1 == c2 = unify_tys subst tys1 tys2 +unify_pred subst (IParam n1 t1) (IParam n2 t2) + | n1 == n2 = unify subst t1 t2 +unify_pred subst p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2)) ------------------------------ -unifySplitAppTy_maybe :: Type -> Maybe (Type,Type) --- NoteTy is already dealt with; take NewTcApps at face value -unifySplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) -unifySplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) -unifySplitAppTy_maybe (TyConApp tc tys) = case snocView tys of - Just (tys', ty') -> Just (TyConApp tc tys', ty') - Nothing -> Nothing -unifySplitAppTy_maybe other = Nothing - ------------------------------- -unify_tys s = unifyList (unify s) - -unify_preds :: SrcFlag -> TvSubstEnv -> [PredType] -> [PredType] -> UM TvSubstEnv -unify_preds s = unifyList (unify_pred s) +unify_tys = unifyList unify unifyList :: Outputable a => (TvSubstEnv -> a -> a -> UM TvSubstEnv) @@ -229,19 +312,18 @@ unifyList unifier subst orig_xs orig_ys go subst _ _ = failWith (lengthMisMatch orig_xs orig_ys) ------------------------------ -uVar :: SrcFlag -- True, unifying source types, false core types. - -> Bool -- Swapped +uVar :: Bool -- Swapped -> TvSubstEnv -- An existing substitution to extend -> TyVar -- Type variable to be unified -> Type -- with this type -> UM TvSubstEnv -uVar s swap subst tv1 ty +uVar swap subst tv1 ty = -- check to see whether tv1 is refined case (lookupVarEnv subst tv1) of -- yes, call back into unify' - Just ty' | swap -> unify s subst ty ty' - | otherwise -> unify s subst ty' ty + Just ty' | swap -> unify subst ty ty' + | otherwise -> unify subst ty' ty -- No, continue Nothing -> uUnrefined subst tv1 ty @@ -331,15 +413,10 @@ bindTv subst tv ty = return (extendVarEnv subst tv ty) %************************************************************************ \begin{code} -data SrcFlag = Src | Core -- Unifying at the source level, or core level? - data BindFlag = BindMe | AvoidMe | DontBindMe -isCore Core = True -isCore Src = False - newtype UM a = UM { unUM :: (TyVar -> BindFlag) - -> MaybeErr a Message } + -> MaybeErr Message a } instance Monad UM where return a = UM (\tvs -> Succeeded a) @@ -348,7 +425,7 @@ instance Monad UM where Failed err -> Failed err Succeeded v -> unUM (k v) tvs) -initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr a Message +initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a initUM badtvs um = unUM um badtvs tvBindFlag :: TyVar -> UM BindFlag @@ -357,9 +434,19 @@ tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv)) failWith :: Message -> UM a failWith msg = UM (\tv_fn -> Failed msg) -maybeErrToMaybe :: MaybeErr succ fail -> Maybe succ +maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ maybeErrToMaybe (Succeeded a) = Just a maybeErrToMaybe (Failed m) = Nothing + +------------------------------ +repSplitAppTy_maybe :: Type -> Maybe (Type,Type) +-- Like Type.splitAppTy_maybe, but any coreView stuff is already done +repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) +repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) +repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of + Just (tys', ty') -> Just (TyConApp tc tys', ty') + Nothing -> Nothing +repSplitAppTy_maybe other = Nothing \end{code} diff --git a/ghc/compiler/utils/Maybes.lhs b/ghc/compiler/utils/Maybes.lhs index 961da18..3c9bd69 100644 --- a/ghc/compiler/utils/Maybes.lhs +++ b/ghc/compiler/utils/Maybes.lhs @@ -7,7 +7,8 @@ module Maybes ( module Maybe, -- Re-export all of Maybe - MaybeErr(..), + MaybeErr(..), -- Instance of Monad + failME, orElse, mapCatMaybes, @@ -16,10 +17,7 @@ module Maybes ( expectJust, maybeToBool, - thenMaybe, seqMaybe, returnMaybe, failMaybe, - - thenMaB, returnMaB, failMaB - + thenMaybe, seqMaybe, returnMaybe, failMaybe ) where #include "HsVersions.h" @@ -113,20 +111,13 @@ Nothing `orElse` y = y %************************************************************************ \begin{code} -data MaybeErr val err = Succeeded val | Failed err -\end{code} - -\begin{code} -thenMaB :: MaybeErr val1 err -> (val1 -> MaybeErr val2 err) -> MaybeErr val2 err -thenMaB m k - = case m of - Succeeded v -> k v - Failed e -> Failed e +data MaybeErr err val = Succeeded val | Failed err -returnMaB :: val -> MaybeErr val err -returnMaB v = Succeeded v +instance Monad (MaybeErr err) where + return v = Succeeded v + Succeeded v >>= k = k v + Failed e >>= k = Failed e -failMaB :: err -> MaybeErr val err -failMaB e = Failed e +failME :: err -> MaybeErr err val +failME e = Failed e \end{code} - diff --git a/ghc/compiler/utils/Util.lhs b/ghc/compiler/utils/Util.lhs index feeb687..6d2be04 100644 --- a/ghc/compiler/utils/Util.lhs +++ b/ghc/compiler/utils/Util.lhs @@ -33,7 +33,7 @@ module Util ( takeList, dropList, splitAtList, -- comparisons - eqListBy, equalLength, compareLength, + isEqual, eqListBy, equalLength, compareLength, thenCmp, cmpList, prefixMatch, suffixMatch, maybePrefixMatch, -- strictness @@ -577,6 +577,17 @@ splitAtList (_:xs) (y:ys) = (y:ys', ys'') %************************************************************************ \begin{code} +isEqual :: Ordering -> Bool +-- Often used in (isEqual (a `compare` b)) +isEqual GT = False +isEqual EQ = True +isEqual LT = False + +thenCmp :: Ordering -> Ordering -> Ordering +{-# INLINE thenCmp #-} +thenCmp EQ any = any +thenCmp other any = other + eqListBy :: (a->a->Bool) -> [a] -> [a] -> Bool eqListBy eq [] [] = True eqListBy eq (x:xs) (y:ys) = eq x y && eqListBy eq xs ys @@ -593,11 +604,6 @@ compareLength (_:xs) (_:ys) = compareLength xs ys compareLength [] _ys = LT compareLength _xs [] = GT -thenCmp :: Ordering -> Ordering -> Ordering -{-# INLINE thenCmp #-} -thenCmp EQ any = any -thenCmp other any = other - cmpList :: (a -> a -> Ordering) -> [a] -> [a] -> Ordering -- `cmpList' uses a user-specified comparer -- 1.7.10.4