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.
-- may well be happening...);
-- 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)
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.
lintTy :: Type -> LintM Type
returns a substituted type; that's the only reason it returns anything.
find an occurence of an Id, we fetch it from the in-scope set.
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 ()
\begin{code}
lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
-- The returned type has the substitution from the monad
-- already applied to it:
-- lintCoreExpr e subst = exprType (subst e)
-- 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))
lintCoreExpr (Var var)
= do { checkL (not (var == oneTupleDataConId))
lintCoreExpr (Note _ expr)
= lintCoreExpr expr
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])
lintCoreExpr (Let (NonRec bndr rhs) body)
= do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
; addLoc (BodyOfLetRec [bndr])
where
bndrs = map fst pairs
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) $
lintCoreExpr e@(App fun arg)
= do { fun_ty <- lintCoreExpr fun
; addLoc (AnExpr e) $
-lintCoreExpr e@(Type _)
- = addErrL (mkStrangeTyMsg e)
+lintCoreExpr (Type ty)
+ = do { ty' <- lintTy ty
+ ; return (typeKind ty') }
\end{code}
%************************************************************************
\end{code}
%************************************************************************
lintTy :: InType -> LintM OutType
-- Check the type, and apply the substitution to it
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
-- ToDo: check the kind structure of the type
lintTy ty
= do { ty' <- applySubst ty
dupVars vars
= hang (ptext (sLit "Duplicate variables brought into scope"))
2 (ppr vars)
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
isTyVar, isId, cmpAltCon, cmpAlt, ltAlt,
bindersOf, bindersOfBinds, rhssOfBind, rhssOfAlts,
collectBinders, collectTyBinders, collectValBinders, collectTyAndValBinders,
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,
isValArg, isTypeArg, valArgCount, valBndrCount, isRuntimeArg, isRuntimeVar,
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* 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.
* 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
\begin{code}
data Note
= SCC CostCentre
%************************************************************************
\begin{code}
%************************************************************************
\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]
bindersOf :: Bind b -> [b]
bindersOf (NonRec binder _) = [binder]
bindersOf (Rec pairs) = [binder | (binder, _) <- pairs]
pprCoreBinder :: BindingSite -> Var -> SDoc
pprCoreBinder LetBind binder
pprCoreBinder :: BindingSite -> Var -> SDoc
pprCoreBinder LetBind binder
+ | isTyVar binder = pprTypedBinder binder
+ | otherwise
= vcat [sig, pprIdDetails binder, pragmas]
where
sig = pprTypedBinder binder
= vcat [sig, pprIdDetails binder, pragmas]
where
sig = pprTypedBinder binder
wrapBinds ((new,old):prs) e = wrapBind new old (wrapBinds prs e)
wrapBind :: Var -> Var -> CoreExpr -> CoreExpr
wrapBinds ((new,old):prs) e = wrapBind new old (wrapBinds prs e)
wrapBind :: Var -> Var -> CoreExpr -> CoreExpr
+wrapBind new old body -- Can deal with term variables *or* type variables
- | 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)
seqVar :: Var -> CoreExpr -> CoreExpr
seqVar var body = Case (Var var) var (exprType body)
[CoreBind])
occAnalBind env (NonRec binder rhs) body_usage
[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
= (body_usage, [])
| otherwise -- It's mentioned in the body
simplLam env [] body cont = simplExprF env body cont
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
simplLam env (bndr:bndrs) body (ApplyTo _ arg arg_se cont)
= do { tick (BetaReduction bndr)
; simplNonRecE env bndr (arg, arg_se) (bndrs, body) cont }
simplLam env (bndr:bndrs) body (ApplyTo _ arg arg_se cont)
= do { tick (BetaReduction bndr)
; simplNonRecE env bndr (arg, arg_se) (bndrs, body) cont }
-- Why? Because of the binder-occ-info-zapping done before
-- the call to simplLam in simplExprF (Lam ...)
-- 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
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
; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont