Commit 0dad81ca authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix bogus type of case expression

Issue #17056 revealed that we were sometimes building a case
expression whose type field (in the Case constructor) was bogus.

Consider a phantom type synonym
   type S a = Int
and we want to form the case expression
   case x of K (a::*) -> (e :: S a)
We must not make the type field of the Case constructor be (S a)
because 'a' isn't in scope.  We must instead expand the synonym.

Changes in this patch:

* Expand synonyms in the new function CoreUtils.mkSingleAltCase.

* Use mkSingleAltCase in MkCore.wrapFloat, which was the proximate
  source of the bug (when called by exprIsConApp_maybe)

* Use mkSingleAltCase elsewhere

* Documentation
    CoreSyn   new invariant (6) in Note [Case expression invariants]
    CoreSyn   Note [Why does Case have a 'Type' field?]
    CoreUtils Note [Care with the type of a case expression]

* I improved Core Lint's error reporting, which was pretty
  confusing in this case, because it didn't mention that the offending
  type was the return type of a case expression.

* A little bit of cosmetic refactoring in CoreUtils
parent 17554248
......@@ -48,7 +48,7 @@ import FamInstEnv
import Coercion
import TcType
import MkCore
import CoreUtils ( exprType, mkCast )
import CoreUtils ( mkCast, mkDefaultCase )
import CoreUnfold
import Literal
import TyCon
......@@ -463,8 +463,8 @@ mkDictSelRhs clas val_index
rhs_body | new_tycon = unwrapNewTypeBody tycon (mkTyVarTys tyvars)
(Var dict_id)
| otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
[(DataAlt data_con, arg_ids, varToCoreExpr the_arg_id)]
| otherwise = mkSingleAltCase (Var dict_id) dict_id (DataAlt data_con)
arg_ids (varToCoreExpr the_arg_id)
-- varToCoreExpr needed for equality superclass selectors
-- sel a b d = case x of { MkC _ (g:a~b) _ -> CO g }
......@@ -987,7 +987,7 @@ wrapCo co rep_ty (unbox_rep, box_rep) -- co :: arg_ty ~ rep_ty
------------------------
seqUnboxer :: Unboxer
seqUnboxer v = return ([v], \e -> Case (Var v) v (exprType e) [(DEFAULT, [], e)])
seqUnboxer v = return ([v], mkDefaultCase (Var v) v)
unitUnboxer :: Unboxer
unitUnboxer v = return ([v], \e -> e)
......@@ -1014,8 +1014,8 @@ dataConArgUnpack arg_ty
,( \ arg_id ->
do { rep_ids <- mapM newLocal rep_tys
; let unbox_fn body
= Case (Var arg_id) arg_id (exprType body)
[(DataAlt con, rep_ids, body)]
= mkSingleAltCase (Var arg_id) arg_id
(DataAlt con) rep_ids body
; return (rep_ids, unbox_fn) }
, Boxer $ \ subst ->
do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys
......
......@@ -3,7 +3,8 @@
(c) The GRASP/AQUA Project, Glasgow University, 1993-1998
A ``lint'' pass to check for Core correctness
A ``lint'' pass to check for Core correctness.
See Note [Core Lint guarantee].
-}
{-# LANGUAGE CPP #-}
......@@ -78,6 +79,23 @@ import Pair
import qualified GHC.LanguageExtensions as LangExt
{-
Note [Core Lint guarantee]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Core Lint is the type-checker for Core. Using it, we get the following guarantee:
If all of:
1. Core Lint passes,
2. there are no unsafe coercions (i.e. UnsafeCoerceProv),
3. all plugin-supplied coercions (i.e. PluginProv) are valid, and
4. all case-matches are complete
then running the compiled program will not seg-fault, assuming no bugs downstream
(e.g. in the code generator). This guarantee is quite powerful, in that it allows us
to decouple the safety of the resulting program from the type inference algorithm.
However, do note point (4) above. Core Lint does not check for incomplete case-matches;
see Note [Case expression invariants] in CoreSyn, invariant (4). As explained there,
an incomplete case-match might slip by Core Lint and cause trouble at runtime.
Note [GHC Formalism]
~~~~~~~~~~~~~~~~~~~~
This file implements the type-checking algorithm for System FC, the "official"
......@@ -392,6 +410,7 @@ interactiveInScope hsc_env
-- f :: [t] -> [t]
-- where t is a RuntimeUnk (see TcType)
-- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee].
lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
-- Returns (warnings, errors)
-- If you edit this function, you may need to update the GHC formalism
......@@ -786,50 +805,8 @@ lintCoreExpr (Lam var expr)
do { body_ty <- lintCoreExpr expr
; return $ mkLamType var' body_ty }
lintCoreExpr e@(Case scrut var alt_ty alts) =
-- Check the scrutinee
do { scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
-- See Note [Join points are less general than the paper]
-- in CoreSyn
; (alt_ty, _) <- lintInTy alt_ty
; (var_ty, _) <- lintInTy (idType var)
-- We used to try to check whether a case expression with no
-- alternatives was legitimate, but this didn't work.
-- See Note [No alternatives lint check] for details.
-- See Note [Rules for floating-point comparisons] in PrelRules
; let isLitPat (LitAlt _, _ , _) = True
isLitPat _ = False
; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
(ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
"expression with literal pattern in case " ++
"analysis (see #9238).")
$$ text "scrut" <+> ppr scrut)
; case tyConAppTyCon_maybe (idType var) of
Just tycon
| debugIsOn
, isAlgTyCon tycon
, not (isAbstractTyCon tycon)
, null (tyConDataCons tycon)
, not (exprIsBottom scrut)
-> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
-- This can legitimately happen for type families
$ return ()
_otherwise -> return ()
-- Don't use lintIdBndr on var, because unboxed tuple is legitimate
; subst <- getTCvSubst
; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
; lintBinder CaseBind var $ \_ ->
do { -- Check the alternatives
mapM_ (lintCoreAlt scrut_ty alt_ty) alts
; checkCaseAlts e scrut_ty alts
; return alt_ty } }
lintCoreExpr (Case scrut var alt_ty alts)
= lintCaseExpr scrut var alt_ty alts
-- This case can't happen; linting types in expressions gets routed through
-- lintCoreArgs
......@@ -1095,6 +1072,60 @@ lintTyKind tyvar arg_ty
************************************************************************
-}
lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM OutType
lintCaseExpr scrut var alt_ty alts =
do { let e = Case scrut var alt_ty alts -- Just for error messages
-- Check the scrutinee
; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
-- See Note [Join points are less general than the paper]
-- in CoreSyn
; (alt_ty, _) <- addLoc (CaseTy scrut) $
lintInTy alt_ty
; (var_ty, _) <- addLoc (IdTy var) $
lintInTy (idType var)
-- We used to try to check whether a case expression with no
-- alternatives was legitimate, but this didn't work.
-- See Note [No alternatives lint check] for details.
-- Check that the scrutinee is not a floating-point type
-- if there are any literal alternatives
-- See CoreSyn Note [Case expression invariants] item (5)
-- See Note [Rules for floating-point comparisons] in PrelRules
; let isLitPat (LitAlt _, _ , _) = True
isLitPat _ = False
; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
(ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
"expression with literal pattern in case " ++
"analysis (see #9238).")
$$ text "scrut" <+> ppr scrut)
; case tyConAppTyCon_maybe (idType var) of
Just tycon
| debugIsOn
, isAlgTyCon tycon
, not (isAbstractTyCon tycon)
, null (tyConDataCons tycon)
, not (exprIsBottom scrut)
-> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
-- This can legitimately happen for type families
$ return ()
_otherwise -> return ()
-- Don't use lintIdBndr on var, because unboxed tuple is legitimate
; subst <- getTCvSubst
; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
-- See CoreSyn Note [Case expression invariants] item (7)
; lintBinder CaseBind var $ \_ ->
do { -- Check the alternatives
mapM_ (lintCoreAlt scrut_ty alt_ty) alts
; checkCaseAlts e scrut_ty alts
; return alt_ty } }
checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
-- a) Check that the alts are non-empty
-- b1) Check that the DEFAULT comes first, if it exists
......@@ -1106,7 +1137,10 @@ checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
checkCaseAlts e ty alts =
do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
-- See CoreSyn Note [Case expression invariants] item (2)
; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
-- See CoreSyn Note [Case expression invariants] item (3)
-- For types Int#, Word# with an infinite (well, large!) number of
-- possible values, there should usually be a DEFAULT case
......@@ -1136,6 +1170,7 @@ lintAltExpr :: CoreExpr -> OutType -> LintM ()
lintAltExpr expr ann_ty
= do { actual_ty <- lintCoreExpr expr
; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
-- See CoreSyn Note [Case expression invariants] item (6)
lintCoreAlt :: OutType -- Type of scrutinee
-> OutType -- Type of the alternative
......@@ -1246,7 +1281,8 @@ lintIdBndr top_lvl bind_site id linterF
; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
(mkNonTopExternalNameMsg id)
; (ty, k) <- lintInTy (idType id)
; (ty, k) <- addLoc (IdTy id) $
lintInTy (idType id)
-- See Note [Levity polymorphism invariants] in CoreSyn
; lintL (isJoinId id || not (isKindLevPoly k))
......@@ -2180,6 +2216,9 @@ data LintLocInfo
| BodyOfLetRec [Id] -- One of the binders
| CaseAlt CoreAlt -- Case alternative
| CasePat CoreAlt -- The *pattern* of the case alternative
| CaseTy CoreExpr -- The type field of a case expression
-- with this scrutinee
| IdTy Id -- The type field of an Id binder
| AnExpr CoreExpr -- Some expression
| ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
| TopLevelBindings
......@@ -2237,17 +2276,23 @@ addWarnL msg = LintM $ \ env (warns,errs) ->
addMsg :: LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
addMsg env msgs msg
= ASSERT( notNull locs )
= ASSERT( notNull loc_msgs )
msgs `snocBag` mk_msg msg
where
locs = le_loc env
(loc, cxt1) = dumpLoc (head locs)
cxts = [snd (dumpLoc loc) | loc <- locs]
context = ifPprDebug (vcat (reverse cxts) $$ cxt1 $$
text "Substitution:" <+> ppr (le_subst env))
cxt1
loc_msgs :: [(SrcLoc, SDoc)] -- Innermost first
loc_msgs = map dumpLoc (le_loc env)
cxt_doc = vcat $ reverse $ map snd loc_msgs
context = cxt_doc $$ whenPprDebug extra
extra = text "Substitution:" <+> ppr (le_subst env)
mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
msg_span = case [ span | (loc,_) <- loc_msgs
, let span = srcLocSpan loc
, isGoodSrcSpan span ] of
[] -> noSrcSpan
(s:_) -> s
mk_msg msg = mkLocMessage SevWarning msg_span
(msg $$ context)
addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc extra_loc m
......@@ -2345,7 +2390,8 @@ lintTyCoVarInScope :: TyCoVar -> LintM ()
lintTyCoVarInScope var
= do { subst <- getTCvSubst
; lintL (var `isInScope` subst)
(pprBndr LetBind var <+> text "is out of scope") }
(hang (text "The variable" <+> pprBndr LetBind var)
2 (text "is out of scope")) }
ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
-- check ty2 is subtype of ty1 (ie, has same structure but usage
......@@ -2375,19 +2421,19 @@ lintRole co r1 r2
dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
dumpLoc (RhsOf v)
= (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
= (getSrcLoc v, text "In the RHS of" <+> pp_binders [v])
dumpLoc (LambdaBodyOf b)
= (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
= (getSrcLoc b, text "In the body of lambda with binder" <+> pp_binder b)
dumpLoc (UnfoldingOf b)
= (getSrcLoc b, brackets (text "in the unfolding of" <+> pp_binder b))
= (getSrcLoc b, text "In the unfolding of" <+> pp_binder b)
dumpLoc (BodyOfLetRec [])
= (noSrcLoc, brackets (text "In body of a letrec with no binders"))
= (noSrcLoc, text "In body of a letrec with no binders")
dumpLoc (BodyOfLetRec bs@(_:_))
= ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
= ( getSrcLoc (head bs), text "In the body of letrec with binders" <+> pp_binders bs)
dumpLoc (AnExpr e)
= (noSrcLoc, text "In the expression:" <+> ppr e)
......@@ -2398,8 +2444,15 @@ dumpLoc (CaseAlt (con, args, _))
dumpLoc (CasePat (con, args, _))
= (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
dumpLoc (CaseTy scrut)
= (noSrcLoc, hang (text "In the result-type of a case with scrutinee:")
2 (ppr scrut))
dumpLoc (IdTy b)
= (getSrcLoc b, text "In the type of a binder:" <+> ppr b)
dumpLoc (ImportedUnfolding locn)
= (locn, brackets (text "in an imported unfolding"))
= (locn, text "In an imported unfolding")
dumpLoc TopLevelBindings
= (noSrcLoc, Outputable.empty)
dumpLoc (InType ty)
......
......@@ -1274,7 +1274,7 @@ wrapBinds :: Floats -> CpeBody -> CpeBody
wrapBinds (Floats _ binds) body
= foldrOL mk_bind body binds
where
mk_bind (FloatCase bndr rhs _) body = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
mk_bind (FloatCase bndr rhs _) body = mkDefaultCase rhs bndr body
mk_bind (FloatLet bind) body = Let bind body
mk_bind (FloatTick tickish) body = mkTick tickish body
......
......@@ -201,40 +201,7 @@ These data types are the heart of the compiler
-- The binder gets bound to the value of the scrutinee,
-- and the 'Type' must be that of all the case alternatives
--
-- #case_invariants#
-- This is one of the more complicated elements of the Core language,
-- and comes with a number of restrictions:
--
-- 1. The list of alternatives may be empty;
-- See Note [Empty case alternatives]
--
-- 2. The 'DEFAULT' case alternative must be first in the list,
-- if it occurs at all.
--
-- 3. The remaining cases are in order of increasing
-- tag (for 'DataAlts') or
-- lit (for 'LitAlts').
-- This makes finding the relevant constructor easy,
-- and makes comparison easier too.
--
-- 4. The list of alternatives must be exhaustive. An /exhaustive/ case
-- does not necessarily mention all constructors:
--
-- @
-- data Foo = Red | Green | Blue
-- ... case x of
-- Red -> True
-- other -> f (case x of
-- Green -> ...
-- Blue -> ... ) ...
-- @
--
-- The inner case does not need a @Red@ alternative, because @x@
-- can't be @Red@ at that program point.
--
-- 5. Floating-point values must not be scrutinised against literals.
-- See #9238 and Note [Rules for floating-point comparisons]
-- in PrelRules for rationale.
-- IMPORTANT: see Note [Case expression invariants]
--
-- * Cast an expression to a particular type.
-- This is used to implement @newtype@s (a @newtype@ constructor or
......@@ -247,6 +214,41 @@ These data types are the heart of the compiler
--
-- * A coercion
{- Note [Why does Case have a 'Type' field?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The obvious alternative is
exprType (Case scrut bndr alts)
| (_,_,rhs1):_ <- alts
= exprType rhs1
But caching the type in the Case constructor
exprType (Case scrut bndr ty alts) = ty
is better for at least three reasons:
* It works when there are no alternatives (see case invarant 1 above)
* It might be faster in deeply-nested situations.
* It might not be quite the same as (exprType rhs) for one
of the RHSs in alts. Consider a phantom type synonym
type S a = Int
and we want to form the case expression
case x of { K (a::*) -> (e :: S a) }
Then exprType of the RHS is (S a), but we cannot make that be
the 'ty' in the Case constructor because 'a' is simply not in
scope there. Instead we must expand the synonym to Int before
putting it in the Case constructor. See CoreUtils.mkSingleAltCase.
So we'd have to do synonym expansion in exprType which would
be inefficient.
* The type stored in the case is checked with lintInTy. This checks
(among other things) that it does not mention any variables that are
not in scope. If we did not have the type there, it would be a bit
harder for Core Lint to reject case blah of Ex x -> x where
data Ex = forall a. Ex a.
-}
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data Expr b
......@@ -255,7 +257,8 @@ data Expr b
| App (Expr b) (Arg b)
| Lam b (Expr b)
| Let (Bind b) (Expr b)
| Case (Expr b) b Type [Alt b] -- See #case_invariants#
| Case (Expr b) b Type [Alt b] -- See Note [Case expression invariants]
-- and Note [Why does Case have a 'Type' field?]
| Cast (Expr b) Coercion
| Tick (Tickish Id) (Expr b)
| Type Type
......@@ -448,6 +451,71 @@ coreSyn/MkCore.
For discussion of some implications of the let/app invariant primops see
Note [Checking versus non-checking primops] in PrimOp.
Note [Case expression invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Case expressions are one of the more complicated elements of the Core
language, and come with a number of invariants. All of them should be
checked by Core Lint.
1. The list of alternatives may be empty;
See Note [Empty case alternatives]
2. The 'DEFAULT' case alternative must be first in the list,
if it occurs at all. Checked in CoreLint.checkCaseAlts.
3. The remaining cases are in order of (strictly) increasing
tag (for 'DataAlts') or
lit (for 'LitAlts').
This makes finding the relevant constructor easy, and makes
comparison easier too. Checked in CoreLint.checkCaseAlts.
4. The list of alternatives must be exhaustive. An /exhaustive/ case
does not necessarily mention all constructors:
@
data Foo = Red | Green | Blue
... case x of
Red -> True
other -> f (case x of
Green -> ...
Blue -> ... ) ...
@
The inner case does not need a @Red@ alternative, because @x@
can't be @Red@ at that program point.
This is not checked by Core Lint -- it's very hard to do so.
E.g. suppose that inner case was floated out, thus:
let a = case x of
Green -> ...
Blue -> ... )
case x of
Red -> True
other -> f a
Now it's really hard to see that the Green/Blue case is
exhaustive. But it is.
If you have a case-expression that really /isn't/ exhaustive,
we may generate seg-faults. Consider the Green/Blue case
above. Since there are only two branches we may generate
code that tests for Green, and if not Green simply /assumes/
Blue (since, if the case is exhaustive, that's all that
remains). Of course, if it's not Blue and we start fetching
fields that should be in a Blue constructor, we may die
horribly. See also Note [Core Lint guarantee] in CoreLint.
5. Floating-point values must not be scrutinised against literals.
See #9238 and Note [Rules for floating-point comparisons]
in PrelRules for rationale. Checked in lintCaseExpr;
see the call to isFloatingTy.
6. The 'ty' field of (Case scrut bndr ty alts) is the type of the
/entire/ case expression. Checked in lintAltExpr.
See also Note [Why does Case have a 'Type' field?].
7. The type of the scrutinee must be the same as the type
of the case binder, obviously. Checked in lintCaseExpr.
Note [CoreSyn type and coercion invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We allow a /non-recursive/, /non-top-level/ let to bind type and
......@@ -1748,8 +1816,8 @@ ltAlt a1 a2 = (a1 `cmpAlt` a2) == LT
cmpAltCon :: AltCon -> AltCon -> Ordering
-- ^ Compares 'AltCon's within a single list of alternatives
-- DEFAULT comes out smallest, so that sorting by AltCon
-- puts alternatives in the order required by #case_invariants#
-- DEFAULT comes out smallest, so that sorting by AltCon puts
-- alternatives in the order required: see Note [Case expression invariants]
cmpAltCon DEFAULT DEFAULT = EQ
cmpAltCon DEFAULT _ = LT
......
......@@ -14,7 +14,7 @@ module CoreUtils (
mkCast,
mkTick, mkTicks, mkTickNoHNF, tickHNFArgs,
bindNonRec, needsCaseBinding,
mkAltExpr,
mkAltExpr, mkDefaultCase, mkSingleAltCase,
-- * Taking expressions apart
findDefault, addDefault, findAlt, isDefaultAlt,
......@@ -488,7 +488,7 @@ bindNonRec bndr rhs body
| needsCaseBinding (idType bndr) rhs = case_bind
| otherwise = let_bind
where
case_bind = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
case_bind = mkDefaultCase rhs bndr body
let_bind = Let (NonRec bndr rhs) body
-- | Tests whether we have to use a @case@ rather than @let@ binding for this expression
......@@ -512,8 +512,45 @@ mkAltExpr (LitAlt lit) [] []
mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt"
mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT"
{- Note [Binding coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
mkDefaultCase :: CoreExpr -> Id -> CoreExpr -> CoreExpr
-- Make (case x of y { DEFAULT -> e }
mkDefaultCase scrut case_bndr body
= Case scrut case_bndr (exprType body) [(DEFAULT, [], body)]
mkSingleAltCase :: CoreExpr -> Id -> AltCon -> [Var] -> CoreExpr -> CoreExpr
-- Use this function if possible, when building a case,
-- because it ensures that the type on the Case itself
-- doesn't mention variables bound by the case
-- See Note [Care with the type of a case expression]
mkSingleAltCase scrut case_bndr con bndrs body
= Case scrut case_bndr case_ty [(con,bndrs,body)]
where
body_ty = exprType body
case_ty -- See Note [Care with the type of a case expression]
| Just body_ty' <- occCheckExpand bndrs body_ty
= body_ty'
| otherwise
= pprPanic "mkSingleAltCase" (ppr scrut $$ ppr bndrs $$ ppr body_ty)
{- Note [Care with the type of a case expression]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a phantom type synonym
type S a = Int
and we want to form the case expression
case x of K (a::*) -> (e :: S a)
We must not make the type field of the case-expression (S a) because
'a' isn't in scope. Hence the call to occCheckExpand. This caused
issue #17056.
NB: this situation can only arise with type synonyms, which can
falsely "mention" type variables that aren't "really there", and which
can be eliminated by expanding the synonym.
Note [Binding coercions]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider binding a CoVar, c = e. Then, we must atisfy
Note [CoreSyn type and coercion invariant] in CoreSyn,
which allows only (Coercion co) on the RHS.
......
......@@ -7,6 +7,7 @@ module MkCore (
mkCoreApp, mkCoreApps, mkCoreConApps,
mkCoreLams, mkWildCase, mkIfThenElse,
mkWildValBinder, mkWildEvBinder,
mkSingleAltCase,
sortQuantVars, castBottomExpr,
-- * Constructing boxed literals
......@@ -57,7 +58,7 @@ import Id
import Var ( EvVar, setTyVarUnique )
import CoreSyn
import CoreUtils ( exprType, needsCaseBinding, bindNonRec )
import CoreUtils ( exprType, needsCaseBinding, mkSingleAltCase, bindNonRec )
import Literal
import HscTypes
......@@ -111,29 +112,34 @@ mkCoreLet (NonRec bndr rhs) body -- See Note [CoreSyn let/app invariant]
mkCoreLet bind body
= Let bind body
-- | Create a lambda where the given expression has a number of variables
-- bound over it. The leftmost binder is that bound by the outermost
-- lambda in the result
mkCoreLams :: [CoreBndr] -> CoreExpr -> CoreExpr
mkCoreLams = mkLams
-- | Bind a list of binding groups over an expression. The leftmost binding
-- group becomes the outermost group in the resulting expression
mkCoreLets :: [CoreBind] -> CoreExpr -> CoreExpr
mkCoreLets binds body = foldr mkCoreLet body binds
-- | Construct an expression which represents the application of one expression
-- paired with its type to an argument. The result is paired with its type. This
-- function is not exported and used in the definition of 'mkCoreApp' and
-- 'mkCoreApps'.
-- | Construct an expression which represents the application of a number of
-- expressions to that of a data constructor expression. The leftmost expression
-- in the list is applied first
mkCoreConApps :: DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps con args = mkCoreApps (Var (dataConWorkId con)) args
-- | Construct an expression which represents the application of a number of
-- expressions to another. The leftmost expression in the list is applied first
-- Respects the let/app invariant by building a case expression where necessary
-- See CoreSyn Note [CoreSyn let/app invariant]
mkCoreAppTyped :: SDoc -> (CoreExpr, Type) -> CoreExpr -> (CoreExpr, Type)
mkCoreAppTyped _ (fun, fun_ty) (Type ty)
= (App fun (Type ty), piResultTy fun_ty ty)
mkCoreAppTyped _ (fun, fun_ty) (Coercion co)
= (App fun (Coercion co), res_ty)
where
(_, res_ty) = splitFunTy fun_ty
mkCoreAppTyped d (fun, fun_ty) arg
= ASSERT2( isFunTy fun_ty, ppr fun $$ ppr arg $$ d )
(mk_val_app fun arg arg_ty res_ty, res_ty)
mkCoreApps :: CoreExpr -> [CoreExpr] -> CoreExpr
mkCoreApps fun args
= fst $
foldl' (mkCoreAppTyped doc_string) (fun, fun_ty) args
where
(arg_ty, res_ty) = splitFunTy fun_ty
doc_string = ppr fun_ty $$ ppr fun $$ ppr args
fun_ty = exprType fun
-- | Construct an expression which represents the application of one expression
-- to the other
......@@ -143,47 +149,40 @@ mkCoreApp :: SDoc -> CoreExpr -> CoreExpr -> CoreExpr
mkCoreApp s fun arg
= fst $ mkCoreAppTyped s (fun, exprType fun) arg
-- | Construct an expression which represents the application of a number of