Commit 1b1190e0 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Add non-recursive let-bindings for types

This patch adds to Core the ability to say
	let a = Int in <body>
where 'a' is a type variable.  That is: a type-let.
See Note [Type let] in CoreSyn.

* The binding is always non-recursive
* The simplifier immediately eliminates it by substitution 

So in effect a type-let is just a delayed substitution.  This is convenient
in a couple of places in the desugarer, one existing (see the call to
CoreTyn.mkTyBind in DsUtils), and one that's in the next upcoming patch.

The first use in the desugarer was previously encoded as
	(/\a. <body>) Int
rather that eagerly substituting, but that was horrid because Core Lint
had do "know" that a=Int inside <body> else it would bleat.  Expressing
it directly as a 'let' seems much nicer.
parent 628ca41d
......@@ -114,21 +114,15 @@ Outstanding issues:
-- may well be happening...);
Note [Type lets]
~~~~~~~~~~~~~~~~
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
In the desugarer, it's very very convenient to be able to say (in effect)
let a = Int in <body>
That is, use a type let. (See notes just below for why we want this.)
We don't have type lets in Core, so the desugarer uses type lambda
(/\a. <body>) Int
However, in the lambda form, we'd get lint errors from:
(/\a. let x::a = 4 in <body>) Int
because (x::a) doesn't look compatible with (4::Int).
So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
as it were. It carries a type substitution (in this example [a -> Int])
and applies this substitution before comparing types. The functin
let a = Type Int in <body>
That is, use a type let. See Note [Type let] in CoreSyn.
However, when linting <body> we need to remember that a=Int, else we might
reject a correct program. So we carry a type substitution (in this example
[a -> Int]) and apply this substitution before comparing types. The functin
lintTy :: Type -> LintM Type
returns a substituted type; that's the only reason it returns anything.
......@@ -140,33 +134,6 @@ itself is part of the TvSubst we are carrying down), and when we
find an occurence of an Id, we fetch it from the in-scope set.
Why we need type let
~~~~~~~~~~~~~~~~~~~~
It's needed when dealing with desugarer output for GADTs. Consider
data T = forall a. T a (a->Int) Bool
f :: T -> ... ->
f (T x f True) = <e1>
f (T y g False) = <e2>
After desugaring we get
f t b = case t of
T a (x::a) (f::a->Int) (b:Bool) ->
case b of
True -> <e1>
False -> (/\b. let y=x; g=f in <e2>) a
And for a reason I now forget, the ...<e2>... can mention a; so
we want Lint to know that b=a. Ugh.
I tried quite hard to make the necessity for this go away, by changing the
desugarer, but the fundamental problem is this:
T a (x::a) (y::Int) -> let fail::a = ...
in (/\b. ...(case ... of
True -> x::b
False -> fail)
) a
Now the inner case look as though it has incompatible branches.
\begin{code}
lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
......@@ -279,6 +246,8 @@ lintCoreExpr :: CoreExpr -> LintM OutType
-- The returned type has the substitution from the monad
-- already applied to it:
-- lintCoreExpr e subst = exprType (subst e)
--
-- The returned "type" can be a kind, if the expression is (Type ty)
lintCoreExpr (Var var)
= do { checkL (not (var == oneTupleDataConId))
......@@ -307,6 +276,20 @@ lintCoreExpr (Cast expr co)
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' <- lintTy ty
; kind' <- lintTy (tyVarKind tv)
; let tv' = setTyVarKind tv kind'
; checkKinds tv' ty'
-- Now extend the substitution so we
-- take advantage of it in the body
; addLoc (BodyOfLetRec [tv]) $
addInScopeVars [tv'] $
extendSubstL tv' ty' $
lintCoreExpr body }
lintCoreExpr (Let (NonRec bndr rhs) body)
= do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
; addLoc (BodyOfLetRec [bndr])
......@@ -319,29 +302,6 @@ lintCoreExpr (Let (Rec pairs) body)
where
bndrs = map fst pairs
lintCoreExpr e@(App fun (Type ty))
-- See Note [Type let] above
= addLoc (AnExpr e) $
go fun [ty]
where
go (App fun (Type ty)) tys
= do { go fun (ty:tys) }
go (Lam tv body) (ty:tys)
= do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
; ty' <- lintTy ty
; let kind = tyVarKind tv
; kind' <- lintTy kind
; let tv' = setTyVarKind tv kind'
; checkKinds tv' ty'
-- Now extend the substitution so we
-- take advantage of it in the body
; addInScopeVars [tv'] $
extendSubstL tv' ty' $
go body tys }
go fun tys
= do { fun_ty <- lintCoreExpr fun
; lintCoreArgs fun_ty (map Type tys) }
lintCoreExpr e@(App fun arg)
= do { fun_ty <- lintCoreExpr fun
; addLoc (AnExpr e) $
......@@ -392,8 +352,9 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
where
pass_var f = f var
lintCoreExpr e@(Type _)
= addErrL (mkStrangeTyMsg e)
lintCoreExpr (Type ty)
= do { ty' <- lintTy ty
; return (typeKind ty') }
\end{code}
%************************************************************************
......@@ -607,6 +568,7 @@ lintAndScopeId id linterF
lintTy :: InType -> LintM OutType
-- Check the type, and apply the substitution to it
-- See Note [Linting type lets]
-- ToDo: check the kind structure of the type
lintTy ty
= do { ty' <- applySubst ty
......@@ -957,8 +919,4 @@ dupVars :: [[Var]] -> Message
dupVars vars
= hang (ptext (sLit "Duplicate variables brought into scope"))
2 (ppr vars)
mkStrangeTyMsg :: CoreExpr -> Message
mkStrangeTyMsg e
= ptext (sLit "Type where expression expected:") <+> ppr e
\end{code}
......@@ -20,9 +20,8 @@ module CoreSyn (
isTyVar, isId, cmpAltCon, cmpAlt, ltAlt,
bindersOf, bindersOfBinds, rhssOfBind, rhssOfAlts,
collectBinders, collectTyBinders, collectValBinders, collectTyAndValBinders,
collectArgs,
coreExprCc,
flattenBinds,
collectArgs, coreExprCc,
mkTyBind, flattenBinds,
isValArg, isTypeArg, valArgCount, valBndrCount, isRuntimeArg, isRuntimeVar,
......@@ -150,12 +149,23 @@ Invariant: The list of alternatives is ALWAYS EXHAUSTIVE,
Note [CoreSyn let goal]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~
* The simplifier tries to ensure that if the RHS of a let is a constructor
application, its arguments are trivial, so that the constructor can be
inlined vigorously.
Note [Type let]
~~~~~~~~~~~~~~~
We allow a *non-recursive* let to bind a type variable, thus
Let (NonRec tv (Type ty)) body
This can be very convenient for postponing type substitutions until
the next run of the simplifier.
At the moment, the rest of the compiler only deals with type-let
in a Let expression, rather than at top level. We may want to revist
this choice.
\begin{code}
data Note
= SCC CostCentre
......@@ -501,6 +511,11 @@ mkCast e co = Cast e co
%************************************************************************
\begin{code}
mkTyBind :: TyVar -> Type -> CoreBind
mkTyBind tv ty = NonRec tv (Type ty)
-- Note [Type let]
-- A non-recursive let can bind a type variable
bindersOf :: Bind b -> [b]
bindersOf (NonRec binder _) = [binder]
bindersOf (Rec pairs) = [binder | (binder, _) <- pairs]
......
......@@ -250,6 +250,8 @@ instance OutputableBndr Var where
pprCoreBinder :: BindingSite -> Var -> SDoc
pprCoreBinder LetBind binder
| isTyVar binder = pprTypedBinder binder
| otherwise
= vcat [sig, pprIdDetails binder, pragmas]
where
sig = pprTypedBinder binder
......
......@@ -347,10 +347,10 @@ wrapBinds [] e = e
wrapBinds ((new,old):prs) e = wrapBind new old (wrapBinds prs e)
wrapBind :: Var -> Var -> CoreExpr -> CoreExpr
wrapBind new old body
wrapBind new old body -- Can deal with term variables *or* type variables
| new==old = body
| isTyVar new = App (Lam new body) (Type (mkTyVarTy old))
| otherwise = Let (NonRec new (Var old)) body
| isTyVar new = Let (mkTyBind new (mkTyVarTy old)) body
| otherwise = Let (NonRec new (Var old)) body
seqVar :: Var -> CoreExpr -> CoreExpr
seqVar var body = Case (Var var) var (exprType body)
......
......@@ -84,7 +84,10 @@ occAnalBind :: OccEnv
[CoreBind])
occAnalBind env (NonRec binder rhs) body_usage
| not (binder `usedIn` body_usage) -- It's not mentioned
| isTyVar binder -- A type let; we don't gather usage info
= (body_usage, [NonRec binder rhs])
| not (binder `usedIn` body_usage) -- It's not mentioned
= (body_usage, [])
| otherwise -- It's mentioned in the body
......
......@@ -864,14 +864,7 @@ simplLam :: SimplEnv -> [InId] -> InExpr -> SimplCont
simplLam env [] body cont = simplExprF env body cont
-- Type-beta reduction
simplLam env (bndr:bndrs) body (ApplyTo _ (Type ty_arg) arg_se cont)
= ASSERT( isTyVar bndr )
do { tick (BetaReduction bndr)
; ty_arg' <- simplType (arg_se `setInScope` env) ty_arg
; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
-- Ordinary beta reduction
-- Beta reduction
simplLam env (bndr:bndrs) body (ApplyTo _ arg arg_se cont)
= do { tick (BetaReduction bndr)
; simplNonRecE env bndr (arg, arg_se) (bndrs, body) cont }
......@@ -904,9 +897,11 @@ simplNonRecE :: SimplEnv
-- Why? Because of the binder-occ-info-zapping done before
-- the call to simplLam in simplExprF (Lam ...)
-- First deal with type lets: let a = Type ty in b
-- First deal with type applications and type lets
-- (/\a. e) (Type ty) and (let a = Type ty in e)
simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
= do { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
= ASSERT( isTyVar bndr )
do { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment