Commit d2ce0f52 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Super-monster patch implementing the new typechecker -- at last

This major patch implements the new OutsideIn constraint solving
algorithm in the typecheker, following our JFP paper "Modular type
inference with local assumptions".  

Done with major help from Dimitrios Vytiniotis and Brent Yorgey.
parent 0084ab49
......@@ -56,7 +56,7 @@ name = Util.globalMVar (value);
#ifdef DEBUG
#define ASSERT(e) if (not (e)) then (assertPanic __FILE__ __LINE__) else
#define ASSERT2(e,msg) if (not (e)) then (assertPprPanic __FILE__ __LINE__ (msg)) else
#define WARN( e, msg ) (warnPprTrace (e) __FILE__ __LINE__ (msg))
#define WARN( e, msg ) (warnPprTrace (e) __FILE__ __LINE__ (msg)) $
#else
-- We have to actually use all the variables we are given or we may get
-- unused variable warnings when DEBUG is off.
......
......@@ -30,7 +30,7 @@ module Id (
mkLocalId, mkLocalIdWithInfo, mkExportedLocalId,
mkSysLocal, mkSysLocalM, mkUserLocal, mkUserLocalM,
mkTemplateLocals, mkTemplateLocalsNum, mkTemplateLocal,
mkWorkerId,
mkWorkerId, mkWiredInIdName,
-- ** Taking an Id apart
idName, idType, idUnique, idInfo, idDetails,
......@@ -258,6 +258,9 @@ mkUserLocal occ uniq ty loc = mkLocalId (mkInternalName uniq occ loc) ty
mkUserLocalM :: MonadUnique m => OccName -> Type -> SrcSpan -> m Id
mkUserLocalM occ ty loc = getUniqueM >>= (\uniq -> return (mkUserLocal occ uniq ty loc))
mkWiredInIdName :: Module -> FastString -> Unique -> Id -> Name
mkWiredInIdName mod fs uniq id
= mkWiredInName mod (mkOccNameFS varName fs) uniq (AnId id) UserSyntax
\end{code}
Make some local @Ids@ for a template @CoreExpr@. These have bogus
......
This diff is collapsed.
......@@ -25,8 +25,8 @@
-- Global 'Id's and 'Var's are those that are imported or correspond to a data constructor, primitive operation, or record selectors.
-- Local 'Id's and 'Var's are those bound within an expression (e.g. by a lambda) or at the top level of the module being compiled.
module Var (
-- * The main data type
Var,
-- * The main data type and synonyms
Var, TyVar, CoVar, Id, DictId, DFunId, EvVar, EvId, IpId,
-- ** Taking 'Var's apart
varName, varUnique, varType,
......@@ -41,14 +41,11 @@ module Var (
setIdExported, setIdNotExported,
-- ** Predicates
isCoVar, isId, isTyVar, isTcTyVar,
isCoVar, isId, isTyCoVar, isTyVar, isTcTyVar,
isLocalVar, isLocalId,
isGlobalId, isExportedId,
mustHaveLocalBinding,
-- * Type variable data type
TyVar,
-- ** Constructing 'TyVar's
mkTyVar, mkTcTyVar, mkWildCoVar,
......@@ -58,9 +55,6 @@ module Var (
-- ** Modifying 'TyVar's
setTyVarName, setTyVarUnique, setTyVarKind,
-- * Coercion variable data type
CoVar,
-- ** Constructing 'CoVar's
mkCoVar,
......@@ -68,10 +62,8 @@ module Var (
coVarName,
-- ** Modifying 'CoVar's
setCoVarUnique, setCoVarName,
setCoVarUnique, setCoVarName
-- * 'Var' type synonyms
Id, DictId
) where
#include "HsVersions.h"
......@@ -93,6 +85,30 @@ import Data.Data
\end{code}
%************************************************************************
%* *
Synonyms
%* *
%************************************************************************
-- These synonyms are here and not in Id because otherwise we need a very
-- large number of SOURCE imports of Id.hs :-(
\begin{code}
type EvVar = Var -- An evidence variable: dictionary or equality constraint
-- Could be an DictId or a CoVar
type Id = Var -- A term-level identifier
type DFunId = Id -- A dictionary function
type EvId = Id -- Term-level evidence: DictId or IpId
type DictId = EvId -- A dictionary variable
type IpId = EvId -- A term-level implicit parameter
type TyVar = Var
type CoVar = TyVar -- A coercion variable is simply a type
-- variable of kind @ty1 ~ ty2@. Hence its
-- 'varType' is always @PredTy (EqPred t1 t2)@
\end{code}
%************************************************************************
%* *
\subsection{The main data type declarations}
......@@ -124,7 +140,7 @@ data Var
varName :: !Name,
realUnique :: FastInt,
varType :: Kind,
tcTyVarDetails :: TcTyVarDetails }
tc_tv_details :: TcTyVarDetails }
| Id {
varName :: !Name,
......@@ -166,7 +182,7 @@ instance Outputable Var where
ppr_debug :: Var -> SDoc
ppr_debug (TyVar {}) = ptext (sLit "tv")
ppr_debug (TcTyVar {tcTyVarDetails = d}) = pprTcTyVarDetails d
ppr_debug (TcTyVar {tc_tv_details = d}) = pprTcTyVarDetails d
ppr_debug (Id { idScope = s, id_details = d }) = ppr_id_scope s <> pprIdDetails d
ppr_id_scope :: IdScope -> SDoc
......@@ -229,8 +245,6 @@ setVarType id ty = id { varType = ty }
%************************************************************************
\begin{code}
type TyVar = Var
tyVarName :: TyVar -> Name
tyVarName = varName
......@@ -262,8 +276,12 @@ mkTcTyVar name kind details
TcTyVar { varName = name,
realUnique = getKeyFastInt (nameUnique name),
varType = kind,
tcTyVarDetails = details
tc_tv_details = details
}
tcTyVarDetails :: TyVar -> TcTyVarDetails
tcTyVarDetails (TcTyVar { tc_tv_details = details }) = details
tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var)
\end{code}
%************************************************************************
......@@ -273,10 +291,6 @@ mkTcTyVar name kind details
%************************************************************************
\begin{code}
type CoVar = TyVar -- A coercion variable is simply a type
-- variable of kind @ty1 ~ ty2@. Hence its
-- 'varType' is always @PredTy (EqPred t1 t2)@
coVarName :: CoVar -> Name
coVarName = varName
......@@ -307,11 +321,6 @@ mkWildCoVar = mkCoVar (mkSysTvName (mkBuiltinUnique 1) (fsLit "co_wild"))
%************************************************************************
\begin{code}
-- These synonyms are here and not in Id because otherwise we need a very
-- large number of SOURCE imports of Id.hs :-(
type Id = Var
type DictId = Var
idInfo :: Id -> IdInfo
idInfo (Id { id_info = info }) = info
idInfo other = pprPanic "idInfo" (ppr other)
......@@ -375,11 +384,20 @@ setIdNotExported id = ASSERT( isLocalId id )
%************************************************************************
\begin{code}
isTyVar :: Var -> Bool -- True of both type and coercion variables
isTyVar (TyVar {}) = True
isTyCoVar :: Var -> Bool -- True of both type and coercion variables
isTyCoVar (TyVar {}) = True
isTyCoVar (TcTyVar {}) = True
isTyCoVar _ = False
isTyVar :: Var -> Bool -- True of both type variables only
isTyVar v@(TyVar {}) = not (isCoercionVar v)
isTyVar (TcTyVar {}) = True
isTyVar _ = False
isCoVar :: Var -> Bool -- Only works after type checking (sigh)
isCoVar v@(TyVar {}) = isCoercionVar v
isCoVar _ = False
isTcTyVar :: Var -> Bool
isTcTyVar (TcTyVar {}) = True
isTcTyVar _ = False
......@@ -392,11 +410,6 @@ isLocalId :: Var -> Bool
isLocalId (Id { idScope = LocalId _ }) = True
isLocalId _ = False
isCoVar :: Var -> Bool
isCoVar (v@(TyVar {})) = isCoercionVar v
isCoVar (TcTyVar {varType = kind}) = isCoercionKind kind -- used during solving
isCoVar _ = False
-- | 'isLocalVar' returns @True@ for type variables as well as local 'Id's
-- These are the variables that we need to pay attention to when finding free
-- variables, or doing dependency analysis.
......
......@@ -27,7 +27,8 @@ module VarEnv (
-- ** Operations on InScopeSets
emptyInScopeSet, mkInScopeSet, delInScopeSet,
extendInScopeSet, extendInScopeSetList, extendInScopeSetSet,
getInScopeVars, lookupInScope, elemInScopeSet, uniqAway,
getInScopeVars, lookupInScope, lookupInScope_Directly,
elemInScopeSet, uniqAway,
-- * The RnEnv2 type
RnEnv2,
......@@ -114,6 +115,10 @@ elemInScopeSet v (InScope in_scope _) = v `elemVarEnv` in_scope
-- the variable's identity (unique) to its full value.
lookupInScope :: InScopeSet -> Var -> Maybe Var
lookupInScope (InScope in_scope _) v = lookupVarEnv in_scope v
lookupInScope_Directly :: InScopeSet -> Unique -> Maybe Var
lookupInScope_Directly (InScope in_scope _) uniq
= lookupVarEnv_Directly in_scope uniq
\end{code}
\begin{code}
......
{-# OPTIONS_GHC -XNoMonoLocalBinds #-}
-- Norman likes local bindings
-- If this module lives on I'd like to get rid of this flag in due course
module CmmBuildInfoTables
( CAFSet, CAFEnv, CmmTopForInfoTables(..), cafAnal, localCAFInfo, mkTopCAFInfo
, setInfoTableSRT, setInfoTableStackMap
......
......@@ -235,6 +235,7 @@ gatherBlocksIntoContinuation live proc_points blocks start =
children = (collectNonProcPointTargets proc_points blocks (unitUniqSet start) [start]) `minusUniqSet` (unitUniqSet start)
start_block = lookupWithDefaultBEnv blocks unknown_block start
children_blocks = map (lookupWithDefaultBEnv blocks unknown_block) (uniqSetToList children)
unknown_block :: a -- Used at more than one type
unknown_block = panic "unknown block in gatherBlocksIntoContinuation"
body = start_block : children_blocks
......
{-# OPTIONS_GHC -XNoMonoLocalBinds #-}
-- Norman likes local bindings
-- If this module lives on I'd like to get rid of this flag in due course
module CmmCPSZ (
-- | Converts C-- with full proceedures and parameters
-- to a CPS transformed C-- with the stack made manifest.
......@@ -153,7 +157,10 @@ cpsTop hsc_env (CmmProc h l args (stackInfo@(entry_off, _), g)) =
where dflags = hsc_dflags hsc_env
mbpprTrace x y z = if dopt Opt_D_dump_cmmz dflags then pprTrace x y z else z
dump f txt g = dumpIfSet_dyn dflags f txt (ppr g)
run :: FuelMonad a -> IO a
run = runFuelIO (hsc_OptFuel hsc_env)
dual_rewrite flag txt pass g =
do dump flag ("Pre " ++ txt) g
g <- run $ pass g
......
{-# OPTIONS_GHC -XNoMonoLocalBinds #-}
-- Norman likes local bindings
-- If this module lives on I'd like to get rid of this flag in due course
module CmmSpillReload
( DualLive(..)
......
{-# OPTIONS_GHC -XNoMonoLocalBinds #-}
-- Norman likes local bindings
-- If this module lives on I'd like to get rid of this flag in due course
module CmmStackLayout
( SlotEnv, liveSlotAnal, liveSlotTransfers, removeLiveSlotDefs
, layout, manifestSP, igraph, areaBuilder
......
......@@ -461,25 +461,32 @@ postorder_dfs g@(LGraph _ blockenv) =
let FGraph id eblock _ = entry g in
zip eblock : postorder_dfs_from_except blockenv eblock (unitBlockSet id)
postorder_dfs_from_except :: (HavingSuccessors b, LastNode l)
postorder_dfs_from_except :: forall m b l. (HavingSuccessors b, LastNode l)
=> BlockEnv (Block m l) -> b -> BlockSet -> [Block m l]
postorder_dfs_from_except blocks b visited =
vchildren (get_children b) (\acc _visited -> acc) [] visited
postorder_dfs_from_except blocks b visited
= vchildren (get_children b) (\acc _visited -> acc) [] visited
where
-- vnode ::
-- Block m l -> ([Block m l] -> BlockSet -> a) -> [Block m l] -> BlockSet -> a
vnode :: Block m l -> ([Block m l] -> BlockSet -> a)
-> [Block m l] -> BlockSet -> a
vnode block@(Block id _) cont acc visited =
if elemBlockSet id visited then
cont acc visited
else
let cont' acc visited = cont (block:acc) visited in
vchildren (get_children block) cont' acc (extendBlockSet visited id)
vchildren :: [Block m l] -> ([Block m l] -> BlockSet -> a)
-> [Block m l] -> BlockSet -> a
vchildren bs cont acc visited =
let next children acc visited =
case children of [] -> cont acc visited
(b:bs) -> vnode b (next bs) acc visited
in next bs acc visited
get_children :: HavingSuccessors c => c -> [Block m l]
get_children block = foldl add_id [] (succs block)
add_id :: [Block m l] -> BlockId -> [Block m l]
add_id rst id = case lookupBlockEnv blocks id of
Just b -> b : rst
Nothing -> rst
......
{-# OPTIONS_GHC -XNoMonoLocalBinds #-}
-- Norman likes local bindings
-- This module is pure representation and should be imported only by
-- clients that need to manipulate representation and know what
-- they're doing. Clients that need to create flow graphs should
......
......@@ -528,8 +528,14 @@ forward_sol check_maybe = forw
; b <- finish
; return (b, fuel)
}
-- The need for both k1 and k2 suggests that maybe there's an opportunity
-- for improvement here -- in most cases, they're the same...
rec_rewrite :: forall t bI bW.
Maybe (AGraph m l) -> t -> DFM a bW
-> (t -> Fuel -> DFM a bI)
-> (bW -> Fuel -> DFM a bI)
-> a -> Fuel -> DFM a bI
rec_rewrite rewritten analyzed finish k1 k2 in' fuel =
case check_maybe fuel rewritten of -- fr_first rewrites id idfact of
Nothing -> k1 analyzed fuel
......@@ -589,7 +595,6 @@ forward_rew
-> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
forward_rew check_maybe = forw
where
solve = forward_sol check_maybe
forw :: RewritingDepth
-> BlockEnv a
-> PassName
......@@ -607,7 +612,8 @@ forward_rew check_maybe = forw
in_fact `seq` g `seq`
let Graph entry blockenv = g
blocks = G.postorder_dfs_from blockenv entry
in do { _ <- solve depth name start transfers rewrites in_fact g fuel
in do { _ <- forward_sol check_maybe depth name start
transfers rewrites in_fact g fuel
; eid <- freshBlockId "temporary entry id"
; (rewritten, fuel) <-
rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
......@@ -615,11 +621,18 @@ forward_rew check_maybe = forw
; a <- finish
; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
}
don't_rewrite :: forall t.
BlockEnv a -> DFM a t -> a
-> Graph m l -> Fuel
-> DFM a (t, Graph m l, Fuel)
don't_rewrite facts finish in_fact g fuel =
do { _ <- solve depth name facts transfers rewrites in_fact g fuel
do { _ <- forward_sol check_maybe depth name facts
transfers rewrites in_fact g fuel
; a <- finish
; return (a, g, fuel)
}
inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
where inner_rew' = case depth of RewriteShallow -> don't_rewrite
......@@ -633,6 +646,7 @@ forward_rew check_maybe = forw
; let fp = FFP cfp last_outs
; return (fp, fuel)
}
-- JD: WHY AREN'T WE TAKING ANY FUEL HERE?
rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
-> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
......@@ -1028,8 +1042,9 @@ run dir name do_block blocks b =
pprFacts depth n env =
my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
(nest 2 $ vcat $ map pprFact $ blockEnvToList env))
pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
pprFact :: (Outputable a, Outputable b) => (a,b) -> SDoc
pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)
f4sep :: [SDoc] -> SDoc
f4sep [] = fsep []
......
......@@ -612,7 +612,7 @@ etaExpand n orig_expr
-- Strip off existing lambdas and casts
-- Note [Eta expansion and SCCs]
go 0 expr = expr
go n (Lam v body) | isTyVar v = Lam v (go n body)
go n (Lam v body) | isTyCoVar v = Lam v (go n body)
| otherwise = Lam v (go (n-1) body)
go n (Cast expr co) = Cast (go n expr) co
go n expr = -- pprTrace "ee" (vcat [ppr orig_expr, ppr expr, ppr etas]) $
......@@ -655,7 +655,7 @@ etaInfoApp :: Subst -> CoreExpr -> [EtaInfo] -> CoreExpr
etaInfoApp subst (Lam v1 e) (EtaVar v2 : eis)
= etaInfoApp subst' e eis
where
subst' | isTyVar v1 = CoreSubst.extendTvSubst subst v1 (mkTyVarTy v2)
subst' | isTyCoVar v1 = CoreSubst.extendTvSubst subst v1 (mkTyVarTy v2)
| otherwise = CoreSubst.extendIdSubst subst v1 (Var v2)
etaInfoApp subst (Cast e co1) eis
......
......@@ -395,7 +395,7 @@ idFreeVars id = ASSERT( isId id)
bndrRuleAndUnfoldingVars ::Var -> VarSet
-- A 'let' can bind a type variable, and idRuleVars assumes
-- it's seeing an Id. This function tests first.
bndrRuleAndUnfoldingVars v | isTyVar v = emptyVarSet
bndrRuleAndUnfoldingVars v | isTyCoVar v = emptyVarSet
| otherwise = idRuleAndUnfoldingVars v
idRuleAndUnfoldingVars :: Id -> VarSet
......
......@@ -229,9 +229,9 @@ lintCoreExpr (Note _ expr)
= lintCoreExpr expr
lintCoreExpr (Let (NonRec tv (Type ty)) body)
= -- See Note [Type let] in CoreSyn
do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
; ty' <- lintInTy ty
| isTyVar tv
= -- See Note [Linting type lets]
do { ty' <- addLoc (RhsOf tv) $ lintInTy ty
; lintTyBndr tv $ \ tv' ->
addLoc (BodyOfLetRec [tv]) $
extendSubstL tv' ty' $ do
......@@ -240,6 +240,19 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body)
-- take advantage of it in the body
; lintCoreExpr body } }
| isCoVar tv
= do { co <- applySubst ty
; (s1,s2) <- addLoc (RhsOf tv) $ lintCoercion co
; lintTyBndr tv $ \ tv' ->
addLoc (BodyOfLetRec [tv]) $ do
{ let (t1,t2) = coVarKind tv'
; checkTys s1 t1 (mkTyVarLetErr tv ty)
; checkTys s2 t2 (mkTyVarLetErr tv ty)
; lintCoreExpr body } }
| otherwise
= failWithL (mkTyVarLetErr tv ty) -- Not quite accurate
lintCoreExpr (Let (NonRec bndr rhs) body)
= do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
; addLoc (BodyOfLetRec [bndr])
......@@ -279,7 +292,7 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
Just (tycon, _)
| debugIsOn &&
isAlgTyCon tycon &&
not (isOpenTyCon tycon) &&
not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
null (tyConDataCons tycon) ->
pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
-- This can legitimately happen for type families
......@@ -1081,6 +1094,14 @@ mkNonFunAppMsg fun_ty arg_ty arg
hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
hang (ptext (sLit "Arg:")) 4 (ppr arg)]
mkTyVarLetErr :: TyVar -> Type -> Message
mkTyVarLetErr tyvar ty
= vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"),
hang (ptext (sLit "Type/coercion variable:"))
4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
hang (ptext (sLit "Arg type/coercion:"))
4 (ppr ty)]
mkKindErrMsg :: TyVar -> Type -> Message
mkKindErrMsg tyvar arg_ty
= vcat [ptext (sLit "Kinds don't match in type application:"),
......
......@@ -465,7 +465,7 @@ rhsToBody (Cast e co)
rhsToBody expr@(Lam {})
| Just no_lam_result <- tryEtaReducePrep bndrs body
= return (emptyFloats, no_lam_result)
| all isTyVar bndrs -- Type lambdas are ok
| all isTyCoVar bndrs -- Type lambdas are ok
= return (emptyFloats, expr)
| otherwise -- Some value lambdas
= do { fn <- newVar (exprType expr)
......@@ -688,7 +688,7 @@ cpe_ExprIsTrivial (App e arg) = isTypeArg arg && cpe_ExprIsTrivial
cpe_ExprIsTrivial (Note (SCC _) _) = False
cpe_ExprIsTrivial (Note _ e) = cpe_ExprIsTrivial e
cpe_ExprIsTrivial (Cast e _) = cpe_ExprIsTrivial e
cpe_ExprIsTrivial (Lam b body) | isTyVar b = cpe_ExprIsTrivial body
cpe_ExprIsTrivial (Lam b body) | isTyCoVar b = cpe_ExprIsTrivial body
cpe_ExprIsTrivial _ = False
\end{code}
......
This diff is collapsed.
......@@ -26,7 +26,7 @@ module CoreSyn (
mkConApp, mkTyBind,
varToCoreExpr, varsToCoreExprs,
isTyVar, isId, cmpAltCon, cmpAlt, ltAlt,
isTyCoVar, isId, cmpAltCon, cmpAlt, ltAlt,
-- ** Simple 'Expr' access functions and predicates
bindersOf, bindersOfBinds, rhssOfBind, rhssOfAlts,
......@@ -87,7 +87,7 @@ import Util
import Data.Data
import Data.Word
infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`
infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`, `App`
-- Left associative, so that we can say (f `mkTyApps` xs `mkVarApps` ys)
\end{code}
......@@ -100,8 +100,6 @@ infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`
These data types are the heart of the compiler
\begin{code}
infixl 8 `App` -- App brackets to the left
-- | This is the data type that represents GHCs core intermediate language. Currently
-- GHC uses System FC <http://research.microsoft.com/~simonpj/papers/ext-f/> for this purpose,
-- which is closely related to the simpler and better known System F <http://en.wikipedia.org/wiki/System_F>.
......@@ -975,7 +973,7 @@ collectTyAndValBinders expr
collectTyBinders expr
= go [] expr
where
go tvs (Lam b e) | isTyVar b = go (b:tvs) e
go tvs (Lam b e) | isTyCoVar b = go (b:tvs) e
go tvs e = (reverse tvs, e)
collectValBinders expr
......
......@@ -17,7 +17,7 @@ import CoreSyn
import CoreArity
import Id
import IdInfo
import Type
import TcType( tidyType, tidyTyVarBndr )
import Var
import VarEnv
import UniqFM
......@@ -123,7 +123,7 @@ tidyVarOcc (_, var_env) v = lookupVarEnv var_env v `orElse` v
-- tidyBndr is used for lambda and case binders
tidyBndr :: TidyEnv -> Var -> (TidyEnv, Var)
tidyBndr env var
| isTyVar var = tidyTyVarBndr env var
| isTyCoVar var = tidyTyVarBndr env var
| otherwise = tidyIdBndr env var
tidyBndrs :: TidyEnv -> [Var] -> (TidyEnv, [Var])
......
......@@ -1112,7 +1112,7 @@ interestingArg e = go e 0
go (Note _ a) n = go a n
go (Cast e _) n = go e n
go (Lam v e) n
| isTyVar v = go e n
| isTyCoVar v = go e n
| n>0 = go e (n-1)
| otherwise = ValueArg
go (Let _ e) n = case go e n of { ValueArg -> ValueArg; _ -> NonTrivArg }
......
......@@ -38,6 +38,9 @@ module CoreUtils (
-- * Equality
cheapEqExpr, eqExpr, eqExprX,
-- * Eta reduction
tryEtaReduce,
-- * Manipulating data constructors and types
applyTypeToArgs, applyTypeToArg,
dataConOrigInstPat, dataConRepInstPat, dataConRepFSInstPat
......@@ -109,7 +112,7 @@ coreAltType (_,bs,rhs)
where
ty = exprType rhs
free_tvs = tyVarsOfType ty
bad_binder b = isTyVar b && b `elemVarSet` free_tvs
bad_binder b = isTyCoVar b && b `elemVarSet` free_tvs
coreAltsType :: [CoreAlt] -> Type
-- ^ Returns the type of the first alternative, which should be the same as for all alternatives
......@@ -142,10 +145,10 @@ Various possibilities suggest themselves:
we are doing here. It's not too expensive, I think.
\begin{code}
mkPiType :: Var -> Type -> Type
mkPiType :: EvVar -> Type -> Type
-- ^ Makes a @(->)@ type or a forall type, depending
-- on whether it is given a type variable or a term variable.
mkPiTypes :: [Var] -> Type -> Type
mkPiTypes :: [EvVar] -> Type -> Type
-- ^ 'mkPiType' for multiple type or value arguments
mkPiType v ty
......@@ -195,7 +198,7 @@ panic_msg e op_ty = pprCoreExpr e $$ ppr op_ty
\begin{code}
-- | Wrap the given expression in the coercion, dropping identity coercions and coalescing nested coercions
mkCoerceI :: CoercionI -> CoreExpr -> CoreExpr
mkCoerceI IdCo e = e
mkCoerceI (IdCo _) e = e
mkCoerceI (ACo co) e = mkCoerce co e
-- | Wrap the given expression in the coercion safely, coalescing nested coercions
......@@ -1077,7 +1080,7 @@ noteSize (SCC cc) = cc `seq` 1
noteSize (CoreNote s) = s `seq` 1 -- hdaume: core annotations
varSize :: Var -> Int
varSize b | isTyVar b = 1
varSize b | isTyCoVar b = 1
| otherwise = seqType (idType b) `seq`
megaSeqIdInfo (idInfo b) `seq`
1
......@@ -1161,6 +1164,100 @@ hashVar (_,env) v
= fromIntegral (lookupVarEnv env v `orElse` hashName (idName v))
\end{code}
%************************************************************************
%* *
Eta reduction
%* *
%************************************************************************
Note [Eta reduction conditions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We try for eta reduction here, but *only* if we get all the way to an
trivial expression. We don't want to remove extra lambdas unless we
are going to avoid allocating this thing altogether.
There are some particularly delicate points here:
* Eta reduction is not valid in general:
\x. bot /= bot
This matters, partly for old-fashioned correctness reasons but,
worse, getting it wrong can yield a seg fault. Consider
f = \x.f x
h y = case (case y of { True -> f `seq` True; False -> False }) of
True -> ...; False -> ...
If we (unsoundly) eta-reduce f to get f=f, the strictness analyser
says f=bottom, and replaces the (f `seq` True) with just
(f `cast` unsafe-co). BUT, as thing stand, 'f' got arity 1, and it
*keeps* arity 1 (perhaps also wrongly). So CorePrep eta-expands
the definition again, so that it does not termninate after all.
Result: seg-fault because the boolean case actually gets a function value.
See Trac #1947.
So it's important to to the right thing.
* Note [Arity care]: we need to be careful if we just look at f's
arity. Currently (Dec07), f's arity is visible in its own RHS (see
Note [Arity robustness] in SimplEnv) so we must *not* trust the
arity when checking that 'f' is a value. Otherwise we will
eta-reduce
f = \x. f x
to
f = f
Which might change a terminiating program (think (f `seq` e)) to a
non-terminating one. So we check for being a loop breaker first.
However for GlobalIds we can look at the arity; and for primops we
must, since they have no unfolding.
* Regardless of whether 'f' is a value, we always want to
reduce (/\a -> f a) to f
This came up in a RULE: foldr (build (/\a -> g a))
did not match foldr (build (/\b -> ...something complex...))
The type checker can insert these eta-expanded versions,
with both type and dictionary lambdas; hence the slightly
ad-hoc isDictId
* Never *reduce* arity. For example
f = \xy. g x y
Then if h has arity 1 we don't want to eta-reduce because then
f's arity would decrease, and that is bad
These delicacies are why we don't use exprIsTrivial and exprIsHNF here.
Alas.
\begin{code}
tryEtaReduce :: [Var] -> CoreExpr -> Maybe CoreExpr
tryEtaReduce bndrs body
= go (reverse bndrs) body
where
incoming_arity = count isId bndrs
go (b : bs) (App fun arg) | ok_arg b arg = go bs fun -- Loop round
go [] fun | ok_fun fun = Just fun -- Success!
go _ _ = Nothing -- Failure!
-- Note [Eta reduction conditions]
ok_fun (App fun (Type ty))
| not (any (`elemVarSet` tyVarsOfType ty) bndrs)
= ok_fun fun
ok_fun (Var fun_id)
= not (fun_id `elem` bndrs)
&& (ok_fun_id fun_id || all ok_lam bndrs)
ok_fun _fun = False
ok_fun_id fun = fun_arity fun >= incoming_arity
fun_arity fun -- See Note [Arity care]
| isLocalId fun && isLoopBreaker (idOccInfo fun) = 0
| otherwise = idArity fun
ok_lam v = isTyCoVar v || isDictId v
ok_arg b arg = varToCoreExpr b `cheapEqExpr` arg