TcRules.hs 15.9 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1993-1998

5 6

TcRules: Typechecking transformation rules
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE ViewPatterns #-}
10
{-# LANGUAGE TypeFamilies #-}
11

12
module TcRules ( tcRules ) where
13

14 15
import GhcPrelude

16
import HsSyn
17
import TcRnTypes
18
import TcRnMonad
19 20 21 22 23 24
import TcSimplify
import TcMType
import TcType
import TcHsType
import TcExpr
import TcEnv
25
import TcUnify( buildImplicationFor )
26
import TcEvidence( mkTcCoVarCo )
27
import Type
28
import TyCon( isTypeFamilyTyCon )
29
import Id
30
import Var( EvVar )
31
import VarSet
32
import BasicTypes       ( RuleName )
33
import SrcLoc
34
import Outputable
35
import FastString
36
import Bag
37
import Data.List( partition )
38

Austin Seipp's avatar
Austin Seipp committed
39
{-
40 41
Note [Typechecking rules]
~~~~~~~~~~~~~~~~~~~~~~~~~
42
We *infer* the typ of the LHS, and use that type to *check* the type of
43 44 45 46 47 48 49 50 51 52 53 54
the RHS.  That means that higher-rank rules work reasonably well. Here's
an example (test simplCore/should_compile/rule2.hs) produced by Roman:

   foo :: (forall m. m a -> m b) -> m a -> m b
   foo f = ...

   bar :: (forall m. m a -> m a) -> m a -> m a
   bar f = ...

   {-# RULES "foo/bar" foo = bar #-}

He wanted the rule to typecheck.
Austin Seipp's avatar
Austin Seipp committed
55
-}
56

57
tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTcId]
Alan Zimmerman's avatar
Alan Zimmerman committed
58 59
tcRules decls = mapM (wrapLocM tcRuleDecls) decls

60
tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTcId)
Alan Zimmerman's avatar
Alan Zimmerman committed
61 62 63
tcRuleDecls (HsRules src decls)
   = do { tc_decls <- mapM (wrapLocM tcRule) decls
        ; return (HsRules src tc_decls) }
64

65
tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTcId)
66
tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
67
  = addErrCtxt (ruleCtxt $ snd $ unLoc name)  $
68
    do { traceTc "---- Rule ------" (pprFullRuleName name)
69

70
        -- Note [Typechecking rules]
71 72 73 74 75 76 77
       ; (vars, bndr_wanted) <- captureConstraints $
                                tcRuleBndrs hs_bndrs
              -- bndr_wanted constraints can include wildcard hole
              -- constraints, which we should not forget about.
              -- It may mention the skolem type variables bound by
              -- the RULE.  c.f. Trac #10072

78
       ; let (id_bndrs, tv_bndrs) = partition isId vars
79
       ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
80 81
            <- tcExtendTyVarEnv tv_bndrs $
               tcExtendIdEnv    id_bndrs $
82 83
               do { -- See Note [Solve order for RULES]
                    ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
84 85
                  ; (rhs', rhs_wanted) <- captureConstraints $
                                          tcMonoExpr rhs (mkCheckExpType rule_ty)
86
                  ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
87

88 89 90 91
       ; traceTc "tcRule 1" (vcat [ pprFullRuleName name
                                  , ppr lhs_wanted
                                  , ppr rhs_wanted ])
       ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
       ; (lhs_evs, residual_lhs_wanted) <- simplifyRule (snd $ unLoc name)
                                              all_lhs_wanted
                                              rhs_wanted

       -- SimplfyRule Plan, step 4
       -- Now figure out what to quantify over
       -- c.f. TcSimplify.simplifyInfer
       -- We quantify over any tyvars free in *either* the rule
       --  *or* the bound variables.  The latter is important.  Consider
       --      ss (x,(y,z)) = (x,z)
       --      RULE:  forall v. fst (ss v) = fst v
       -- The type of the rhs of the rule is just a, but v::(a,(b,c))
       --
       -- We also need to get the completely-uconstrained tyvars of
       -- the LHS, lest they otherwise get defaulted to Any; but we do that
       -- during zonking (see TcHsSyn.zonkRule)

       ; let tpl_ids = lhs_evs ++ id_bndrs
110 111
       ; forall_tkvs <- zonkTcTypesAndSplitDepVars $
                        rule_ty : map idType tpl_ids
112
       ; gbls  <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
113
                                      -- monomorphic bindings from the MR; test tc111
114
       ; qtkvs <- quantifyTyVars gbls forall_tkvs
115 116
       ; traceTc "tcRule" (vcat [ pprFullRuleName name
                                , ppr forall_tkvs
117
                                , ppr qtkvs
118
                                , ppr rule_ty
119
                                , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
120 121
                  ])

122 123 124 125 126 127 128 129
       -- SimplfyRule Plan, step 5
       -- Simplify the LHS and RHS constraints:
       -- For the LHS constraints we must solve the remaining constraints
       -- (a) so that we report insoluble ones
       -- (b) so that we bind any soluble ones
       ; let skol_info = RuleSkol (snd (unLoc name))
       ; (lhs_implic, lhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
                                         lhs_evs residual_lhs_wanted
130 131
       ; (rhs_implic, rhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
                                         lhs_evs rhs_wanted
132

133
       ; emitImplications (lhs_implic `unionBags` rhs_implic)
134
       ; return (HsRule name act
135
                    (map (noLoc . RuleBndr . noLoc) (qtkvs ++ tpl_ids))
136 137
                    (mkHsDictLet lhs_binds lhs') fv_lhs
                    (mkHsDictLet rhs_binds rhs') fv_rhs) }
138

139
tcRuleBndrs :: [LRuleBndr GhcRn] -> TcM [Var]
140
tcRuleBndrs []
141
  = return []
142
tcRuleBndrs (L _ (RuleBndr (L _ name)) : rule_bndrs)
143
  = do  { ty <- newOpenFlexiTyVarTy
144
        ; vars <- tcRuleBndrs rule_bndrs
145
        ; return (mkLocalId name ty : vars) }
146
tcRuleBndrs (L _ (RuleBndrSig (L _ name) rn_ty) : rule_bndrs)
147
--  e.g         x :: a->a
148
--  The tyvar 'a' is brought into scope first, just as if you'd written
149 150
--              a::*, x :: a->a
  = do  { let ctxt = RuleSigCtxt name
151
        ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt rn_ty
152
        ; let id  = mkLocalIdOrCoVar name id_ty
153
                    -- See Note [Pattern signature binders] in TcHsType
154

155
              -- The type variables scope over subsequent bindings; yuk
156
        ; vars <- tcExtendTyVarEnv2 tvs $
157
                  tcRuleBndrs rule_bndrs
158
        ; return (map snd tvs ++ id : vars) }
159

Ian Lynagh's avatar
Ian Lynagh committed
160
ruleCtxt :: FastString -> SDoc
161
ruleCtxt name = text "When checking the transformation rule" <+>
162
                doubleQuotes (ftext name)
163 164 165 166 167 168 169 170 171


{-
*********************************************************************************
*                                                                                 *
              Constraint simplification for rules
*                                                                                 *
***********************************************************************************

172 173
Note [The SimplifyRule Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
Example.  Consider the following left-hand side of a rule
        f (x == y) (y > z) = ...
If we typecheck this expression we get constraints
        d1 :: Ord a, d2 :: Eq a
We do NOT want to "simplify" to the LHS
        forall x::a, y::a, z::a, d1::Ord a.
          f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
Instead we want
        forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
          f ((==) d2 x y) ((>) d1 y z) = ...

Here is another example:
        fromIntegral :: (Integral a, Num b) => a -> b
        {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
        forall dIntegralInt.
           fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
because the scsel will mess up RULE matching.  Instead we want
        forall dIntegralInt, dNumInt.
          fromIntegral Int Int dIntegralInt dNumInt = id Int

Even if we have
        g (x == y) (y == z) = ..
where the two dictionaries are *identical*, we do NOT WANT
        forall x::a, y::a, z::a, d1::Eq a
          f ((==) d1 x y) ((>) d1 y z) = ...
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.

In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.

Also note that we can't solve the LHS constraints in isolation:
Example   foo :: Ord a => a -> a
          foo_spec :: Int -> Int
          {-# RULE "foo"  foo = foo_spec #-}
Here, it's the RHS that fixes the type variable

HOWEVER, under a nested implication things are different
Consider
  f :: (forall a. Eq a => a->a) -> Bool -> ...
  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
       f b True = ...
    #-}
Here we *must* solve the wanted (Eq a) from the given (Eq a)
Gabor Greif's avatar
Gabor Greif committed
220
resulting from skolemising the argument type of g.  So we
221 222 223
revert to SimplCheck when going under an implication.


224
--------- So the SimplifyRule Plan is this -----------------------
225

226 227
* Step 0: typecheck the LHS and RHS to get constraints from each

228 229 230
* Step 1: Simplify the LHS and RHS constraints all together in one bag
          We do this to discover all unification equalities

231 232 233 234 235
* Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
          advantage of those unifications

* Setp 3: Partition the LHS constraints into the ones we will
          quantify over, and the others.
236
          See Note [RULE quantification over equalities]
237

238
* Step 4: Decide on the type variables to quantify over
239

240
* Step 5: Simplify the LHS and RHS constraints separately, using the
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
          quantified constraints as givens

Note [Solve order for RULES]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In step 1 above, we need to be a bit careful about solve order.
Consider
   f :: Int -> T Int
   type instance T Int = Bool

   RULE f 3 = True

From the RULE we get
   lhs-constraints:  T Int ~ alpha
   rhs-constraints:  Bool ~ alpha
where 'alpha' is the type that connects the two.  If we glom them
256
all together, and solve the RHS constraint first, we might solve
257 258
with alpha := Bool.  But then we'd end up with a RULE like

259
    RULE: f 3 |> (co :: T Int ~ Bool) = True
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282

which is terrible.  We want

    RULE: f 3 = True |> (sym co :: Bool ~ T Int)

So we are careful to solve the LHS constraints first, and *then* the
RHS constraints.  Actually much of this is done by the on-the-fly
constraint solving, so the same order must be observed in
tcRule.


Note [RULE quantification over equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Deciding which equalities to quantify over is tricky:
 * We do not want to quantify over insoluble equalities (Int ~ Bool)
    (a) because we prefer to report a LHS type error
    (b) because if such things end up in 'givens' we get a bogus
        "inaccessible code" error

 * But we do want to quantify over things like (a ~ F b), where
   F is a type function.

The difficulty is that it's hard to tell what is insoluble!
Simon Peyton Jones's avatar
Simon Peyton Jones committed
283
So we see whether the simplification step yielded any type errors,
284
and if so refrain from quantifying over *any* equalities.
285 286 287 288 289 290 291 292

Note [Quantifying over coercion holes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality constraints from the LHS will emit coercion hole Wanteds.
These don't have a name, so we can't quantify over them directly.
Instead, because we really do want to quantify here, invent a new
EvVar for the coercion, fill the hole with the invented EvVar, and
then quantify over the EvVar. Not too tricky -- just some
Gabor Greif's avatar
Gabor Greif committed
293
impedance matching, really.
294

295
Note [Simplify cloned constraints]
296 297 298
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this stage, we're simplifying constraints only for insolubility
and for unification. Note that all the evidence is quickly discarded.
299
We use a clone of the real constraint. If we don't do this,
300 301
then RHS coercion-hole constraints get filled in, only to get filled
in *again* when solving the implications emitted from tcRule. That's
302
terrible, so we avoid the problem by cloning the constraints.
303

304 305 306 307 308
-}

simplifyRule :: RuleName
             -> WantedConstraints       -- Constraints from LHS
             -> WantedConstraints       -- Constraints from RHS
309 310 311
             -> TcM ( [EvVar]               -- Quantify over these LHS vars
                    , WantedConstraints)    -- Residual un-quantified LHS constraints
-- See Note [The SimplifyRule Plan]
312 313
-- NB: This consumes all simple constraints on the LHS, but not
-- any LHS implication constraints.
314
simplifyRule name lhs_wanted rhs_wanted
315
  = do {
316 317 318
       -- Note [The SimplifyRule Plan] step 1
       -- First solve the LHS and *then* solve the RHS
       -- Crucially, this performs unifications
319 320 321 322 323 324 325 326 327
       -- Why clone?  See Note [Simplify cloned constraints]
       ; lhs_clone <- cloneWC lhs_wanted
       ; rhs_clone <- cloneWC rhs_wanted
       ; runTcSDeriveds $
             do { _ <- solveWanteds lhs_clone
                ; _ <- solveWanteds rhs_clone
                  -- Why do them separately?
                  -- See Note [Solve order for RULES]
                ; return () }
328

329
       -- Note [The SimplifyRule Plan] step 2
330 331
       ; lhs_wanted <- zonkWC lhs_wanted
       ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
332 333 334

       -- Note [The SimplifyRule Plan] step 3
       ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
335 336

       ; traceTc "simplifyRule" $
337
         vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
338 339 340
              , text "lhs_wanted" <+> ppr lhs_wanted
              , text "rhs_wanted" <+> ppr rhs_wanted
              , text "quant_cts" <+> ppr quant_cts
341
              , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
342 343
              ]

344
       ; return (quant_evs, residual_lhs_wanted) }
345 346

  where
347 348 349 350 351 352 353 354 355 356
    mk_quant_ev :: Ct -> TcM EvVar
    mk_quant_ev ct
      | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
      = case dest of
          EvVarDest ev_id -> return ev_id
          HoleDest hole   -> -- See Note [Quantifying over coercion holes]
                             do { ev_id <- newEvVar pred
                                ; fillCoercionHole hole (mkTcCoVarCo ev_id)
                                ; return ev_id }
    mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413


getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
-- Extract all the constraints we can quantify over,
--   also returning the depleted WantedConstraints
--
-- NB: we must look inside implications, because with
--     -fdefer-type-errors we generate implications rather eagerly;
--     see TcUnify.implicationNeeded. Not doing so caused Trac #14732.
--
-- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
--   and attempt to solve them from the quantified constraints.  That
--   nearly works, but fails for a constraint like (d :: Eq Int).
--   We /do/ want to quantify over it, but the short-cut solver
--   (see TcInteract Note [Shortcut solving]) ignores the quantified
--   and instead solves from the top level.
--
--   So we must partition the WantedConstraints ourselves
--   Not hard, but tiresome.

getRuleQuantCts wc
  = float_wc emptyVarSet wc
  where
    float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
    float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics })
      = ( simple_yes `andCts` implic_yes
        , WC { wc_simple = simple_no, wc_impl = implics_no })
     where
        (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
        (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
                                                emptyBag implics

    float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
    float_implic skol_tvs yes1 imp
      = (yes1 `andCts` yes2, imp { ic_wanted = no })
      where
        (yes2, no) = float_wc new_skol_tvs (ic_wanted imp)
        new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp

    rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
    rule_quant_ct skol_tvs ct
      | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
      , not (ok_eq t1 t2)
       = False        -- Note [RULE quantification over equalities]
      | isHoleCt ct
      = False         -- Don't quantify over type holes, obviously
      | otherwise
      = tyCoVarsOfCt ct `disjointVarSet` skol_tvs

    ok_eq t1 t2
       | t1 `tcEqType` t2 = False
       | otherwise        = is_fun_app t1 || is_fun_app t2

    is_fun_app ty   -- ty is of form (F tys) where F is a type function
      = case tyConAppTyCon_maybe ty of
          Just tc -> isTypeFamilyTyCon tc
          Nothing -> False