-- 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.
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 ()
-- 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 (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])
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) $
where
pass_var f = f var
-lintCoreExpr e@(Type _)
- = addErrL (mkStrangeTyMsg e)
+lintCoreExpr (Type ty)
+ = do { ty' <- lintTy ty
+ ; return (typeKind ty') }
\end{code}
%************************************************************************
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
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}
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,
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
%************************************************************************
\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]
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 }
-- 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
projects / ghc-hetmet.git / commitdiff