Commit 6ad2b42f authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor free tyvars on LHS of rules

A RULE can have unbound meta-tyvars on the LHS.  Consider
  data T a = C

  foo :: T a -> Int
  foo C = 1

  {-# RULES "myrule"  foo C = 1 #-}

After type checking the LHS becomes (foo alpha (C alpah)) and we do
not want to zap the unbound meta-tyvar 'alpha' to Any, because that
limits the applicability of the rule.  Instead, we want to quantify
over it!

Previously there was a rather clunky implementation of this
quantification, buried in the zonker in TcHsSyn (zonkTvCollecting).

This patch refactors it so that the zonker just turns the meta-tyvar
into a skolem, and the desugarer adds the quantification.  See DsBinds
Note [Free tyvars on rule LHS]. As it happened, the desugarer was
already doing something similar for dictionaries. See DsBinds
Note [Free dictionaries on rule LHS]

No change in functionality, but less cruft.
parent 970ff585
......@@ -776,14 +776,14 @@ decomposeRuleLhs orig_bndrs orig_lhs
= Left (vcat (map dead_msg unbound))
| Just (fn_id, args) <- decompose fun2 args2
, let extra_dict_bndrs = mk_extra_dict_bndrs fn_id args
, let extra_bndrs = mk_extra_bndrs fn_id args
= -- pprTrace "decmposeRuleLhs" (vcat [ text "orig_bndrs:" <+> ppr orig_bndrs
-- , text "orig_lhs:" <+> ppr orig_lhs
-- , text "lhs1:" <+> ppr lhs1
-- , text "extra_dict_bndrs:" <+> ppr extra_dict_bndrs
-- , text "fn_id:" <+> ppr fn_id
-- , text "args:" <+> ppr args]) $
Right (orig_bndrs ++ extra_dict_bndrs, fn_id, args)
Right (orig_bndrs ++ extra_bndrs, fn_id, args)
| otherwise
= Left bad_shape_msg
......@@ -797,15 +797,19 @@ decomposeRuleLhs orig_bndrs orig_lhs
orig_bndr_set = mkVarSet orig_bndrs
-- Add extra dict binders: Note [Free dictionaries]
mk_extra_dict_bndrs fn_id args
= [ mkLocalId (localiseName (idName d)) (idType d)
| d <- exprsFreeVarsList args
, not (d `elemVarSet` orig_bndr_set)
, not (d == fn_id)
-- fn_id: do not quantify over the function itself, which may
-- itself be a dictionary (in pathological cases, Trac #10251)
, isDictId d ]
-- Add extra tyvar binders: Note [Free tyvars in rule LHS]
-- and extra dict binders: Note [Free dictionaries in rule LHS]
mk_extra_bndrs fn_id args
= toposortTyVars unbound_tvs ++ unbound_dicts
where
unbound_tvs = [ v | v <- unbound_vars, isTyVar v ]
unbound_dicts = [ mkLocalId (localiseName (idName d)) (idType d)
| d <- unbound_vars, isDictId d ]
unbound_vars = [ v | v <- exprsFreeVarsList args
, not (v `elemVarSet` orig_bndr_set)
, not (v == fn_id) ]
-- fn_id: do not quantify over the function itself, which may
-- itself be a dictionary (in pathological cases, Trac #10251)
decompose (Var fn_id) args
| not (fn_id `elemVarSet` orig_bndr_set)
......@@ -867,6 +871,54 @@ There are several things going on here.
* simpleOptExpr: see Note [Simplify rule LHS]
* extra_dict_bndrs: see Note [Free dictionaries]
Note [Free tyvars on rule LHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data T a = C
foo :: T a -> Int
foo C = 1
{-# RULES "myrule" foo C = 1 #-}
After type checking the LHS becomes (foo alpha (C alpha)), where alpha
is an unbound meta-tyvar. The zonker in TcHsSyn is careful not to
turn the free alpha into Any (as it usually does). Instead it turns it
into a skolem 'a'. See TcHsSyn Note [Zonking the LHS of a RULE].
Now we must quantify over that 'a'. It's /really/ inconvenient to do that
in the zonker, because the HsExpr data type is very large. But it's /easy/
to do it here in the desugarer.
Moreover, we have to do something rather similar for dictionaries;
see Note [Free dictionaries on rule LHS]. So that's why we look for
type variables free on the LHS, and quantify over them.
Note [Free dictionaries on rule LHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the LHS of a specialisation rule, (/\as\ds. f es) has a free dict,
which is presumably in scope at the function definition site, we can quantify
over it too. *Any* dict with that type will do.
So for example when you have
f :: Eq a => a -> a
f = <rhs>
... SPECIALISE f :: Int -> Int ...
Then we get the SpecPrag
SpecPrag (f Int dInt)
And from that we want the rule
RULE forall dInt. f Int dInt = f_spec
f_spec = let f = <rhs> in f Int dInt
But be careful! That dInt might be GHC.Base.$fOrdInt, which is an External
Name, and you can't bind them in a lambda or forall without getting things
confused. Likewise it might have an InlineRule or something, which would be
utterly bogus. So we really make a fresh Id, with the same unique and type
as the old one, but with an Internal name and no IdInfo.
Note [Drop dictionary bindings on rule LHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
drop_dicts drops dictionary bindings on the LHS where possible.
......@@ -966,31 +1018,6 @@ the constraint is unused. We could bind 'd' to (error "unused")
but it seems better to reject the program because it's almost certainly
a mistake. That's what the isDeadBinder call detects.
Note [Free dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~
When the LHS of a specialisation rule, (/\as\ds. f es) has a free dict,
which is presumably in scope at the function definition site, we can quantify
over it too. *Any* dict with that type will do.
So for example when you have
f :: Eq a => a -> a
f = <rhs>
... SPECIALISE f :: Int -> Int ...
Then we get the SpecPrag
SpecPrag (f Int dInt)
And from that we want the rule
RULE forall dInt. f Int dInt = f_spec
f_spec = let f = <rhs> in f Int dInt
But be careful! That dInt might be GHC.Base.$fOrdInt, which is an External
Name, and you can't bind them in a lambda or forall without getting things
confused. Likewise it might have an InlineRule or something, which would be
utterly bogus. So we really make a fresh Id, with the same unique and type
as the old one, but with an Internal name and no IdInfo.
************************************************************************
* *
Desugaring evidence
......
......@@ -65,7 +65,6 @@ import SrcLoc
import Bag
import Outputable
import Util
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Data.List ( partition )
......@@ -189,14 +188,18 @@ type UnboundTyVarZonker = TcTyVar -> TcM Type
-- | A ZonkEnv carries around several bits.
-- The UnboundTyVarZonker just zaps unbouned meta-tyvars to Any (as
-- defined in zonkTypeZapping), except on the LHS of rules. See
-- Note [Zonking the LHS of a RULE]. The (TyCoVarEnv TyVar) and is just
-- an optimisation: when binding a tyvar or covar, we zonk the kind right away
-- and add a mapping to the env. This prevents re-zonking the kind at
-- every occurrence. But this is *just* an optimisation.
-- The final (IdEnv Var) optimises zonking for
-- Ids. It is knot-tied. We must be careful never to put coercion variables
-- (which are Ids, after all) in the knot-tied env, because coercions can
-- appear in types, and we sometimes inspect a zonked type in this module.
-- Note [Zonking the LHS of a RULE].
--
-- The (TyCoVarEnv TyVar) and is just an optimisation: when binding a
-- tyvar or covar, we zonk the kind right away and add a mapping to
-- the env. This prevents re-zonking the kind at every occurrence. But
-- this is *just* an optimisation.
--
-- The final (IdEnv Var) optimises zonking for Ids. It is
-- knot-tied. We must be careful never to put coercion variables
-- (which are Ids, after all) in the knot-tied env, because coercions
-- can appear in types, and we sometimes inspect a zonked type in this
-- module.
--
-- Confused by zonking? See Note [What is zonking?] in TcMType.
data ZonkEnv
......@@ -1316,25 +1319,15 @@ zonkRules env rs = mapM (wrapLocM (zonkRule env)) rs
zonkRule :: ZonkEnv -> RuleDecl TcId -> TcM (RuleDecl Id)
zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
= do { unbound_tkv_set <- newMutVar emptyVarSet
; let kind_var_set = identify_kind_vars vars
env_rule = setZonkType env (zonkTvCollecting kind_var_set unbound_tkv_set)
-- See Note [Zonking the LHS of a RULE]
= do { (env_inside, new_bndrs) <- mapAccumLM zonk_bndr env vars
; (env_inside, new_bndrs) <- mapAccumLM zonk_bndr env_rule vars
; let env_lhs = setZonkType env_inside zonkTvSkolemising
-- See Note [Zonking the LHS of a RULE]
; new_lhs <- zonkLExpr env_inside lhs
; new_lhs <- zonkLExpr env_lhs lhs
; new_rhs <- zonkLExpr env_inside rhs
; unbound_tkvs <- readMutVar unbound_tkv_set
; let final_bndrs :: [LRuleBndr Var]
final_bndrs = map (noLoc . RuleBndr . noLoc)
(varSetElemsWellScoped unbound_tkvs)
++ new_bndrs
; return $
HsRule name act final_bndrs new_lhs fv_lhs new_rhs fv_rhs }
; return (HsRule name act new_bndrs new_lhs fv_lhs new_rhs fv_rhs) }
where
zonk_bndr env (L l (RuleBndr (L loc v)))
= do { (env', v') <- zonk_it env v
......@@ -1350,18 +1343,6 @@ zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
-- wrong because we may need to go inside the kind
-- of v and zonk there!
-- returns the set of type variables mentioned in the kind of another
-- type. This is used only when -XPolyKinds is not set.
identify_kind_vars :: [LRuleBndr TcId] -> TyVarSet
identify_kind_vars rule_bndrs
= let vars = map strip_rulebndr rule_bndrs in
unionVarSets (map (\v -> if isTyVar v
then tyCoVarsOfType (tyVarKind v)
else emptyVarSet) vars)
strip_rulebndr (L _ (RuleBndr (L _ v))) = v
strip_rulebndr (L _ (RuleBndrSig {})) = panic "strip_rulebndr zonkRule"
zonkVects :: ZonkEnv -> [LVectDecl TcId] -> TcM [LVectDecl Id]
zonkVects env = mapM (wrapLocM (zonkVect env))
......@@ -1485,31 +1466,6 @@ zonkEvBind env bind@(EvBind { eb_lhs = var, eb_rhs = term })
* *
************************************************************************
Note [Zonking the LHS of a RULE]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to gather the type variables mentioned on the LHS so we can
quantify over them. Example:
data T a = C
foo :: T a -> Int
foo C = 1
{-# RULES "myrule" foo C = 1 #-}
After type checking the LHS becomes (foo a (C a))
and we do not want to zap the unbound tyvar 'a' to (), because
that limits the applicability of the rule. Instead, we
want to quantify over it!
It's easiest to get zonkTvCollecting to gather the free tyvars
here. Attempts to do so earlier are tiresome, because (a) the data
type is big and (b) finding the free type vars of an expression is
necessarily monadic operation. (consider /\a -> f @ b, where b is
side-effected to a)
And that in turn is why ZonkEnv carries the function to use for
type variables!
Note [Zonking mutable unbound type or kind variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In zonkTypeZapping, we zonk mutable but unbound type or kind variables to an
......@@ -1630,23 +1586,17 @@ zonkTcKindToKind binders res_kind
zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
zonkCoToCo = mapCoercion zonk_tycomapper
zonkTvCollecting :: TyVarSet -> TcRef TyVarSet -> UnboundTyVarZonker
-- This variant collects unbound type variables in a mutable variable
-- Works on both types and kinds
zonkTvCollecting kind_vars unbound_tv_set tv
= do { poly_kinds <- xoptM LangExt.PolyKinds
; let default_kind = tv `elemVarSet` kind_vars && not poly_kinds
; ty_or_tv <- zonkQuantifiedTyVarOrType default_kind tv
; case ty_or_tv of
Right ty -> return ty
Left tv' -> do
{ tv_set <- readMutVar unbound_tv_set
; writeMutVar unbound_tv_set (extendVarSet tv_set tv')
; return (mkTyVarTy tv') } }
zonkTvSkolemising :: UnboundTyVarZonker
-- This variant is used for the LHS of rules
-- See Note [Zonking the LHS of a RULE].
zonkTvSkolemising tv
= do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv
; return (mkTyVarTy tv') }
zonkTypeZapping :: UnboundTyVarZonker
-- This variant is used for everything except the LHS of rules
-- It zaps unbound type variables to (), or some other arbitrary type
-- It zaps unbound type variables to Any, except for RuntimeRep
-- vars which it zonks to PtrRepLIfted
-- Works on both types and kinds
zonkTypeZapping tv
= do { let ty | isRuntimeRepVar tv = ptrRepLiftedTy
......@@ -1655,7 +1605,37 @@ zonkTypeZapping tv
; return ty }
---------------------------------------
{-
{- Note [Zonking the LHS of a RULE]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See also DsBinds Note [Free tyvars on rule LHS]
We need to gather the type variables mentioned on the LHS so we can
quantify over them. Example:
data T a = C
foo :: T a -> Int
foo C = 1
{-# RULES "myrule" foo C = 1 #-}
After type checking the LHS becomes (foo alpha (C alpah)) and we do
not want to zap the unbound meta-tyvar 'alpha' to Any, because that
limits the applicability of the rule. Instead, we want to quantify
over it!
We do this in two stages.
* During zonking, we skolemise 'alpha' to 'a'. We do this by using
zonkTvSkolemising as the UnboundTyVarZonker in the ZonkEnv.
(This is the whole reason that the ZonkEnv has a UnboundTyVarZonker.)
* In DsBinds, we quantify over it. See DsBinds
Note [Free tyvars on rule LHS]
Quantifying here is awkward because (a) the data type is big and (b)
finding the free type vars of an expression is necessarily monadic
operation. (consider /\a -> f @ b, where b is side-effected to a)
Note [Unboxed tuples in representation polymorphism check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Recall that all types that have values (that is, lifted and unlifted
......
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