Commit 016a0bd1 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix two cloning-related bugs

Crikey!  Not just one but two bugs in type variable cloning,
both dating from the days before PolyKinds.  Both were shown up
by Trac #11330.

1. In SetLevels, when floating a case expression we must clone its
   binders, *and* do so in a telescope-aware way, because the
   constructor may bind a kind variable that appears in the kind
   of a type variable.

   Instead of doing this (wrongly) by steam, call CoreSubst.cloneBndrs.

   I added Notes and did other refactoring at the same time.

2. It turned out that CoreSubst.cloneBndrs calls TyCoRep.cloneTyVarBndr,
   and that too was bogus!  It didn't substitute in the kind of the
   TyVar being cloned.  There was even a comment to say "variables can't
   appear in kinds".  Thta hasn't been true for a long time now.

Easily fixed.

Interestingly, I then found that test
   dependent/should_compile/KindEqualities
was emitting a new inexhaustive-pattern-match warning.  Sure enough
it was valid!  So the lack of cloning in cloneTyVarBndr really was
causing an observable bug; just one that we had not observed.
parent 1c6d70c2
......@@ -13,10 +13,15 @@
2. We also let-ify many expressions (notably case scrutinees), so they
will have a fighting chance of being floated sensible.
3. We clone the binders of any floatable let-binding, so that when it is
floated out it will be unique. (This used to be done by the simplifier
but the latter now only ensures that there's no shadowing; indeed, even
that may not be true.)
3. Note [Need for cloning during float-out]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We clone the binders of any floatable let-binding, so that when it is
floated out it will be unique. Example
(let x=2 in x) + (let x=3 in x)
we must clone before floating so we get
let x1=2 in
let x2=3 in
x1+x2
NOTE: this can't be done using the uniqAway idea, because the variable
must be unique in the whole program, not just its current scope,
......@@ -29,7 +34,9 @@
We do *not* clone top-level bindings, because some of them must not change,
but we *do* clone bindings that are heading for the top level
4. In the expression
4. Note [Binder-swap during float-out]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the expression
case x of wild { p -> ...wild... }
we substitute x for wild in the RHS of the case alternatives:
case x of wild { p -> ...x... }
......@@ -373,10 +380,8 @@ lvlCase env scrut_fvs scrut' case_bndr ty alts
= -- See Note [Floating cases]
-- Always float the case if possible
-- Unlike lets we don't insist that it escapes a value lambda
do { (rhs_env, (case_bndr':bs')) <- cloneVars NonRecursive env dest_lvl (case_bndr:bs)
-- We don't need to use extendCaseBndrLvlEnv here
-- because we are floating the case outwards so
-- no need to do the binder-swap thing
do { (env1, (case_bndr' : bs')) <- cloneCaseBndrs env dest_lvl (case_bndr : bs)
; let rhs_env = extendCaseBndrEnv env1 case_bndr scrut'
; body' <- lvlMFE True rhs_env body
; let alt' = (con, [TB b (StayPut dest_lvl) | b <- bs'], body')
; return (Case scrut' (TB case_bndr' (FloatMe dest_lvl)) ty [alt']) }
......@@ -387,15 +392,15 @@ lvlCase env scrut_fvs scrut' case_bndr ty alts
; alts' <- mapM (lvl_alt alts_env) alts
; return (Case scrut' case_bndr' ty alts') }
where
incd_lvl = incMinorLvl (le_ctxt_lvl env)
dest_lvl = maxFvLevel (const True) env scrut_fvs
-- Don't abstact over type variables, hence const True
incd_lvl = incMinorLvl (le_ctxt_lvl env)
dest_lvl = maxFvLevel (const True) env scrut_fvs
-- Don't abstact over type variables, hence const True
lvl_alt alts_env (con, bs, rhs)
= do { rhs' <- lvlMFE True new_env rhs
; return (con, bs', rhs') }
where
(new_env, bs') = substAndLvlBndrs NonRecursive alts_env incd_lvl bs
lvl_alt alts_env (con, bs, rhs)
= do { rhs' <- lvlMFE True new_env rhs
; return (con, bs', rhs') }
where
(new_env, bs') = substAndLvlBndrs NonRecursive alts_env incd_lvl bs
{-
Note [Floating cases]
......@@ -708,7 +713,7 @@ lvlBind env (AnnNonRec bndr rhs)
| null abs_vars
= do { -- No type abstraction; clone existing binder
rhs' <- lvlExpr (setCtxtLvl env dest_lvl) rhs
; (env', [bndr']) <- cloneVars NonRecursive env dest_lvl [bndr]
; (env', [bndr']) <- cloneLetVars NonRecursive env dest_lvl [bndr]
; return (NonRec (TB bndr' (FloatMe dest_lvl)) rhs', env') }
| otherwise
......@@ -732,7 +737,7 @@ lvlBind env (AnnRec pairs)
; return (Rec (bndrs' `zip` rhss'), env') }
| null abs_vars
= do { (new_env, new_bndrs) <- cloneVars Recursive env dest_lvl bndrs
= do { (new_env, new_bndrs) <- cloneLetVars Recursive env dest_lvl bndrs
; new_rhss <- mapM (lvlExpr (setCtxtLvl new_env dest_lvl)) rhss
; return ( Rec ([TB b (FloatMe dest_lvl) | b <- new_bndrs] `zip` new_rhss)
, new_env) }
......@@ -754,7 +759,7 @@ lvlBind env (AnnRec pairs)
let (rhs_env, abs_vars_w_lvls) = lvlLamBndrs env dest_lvl abs_vars
rhs_lvl = le_ctxt_lvl rhs_env
(rhs_env', [new_bndr]) <- cloneVars Recursive rhs_env rhs_lvl [bndr]
(rhs_env', [new_bndr]) <- cloneLetVars Recursive rhs_env rhs_lvl [bndr]
let
(lam_bndrs, rhs_body) = collectAnnBndrs rhs
(body_env1, lam_bndrs1) = substBndrsSL NonRecursive rhs_env' lam_bndrs
......@@ -856,11 +861,10 @@ lvlBndrs :: LevelEnv -> Level -> [CoreBndr] -> (LevelEnv, [LevelledBndr])
-- all or none. We never separate binders.
lvlBndrs env@(LE { le_lvl_env = lvl_env }) new_lvl bndrs
= ( env { le_ctxt_lvl = new_lvl
, le_lvl_env = foldl add_lvl lvl_env bndrs }
, le_lvl_env = addLvls new_lvl lvl_env bndrs }
, lvld_bndrs)
where
lvld_bndrs = [TB bndr (StayPut new_lvl) | bndr <- bndrs]
add_lvl env v = extendVarEnv env v new_lvl
-- Destination level is the max Id level of the expression
-- (We'll abstract the type variables, if any.)
......@@ -960,6 +964,12 @@ initialEnv float_lams
, le_subst = emptySubst
, le_env = emptyVarEnv }
addLvl :: Level -> VarEnv Level -> OutVar -> VarEnv Level
addLvl dest_lvl env v' = extendVarEnv env v' dest_lvl
addLvls :: Level -> VarEnv Level -> [OutVar] -> VarEnv Level
addLvls dest_lvl env vs = foldl (addLvl dest_lvl) env vs
floatLams :: LevelEnv -> Maybe Int
floatLams le = floatOutLambdas (le_switches le)
......@@ -972,8 +982,8 @@ floatOverSat le = floatOutOverSatApps (le_switches le)
setCtxtLvl :: LevelEnv -> Level -> LevelEnv
setCtxtLvl env lvl = env { le_ctxt_lvl = lvl }
-- extendCaseBndrLvlEnv adds the mapping case-bndr->scrut-var if it can
-- (see point 4 of the module overview comment)
-- extendCaseBndrEnv adds the mapping case-bndr->scrut-var if it can
-- See Note [Binder-swap during float-out]
extendCaseBndrEnv :: LevelEnv
-> Id -- Pre-cloned case binder
-> Expr LevelledBndr -- Post-cloned scrutinee
......@@ -1061,12 +1071,11 @@ newPolyBndrs dest_lvl
do { uniqs <- getUniquesM
; let new_bndrs = zipWith mk_poly_bndr bndrs uniqs
bndr_prs = bndrs `zip` new_bndrs
env' = env { le_lvl_env = foldl add_lvl lvl_env new_bndrs
env' = env { le_lvl_env = addLvls dest_lvl lvl_env new_bndrs
, le_subst = foldl add_subst subst bndr_prs
, le_env = foldl add_id id_env bndr_prs }
; return (env', new_bndrs) }
where
add_lvl env v' = extendVarEnv env v' dest_lvl
add_subst env (v, v') = extendIdSubst env v (mkVarApps (Var v') abs_vars)
add_id env (v, v') = extendVarEnv env v ((v':abs_vars), mkVarApps (Var v') abs_vars)
......@@ -1091,11 +1100,24 @@ newLvlVar lvld_rhs is_bot
rhs_ty = exprType de_tagged_rhs
mk_name uniq = mkSystemVarName uniq (mkFastString "lvl")
cloneVars :: RecFlag -> LevelEnv -> Level -> [Var] -> LvlM (LevelEnv, [Var])
-- Works for Ids, TyVars and CoVars
cloneCaseBndrs :: LevelEnv -> Level -> [Var] -> LvlM (LevelEnv, [Var])
cloneCaseBndrs env@(LE { le_subst = subst, le_lvl_env = lvl_env, le_env = id_env })
new_lvl vs
= do { us <- getUniqueSupplyM
; let (subst', vs') = cloneBndrs subst us vs
env' = env { le_ctxt_lvl = new_lvl
, le_lvl_env = addLvls new_lvl lvl_env vs'
, le_subst = subst'
, le_env = foldl add_id id_env (vs `zip` vs') }
; return (env', vs') }
cloneLetVars :: RecFlag -> LevelEnv -> Level -> [Var] -> LvlM (LevelEnv, [Var])
-- See Note [Need for cloning during float-out]
-- Works for Ids bound by let(rec)
-- The dest_lvl is attributed to the binders in the new env,
-- but cloneVars doesn't affect the ctxt_lvl of the incoming env
cloneVars is_rec
cloneLetVars is_rec
env@(LE { le_subst = subst, le_lvl_env = lvl_env, le_env = id_env })
dest_lvl vs
= do { us <- getUniqueSupplyM
......@@ -1104,13 +1126,11 @@ cloneVars is_rec
Recursive -> cloneRecIdBndrs subst us vs
vs2 = map zap_demand_info vs1 -- See Note [Zapping the demand info]
prs = vs `zip` vs2
env' = env { le_lvl_env = foldl add_lvl lvl_env vs2
env' = env { le_lvl_env = addLvls dest_lvl lvl_env vs2
, le_subst = subst'
, le_env = foldl add_id id_env prs }
; return (env', vs2) }
where
add_lvl env v_cloned = extendVarEnv env v_cloned dest_lvl
add_id :: IdEnv ([Var], LevelledExpr) -> (Var, Var) -> IdEnv ([Var], LevelledExpr)
add_id id_env (v, v1)
......
......@@ -2049,7 +2049,8 @@ substTyVarBndrCallback subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
-- Here we must simply zap the substitution for x
new_var | no_kind_change = uniqAway in_scope old_var
| otherwise = uniqAway in_scope $ updateTyVarKind (subst_fn subst) old_var
| otherwise = uniqAway in_scope $
setTyVarKind old_var (subst_fn subst old_ki)
-- The uniqAway part makes sure the new variable is not already in scope
substCoVarBndr :: TCvSubst -> CoVar -> (TCvSubst, CoVar)
......@@ -2083,16 +2084,18 @@ substCoVarBndrCallback sym subst_fun subst@(TCvSubst in_scope tenv cenv) old_var
-- because they can have free type variables
cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
cloneTyVarBndr (TCvSubst in_scope tv_env cv_env) tv uniq
| isTyVar tv
= (TCvSubst (extendInScopeSet in_scope tv')
cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq
= ASSERT2( isTyVar tv, ppr tv ) -- I think it's only called on TyVars
(TCvSubst (extendInScopeSet in_scope tv')
(extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv')
| otherwise
= (TCvSubst (extendInScopeSet in_scope tv')
tv_env (extendVarEnv cv_env tv (mkCoVarCo tv')), tv')
where
tv' = setVarUnique tv uniq -- Simply set the unique; the kind
-- has no type variables to worry about
old_ki = tyVarKind tv
no_kind_change = isEmptyVarSet (tyCoVarsOfType old_ki) -- verify that kind is closed
tv1 | no_kind_change = tv
| otherwise = setTyVarKind tv (substTy subst old_ki)
tv' = setVarUnique tv1 uniq
cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
cloneTyVarBndrs subst [] _usupply = (subst, [])
......
KindEqualities.hs:23:1: warning:
Pattern match(es) are non-exhaustive
In an equation for ‘zero’:
Patterns not matched: (TyApp (TyApp _ _) _)
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