OptCoercion.hs 26.6 KB
Newer Older
1
-- (c) The University of Glasgow 2006
2

3
{-# LANGUAGE CPP #-}
Ian Lynagh's avatar
Ian Lynagh committed
4

5
module OptCoercion ( optCoercion, checkAxInstCo ) where
6 7 8 9 10

#include "HsVersions.h"

import Coercion
import Type hiding( substTyVarBndr, substTy, extendTvSubst )
11
import TcType       ( exactTyVarsOfType )
12
import TyCon
13
import CoAxiom
14 15
import Var
import VarSet
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
16
import FamInstEnv   ( flattenTys )
17
import VarEnv
18
import StaticFlags      ( opt_NoOptCoercion )
19 20 21
import Outputable
import Pair
import FastString
22
import Util
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
23
import Unify
24
import ListSetOps
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
25
import InstEnv
Icelandjack's avatar
Icelandjack committed
26
import Control.Monad   ( zipWithM )
27

28 29 30
{-
************************************************************************
*                                                                      *
31
                 Optimising coercions
32 33
*                                                                      *
************************************************************************
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49

Note [Subtle shadowing in coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Supose we optimising a coercion
    optCoercion (forall (co_X5:t1~t2). ...co_B1...)
The co_X5 is a wild-card; the bound variable of a coercion for-all
should never appear in the body of the forall. Indeed we often
write it like this
    optCoercion ( (t1~t2) => ...co_B1... )

Just because it's a wild-card doesn't mean we are free to choose
whatever variable we like.  For example it'd be wrong for optCoercion
to return
   forall (co_B1:t1~t2). ...co_B1...
because now the co_B1 (which is really free) has been captured, and
subsequent substitutions will go wrong.  That's why we can't use
50
mkCoPredTy in the ForAll case, where this note appears.
51

52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
Note [Optimising coercion optimisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Looking up a coercion's role or kind is linear in the size of the
coercion. Thus, doing this repeatedly during the recursive descent
of coercion optimisation is disastrous. We must be careful to avoid
doing this if at all possible.

Because it is generally easy to know a coercion's components' roles
from the role of the outer coercion, we pass down the known role of
the input in the algorithm below. We also keep functions opt_co2
and opt_co3 separate from opt_co4, so that the former two do Phantom
checks that opt_co4 can avoid. This is a big win because Phantom coercions
rarely appear within non-phantom coercions -- only in some TyConAppCos
and some AxiomInstCos. We handle these cases specially by calling
opt_co2.
67
-}
68

69
optCoercion :: CvSubst -> Coercion -> NormalCo
70
-- ^ optCoercion applies a substitution to a coercion,
71
--   *and* optimises it to reduce its size
72
optCoercion env co
73
  | opt_NoOptCoercion = substCo env co
74
  | otherwise         = opt_co1 env False co
75 76

type NormalCo = Coercion
77
  -- Invariants:
78 79 80 81 82 83 84
  --  * The substitution has been fully applied
  --  * For trans coercions (co1 `trans` co2)
  --       co1 is not a trans, and neither co1 nor co2 is identity
  --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)

type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity

85 86 87 88 89 90 91 92 93 94
-- | Do we apply a @sym@ to the result?
type SymFlag = Bool

-- | Do we force the result to be representational?
type ReprFlag = Bool

-- | Optimize a coercion, making no assumptions.
opt_co1 :: CvSubst
        -> SymFlag
        -> Coercion -> NormalCo
95
opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
96 97 98 99 100
{-
opt_co env sym co
 = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
   co1 `seq`
   pprTrace "opt_co done }" (ppr co1) $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
101 102
   (WARN( not same_co_kind, ppr co  <+> dcolon <+> ppr (coercionType co)
                         $$ ppr co1 <+> dcolon <+> ppr (coercionType co1) )
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
    WARN( not (coreEqCoercion co1 simple_result),
           (text "env=" <+> ppr env) $$
           (text "input=" <+> ppr co) $$
           (text "simple=" <+> ppr simple_result) $$
           (text "opt=" <+> ppr co1) )
   co1)
 where
   co1 = opt_co' env sym co
   same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
   Pair s t = coercionKind (substCo env co)
   (s1,t1) | sym = (t,s)
           | otherwise = (s,t)
   Pair s2 t2 = coercionKind co1

   simple_result | sym = mkSymCo (substCo env co)
                 | otherwise = substCo env co
-}

121 122 123 124 125 126
-- See Note [Optimising coercion optimisation]
-- | Optimize a coercion, knowing the coercion's role. No other assumptions.
opt_co2 :: CvSubst
        -> SymFlag
        -> Role   -- ^ The role of the input coercion
        -> Coercion -> NormalCo
127 128
opt_co2 env sym Phantom co = opt_phantom env sym co
opt_co2 env sym r       co = opt_co3 env sym Nothing r co
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162

-- See Note [Optimising coercion optimisation]
-- | Optimize a coercion, knowing the coercion's non-Phantom role.
opt_co3 :: CvSubst -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
opt_co3 env sym (Just Representational) r co = opt_co4 env sym True  r co
  -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
opt_co3 env sym _                       r co = opt_co4 env sym False r co


-- See Note [Optimising coercion optimisation]
-- | Optimize a non-phantom coercion.
opt_co4 :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo

opt_co4 env _   rep r (Refl _r ty)
  = ASSERT( r == _r )
    Refl (chooseRole rep r) (substTy env ty)

opt_co4 env sym rep r (SymCo co)  = opt_co4 env (not sym) rep r co

opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
  = ASSERT( r == _r )
    case (rep, r) of
      (True, Nominal) ->
        mkTyConAppCo Representational tc
                     (zipWith3 (opt_co3 env sym)
                               (map Just (tyConRolesX Representational tc))
                               (repeat Nominal)
                               cos)
      (False, Nominal) ->
        mkTyConAppCo Nominal tc (map (opt_co4 env sym False Nominal) cos)
      (_, Representational) ->
                      -- must use opt_co2 here, because some roles may be P
                      -- See Note [Optimising coercion optimisation]
163
        mkTyConAppCo r tc (zipWith (opt_co2 env sym)
164 165 166 167 168 169 170
                                   (tyConRolesX r tc)  -- the current roles
                                   cos)
      (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)

opt_co4 env sym rep r (AppCo co1 co2) = mkAppCo (opt_co4 env sym rep r co1)
                                                (opt_co4 env sym False Nominal co2)
opt_co4 env sym rep r (ForAllCo tv co)
171
  = case substTyVarBndr env tv of
172
      (env', tv') -> mkForAllCo tv' (opt_co4 env' sym rep r co)
173 174
     -- Use the "mk" functions to check for nested Refls

175
opt_co4 env sym rep r (CoVarCo cv)
176
  | Just co <- lookupCoVar env cv
177
  = opt_co4 (zapCvSubstEnv env) sym rep r co
178 179

  | Just cv1 <- lookupInScope (getCvInScope env) cv
180
  = ASSERT( isCoVar cv1 ) wrapRole rep r $ wrapSym sym (CoVarCo cv1)
181 182 183 184
                -- cv1 might have a substituted kind!

  | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
                ASSERT( isCoVar cv )
185
                wrapRole rep r $ wrapSym sym (CoVarCo cv)
186

187
opt_co4 env sym rep r (AxiomInstCo con ind cos)
188 189 190 191
    -- Do *not* push sym inside top-level axioms
    -- e.g. if g is a top-level axiom
    --   g a : f a ~ a
    -- then (sym (g ty)) /= g (sym ty) !!
192 193
  = ASSERT( r == coAxiomRole con )
    wrapRole rep (coAxiomRole con) $
194
    wrapSym sym $
195 196
                       -- some sub-cos might be P: use opt_co2
                       -- See Note [Optimising coercion optimisation]
197
    AxiomInstCo con ind (zipWith (opt_co2 env False)
198 199
                                 (coAxBranchRoles (coAxiomNthBranch con ind))
                                 cos)
200 201
      -- Note that the_co does *not* have sym pushed into it

202
opt_co4 env sym rep r (UnivCo s _r oty1 oty2)
203
  = ASSERT( r == _r )
204
    opt_univ env s (chooseRole rep r) a b
205
  where
206
    (a,b) = if sym then (oty2,oty1) else (oty1,oty2)
207

208 209 210 211
opt_co4 env sym rep r (TransCo co1 co2)
                      -- sym (g `o` h) = sym h `o` sym g
  | sym       = opt_trans in_scope co2' co1'
  | otherwise = opt_trans in_scope co1' co2'
212
  where
213 214
    co1' = opt_co4 env sym rep r co1
    co2' = opt_co4 env sym rep r co2
215
    in_scope = getCvInScope env
216

217
opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co
218

219
opt_co4 env sym rep r (LRCo lr co)
220
  | Just pr_co <- splitAppCo_maybe co
221 222
  = ASSERT( r == Nominal )
    opt_co4 env sym rep Nominal (pickLR lr pr_co)
223
  | Just pr_co <- splitAppCo_maybe co'
224 225 226
  = ASSERT( r == Nominal )
    if rep
    then opt_co4 (zapCvSubstEnv env) False True Nominal (pickLR lr pr_co)
227
    else pickLR lr pr_co
228
  | otherwise
229
  = wrapRole rep Nominal $ LRCo lr co'
230
  where
231
    co' = opt_co4 env sym False Nominal co
232

233
opt_co4 env sym rep r (InstCo co ty)
234 235 236
    -- See if the first arg is already a forall
    -- ...then we can just extend the current substitution
  | Just (tv, co_body) <- splitForAllCo_maybe co
237
  = opt_co4 (extendTvSubst env tv ty') sym rep r co_body
238

239 240
     -- See if it is a forall after optimization
     -- If so, do an inefficient one-variable substitution
241
  | Just (tv, co'_body) <- splitForAllCo_maybe co'
242
  = substCoWithTy (getCvInScope env) tv ty' co'_body
243 244 245

  | otherwise = InstCo co' ty'
  where
246
    co' = opt_co4 env sym rep r co
247 248
    ty' = substTy env ty

249 250 251
opt_co4 env sym _ r (SubCo co)
  = ASSERT( r == Representational )
    opt_co4 env sym True Nominal co
252

253 254
-- XXX: We could add another field to CoAxiomRule that
-- would allow us to do custom simplifications.
255 256 257
opt_co4 env sym rep r (AxiomRuleCo co ts cs)
  = ASSERT( r == coaxrRole co )
    wrapRole rep r $
258 259
    wrapSym sym $
    AxiomRuleCo co (map (substTy env) ts)
260
                   (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
261 262


263
-------------
264 265 266 267 268
-- | Optimize a phantom coercion. The input coercion may not necessarily
-- be a phantom, but the output sure will be.
opt_phantom :: CvSubst -> SymFlag -> Coercion -> NormalCo
opt_phantom env sym co
  = if sym
269 270
    then opt_univ env (fsLit "opt_phantom") Phantom ty2 ty1
    else opt_univ env (fsLit "opt_phantom") Phantom ty1 ty2
271 272 273
  where
    Pair ty1 ty2 = coercionKind co

274 275
opt_univ :: CvSubst -> FastString -> Role -> Type -> Type -> Coercion
opt_univ env prov role oty1 oty2
276 277 278
  | Just (tc1, tys1) <- splitTyConApp_maybe oty1
  , Just (tc2, tys2) <- splitTyConApp_maybe oty2
  , tc1 == tc2
279
  = mkTyConAppCo role tc1 (zipWith3 (opt_univ env prov) (tyConRolesX role tc1) tys1 tys2)
280 281 282 283 284 285

  | Just (l1, r1) <- splitAppTy_maybe oty1
  , Just (l2, r2) <- splitAppTy_maybe oty2
  , typeKind l1 `eqType` typeKind l2   -- kind(r1) == kind(r2) by consequence
  = let role' = if role == Phantom then Phantom else Nominal in
       -- role' is to comform to mkAppCo's precondition
286
    mkAppCo (opt_univ env prov role l1 l2) (opt_univ env prov role' r1 r2)
287 288 289 290 291 292 293

  | Just (tv1, ty1) <- splitForAllTy_maybe oty1
  , Just (tv2, ty2) <- splitForAllTy_maybe oty2
  , tyVarKind tv1 `eqType` tyVarKind tv2  -- rule out a weird unsafeCo
  = case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
    let ty1' = substTy env1 ty1
        ty2' = substTy env2 ty2 in
294
    mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) prov role ty1' ty2') }
295 296

  | otherwise
297
  = mkUnivCo prov role (substTy env oty1) (substTy env oty2)
298

299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323
-------------
-- NthCo must be handled separately, because it's the one case where we can't
-- tell quickly what the component coercion's role is from the containing
-- coercion. To avoid repeated coercionRole calls as opt_co1 calls opt_co2,
-- we just look for nested NthCo's, which can happen in practice.
opt_nth_co :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
opt_nth_co env sym rep r = go []
  where
    go ns (NthCo n co) = go (n:ns) co
      -- previous versions checked if the tycon is decomposable. This
      -- is redundant, because a non-decomposable tycon under an NthCo
      -- is entirely bogus. See docs/core-spec/core-spec.pdf.
    go ns co
      = opt_nths ns co

      -- input coercion is *not* yet sym'd or opt'd
    opt_nths [] co = opt_co4 env sym rep r co
    opt_nths (n:ns) (TyConAppCo _ _ cos) = opt_nths ns (cos `getNth` n)

      -- here, the co isn't a TyConAppCo, so we opt it, hoping to get
      -- a TyConAppCo as output. We don't know the role, so we use
      -- opt_co1. This is slightly annoying, because opt_co1 will call
      -- coercionRole, but as long as we don't have a long chain of
      -- NthCo's interspersed with some other coercion former, we should
      -- be OK.
324
    opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
325 326 327 328 329 330 331 332 333 334 335 336 337

      -- input coercion *is* sym'd and opt'd
    opt_nths' [] co
      = if rep && (r == Nominal)
            -- propagate the SubCo:
        then opt_co4 (zapCvSubstEnv env) False True r co
        else co
    opt_nths' (n:ns) (TyConAppCo _ _ cos) = opt_nths' ns (cos `getNth` n)
    opt_nths' ns co = wrapRole rep r (mk_nths ns co)

    mk_nths [] co = co
    mk_nths (n:ns) co = mk_nths ns (mkNthCo n co)

338
-------------
339 340
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
341

342 343
opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans is co1 co2
344
  | isReflCo co1 = co2
345
  | otherwise    = opt_trans1 is co1 co2
346

347
opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
348
-- First arg is not the identity
349
opt_trans1 is co1 co2
350
  | isReflCo co2 = co1
351
  | otherwise    = opt_trans2 is co1 co2
352

353
opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
354
-- Neither arg is the identity
355
opt_trans2 is (TransCo co1a co1b) co2
356
    -- Don't know whether the sub-coercions are the identity
357
  = opt_trans is co1a (opt_trans is co1b co2)
358

359
opt_trans2 is co1 co2
360
  | Just co <- opt_trans_rule is co1 co2
361 362
  = co

363 364
opt_trans2 is co1 (TransCo co2a co2b)
  | Just co1_2a <- opt_trans_rule is co1 co2a
365 366
  = if isReflCo co1_2a
    then co2b
367
    else opt_trans1 is co1_2a co2b
368

369
opt_trans2 _ co1 co2
370 371 372 373
  = mkTransCo co1 co2

------
-- Optimize coercions with a top-level use of transitivity.
374
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
375

376
-- Push transitivity through matching destructors
377
opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
378 379 380
  | d1 == d2
  , co1 `compatible_co` co2
  = fireTransRule "PushNth" in_co1 in_co2 $
381
    mkNthCo d1 (opt_trans is co1 co2)
382

383 384 385 386 387 388
opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
  | d1 == d2
  , co1 `compatible_co` co2
  = fireTransRule "PushLR" in_co1 in_co2 $
    mkLRCo d1 (opt_trans is co1 co2)

389
-- Push transitivity inside instantiation
390
opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
391 392 393
  | ty1 `eqType` ty2
  , co1 `compatible_co` co2
  = fireTransRule "TrPushInst" in_co1 in_co2 $
394
    mkInstCo (opt_trans is co1 co2) ty1
395

396
-- Push transitivity down through matching top-level constructors.
397
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
398
  | tc1 == tc2
399 400 401
  = ASSERT( r1 == r2 )
    fireTransRule "PushTyConApp" in_co1 in_co2 $
    TyConAppCo r1 tc1 (opt_transList is cos1 cos2)
402

403
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
404
  = fireTransRule "TrPushApp" in_co1 in_co2 $
405
    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
406

407
-- Eta rules
408
opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
409 410 411
  | Just cos2 <- etaTyConAppCo_maybe tc co2
  = ASSERT( length cos1 == length cos2 )
    fireTransRule "EtaCompL" co1 co2 $
412
    TyConAppCo r tc (opt_transList is cos1 cos2)
413

414
opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
415 416 417
  | Just cos1 <- etaTyConAppCo_maybe tc co1
  = ASSERT( length cos1 == length cos2 )
    fireTransRule "EtaCompR" co1 co2 $
418
    TyConAppCo r tc (opt_transList is cos1 cos2)
419

420 421 422 423 424 425 426 427 428 429
opt_trans_rule is co1@(AppCo co1a co1b) co2
  | Just (co2a,co2b) <- etaAppCo_maybe co2
  = fireTransRule "EtaAppL" co1 co2 $
    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)

opt_trans_rule is co1 co2@(AppCo co2a co2b)
  | Just (co1a,co1b) <- etaAppCo_maybe co1
  = fireTransRule "EtaAppR" co1 co2 $
    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)

430
-- Push transitivity inside forall
431
opt_trans_rule is co1 co2
432 433
  | Just (tv1,r1) <- splitForAllCo_maybe co1
  , Just (tv2,r2) <- etaForAllCo_maybe co2
434 435
  , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
        is' = is `extendInScopeSet` tv1
436
  = fireTransRule "EtaAllL" co1 co2 $
437
    mkForAllCo tv1 (opt_trans2 is' r1 r2')
438 439 440

  | Just (tv2,r2) <- splitForAllCo_maybe co2
  , Just (tv1,r1) <- etaForAllCo_maybe co1
441 442
  , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
        is' = is `extendInScopeSet` tv2
443
  = fireTransRule "EtaAllR" co1 co2 $
444
    mkForAllCo tv1 (opt_trans2 is' r1' r2)
445 446

-- Push transitivity inside axioms
447
opt_trans_rule is co1 co2
448

449
  -- See Note [Why call checkAxInstCo during optimisation]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
450
  -- TrPushSymAxR
451 452
  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
  , Just cos2 <- matchAxiom sym con ind co2
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
453 454 455 456
  , True <- sym
  , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
457

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473
  -- TrPushAxR
  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
  , Just cos2 <- matchAxiom sym con ind co2
  , False <- sym
  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushAxR" co1 co2 newAxInst

  -- TrPushSymAxL
  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
  , Just cos1 <- matchAxiom (not sym) con ind co1
  , True <- sym
  , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst

474
  -- TrPushAxL
475 476
  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
  , Just cos1 <- matchAxiom (not sym) con ind co1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
477 478 479 480
  , False <- sym
  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushAxL" co1 co2 newAxInst
481 482

  -- TrPushAxSym/TrPushSymAx
483 484
  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
485
  , con1 == con2
486
  , ind1 == ind2
487
  , sym1 == not sym2
488 489 490 491
  , let branch = coAxiomNthBranch con1 ind1
        qtvs = coAxBranchTyVars branch
        lhs  = coAxNthLHS con1 ind1
        rhs  = coAxBranchRHS branch
492 493 494 495
        pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
  , all (`elemVarSet` pivot_tvs) qtvs
  = fireTransRule "TrPushAxSym" co1 co2 $
    if sym2
496 497
    then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
    else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
498 499 500
  where
    co1_is_axiom_maybe = isAxiom_maybe co1
    co2_is_axiom_maybe = isAxiom_maybe co2
501
    role = coercionRole co1 -- should be the same as coercionRole co2!
502

503
opt_trans_rule _ co1 co2        -- Identity rule
504
  | (Pair ty1 _, r) <- coercionKindRole co1
505 506 507
  , Pair _ ty2 <- coercionKind co2
  , ty1 `eqType` ty2
  = fireTransRule "RedTypeDirRefl" co1 co2 $
508
    Refl r ty2
509

510
opt_trans_rule _ _ _ = Nothing
511 512 513 514 515 516

fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule _rule _co1 _co2 res
  = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
    Just res

517
{-
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
518 519 520 521 522 523 524 525 526 527 528 529 530
Note [Conflict checking with AxiomInstCo]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following type family and axiom:

type family Equal (a :: k) (b :: k) :: Bool
type instance where
  Equal a a = True
  Equal a b = False
--
Equal :: forall k::BOX. k -> k -> Bool
axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
           ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }

531 532 533 534 535 536 537
We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
0-based, so this is the second branch of the axiom.) The problem is that, on
the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
False) and that all is OK. But, all is not OK: we want to use the first branch
of the axiom in this case, not the second. The problem is that the parameters
of the first branch can unify with the supplied coercions, thus meaning that
the first branch should be taken. See also Note [Branched instance checking]
538
in types/FamInstEnv.hs.
539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571

Note [Why call checkAxInstCo during optimisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is possible that otherwise-good-looking optimisations meet with disaster
in the presence of axioms with multiple equations. Consider

type family Equal (a :: *) (b :: *) :: Bool where
  Equal a a = True
  Equal a b = False
type family Id (a :: *) :: * where
  Id a = a

axEq :: { [a::*].       Equal a a ~ True
        ; [a::*, b::*]. Equal a b ~ False }
axId :: [a::*]. Id a ~ a

co1 = Equal (axId[0] Int) (axId[0] Bool)
  :: Equal (Id Int) (Id Bool) ~  Equal Int Bool
co2 = axEq[1] <Int> <Bool>
  :: Equal Int Bool ~ False

We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
happens when we push the coercions inside? We get

co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
  :: Equal (Id Int) (Id Bool) ~ False

which is bogus! This is because the type system isn't smart enough to know
that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
families. At the time of writing, I (Richard Eisenberg) couldn't think of
a way of detecting this any more efficient than just building the optimised
coercion and checking.
572
-}
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
573 574

-- | Check to make sure that an AxInstCo is internally consistent.
575
-- Returns the conflicting branch, if it exists
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
576
-- See Note [Conflict checking with AxiomInstCo]
577
checkAxInstCo :: Coercion -> Maybe CoAxBranch
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
578
-- defined here to avoid dependencies in Coercion
579 580
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism] in CoreLint
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
581
checkAxInstCo (AxiomInstCo ax ind cos)
582 583 584
  = let branch   = coAxiomNthBranch ax ind
        tvs      = coAxBranchTyVars branch
        incomps  = coAxBranchIncomps branch
585
        tys      = map (pFst . coercionKind) cos
586 587
        subst    = zipOpenTvSubst tvs tys
        target   = Type.substTys subst (coAxBranchLHS branch)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
588 589 590 591
        in_scope = mkInScopeSet $
                   unionVarSets (map (tyVarsOfTypes . coAxBranchLHS) incomps)
        flattened_target = flattenTys in_scope target in
    check_no_conflict flattened_target incomps
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
592
  where
593 594
    check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
    check_no_conflict _    [] = Nothing
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
595 596 597 598
    check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
         -- See Note [Apartness] in FamInstEnv
      | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
      = check_no_conflict flat rest
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
599
      | otherwise
600
      = Just b
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
601 602
checkAxInstCo _ = Nothing

603
-----------
604
wrapSym :: SymFlag -> Coercion -> Coercion
605 606 607
wrapSym sym co | sym       = SymCo co
               | otherwise = co

608 609 610
-- | Conditionally set a role to be representational
wrapRole :: ReprFlag
         -> Role         -- ^ current role
611
         -> Coercion -> Coercion
612 613 614 615 616 617 618 619 620 621
wrapRole False _       = id
wrapRole True  current = downgradeRole Representational current

-- | If we require a representational role, return that. Otherwise,
-- return the "default" role provided.
chooseRole :: ReprFlag
           -> Role    -- ^ "default" role
           -> Role
chooseRole True _ = Representational
chooseRole _    r = r
622 623 624 625 626 627 628
-----------
-- takes two tyvars and builds env'ts to map them to the same tyvar
substTyVarBndr2 :: CvSubst -> TyVar -> TyVar
                -> (CvSubst, CvSubst, TyVar)
substTyVarBndr2 env tv1 tv2
  = case substTyVarBndr env tv1 of
      (env1, tv1') -> (env1, extendTvSubstAndInScope env tv2 (mkTyVarTy tv1'), tv1')
629

630 631 632 633
zapCvSubstEnv2 :: CvSubst -> CvSubst -> CvSubst
zapCvSubstEnv2 env1 env2 = mkCvSubst (is1 `unionInScope` is2) []
  where is1 = getCvInScope env1
        is2 = getCvInScope env2
634
-----------
635
isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
636
isAxiom_maybe (SymCo co)
637 638 639 640
  | Just (sym, con, ind, cos) <- isAxiom_maybe co
  = Just (not sym, con, ind, cos)
isAxiom_maybe (AxiomInstCo con ind cos)
  = Just (False, con, ind, cos)
641 642 643
isAxiom_maybe _ = Nothing

matchAxiom :: Bool -- True = match LHS, False = match RHS
644
           -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
645 646
-- If we succeed in matching, then *all the quantified type variables are bound*
-- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
647
matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
648 649 650 651
  = let (CoAxBranch { cab_tvs   = qtvs
                    , cab_roles = roles
                    , cab_lhs   = lhs
                    , cab_rhs   = rhs }) = coAxiomNthBranch ax ind in
652
    case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
653
      Nothing    -> Nothing
Icelandjack's avatar
Icelandjack committed
654
      Just subst -> zipWithM (liftCoSubstTyVar subst) roles qtvs
655 656 657 658 659

-------------
compatible_co :: Coercion -> Coercion -> Bool
-- Check whether (co1 . co2) will be well-kinded
compatible_co co1 co2
660
  = x1 `eqType` x2
661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680
  where
    Pair _ x1 = coercionKind co1
    Pair x2 _ = coercionKind co2

-------------
etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
-- Try to make the coercion be of form (forall tv. co)
etaForAllCo_maybe co
  | Just (tv, r) <- splitForAllCo_maybe co
  = Just (tv, r)

  | Pair ty1 ty2  <- coercionKind co
  , Just (tv1, _) <- splitForAllTy_maybe ty1
  , Just (tv2, _) <- splitForAllTy_maybe ty2
  , tyVarKind tv1 `eqKind` tyVarKind tv2
  = Just (tv1, mkInstCo co (mkTyVarTy tv1))

  | otherwise
  = Nothing

681 682 683 684 685 686 687
etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
-- If possible, split a coercion
--   g :: t1a t1b ~ t2a t2b
-- into a pair of coercions (left g, right g)
etaAppCo_maybe co
  | Just (co1,co2) <- splitAppCo_maybe co
  = Just (co1,co2)
688
  | (Pair ty1 ty2, Nominal) <- coercionKindRole co
689 690 691
  , Just (_,t1) <- splitAppTy_maybe ty1
  , Just (_,t2) <- splitAppTy_maybe ty2
  , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
692 693 694 695
  = Just (LRCo CLeft co, LRCo CRight co)
  | otherwise
  = Nothing

696
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
697
-- If possible, split a coercion
698
--       g :: T s1 .. sn ~ T t1 .. tn
699
-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
700
etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
701 702 703 704 705 706 707 708 709
  = ASSERT( tc == tc2 ) Just cos2

etaTyConAppCo_maybe tc co
  | isDecomposableTyCon tc
  , Pair ty1 ty2     <- coercionKind co
  , Just (tc1, tys1) <- splitTyConApp_maybe ty1
  , Just (tc2, tys2) <- splitTyConApp_maybe ty2
  , tc1 == tc2
  , let n = length tys1
710
  = ASSERT( tc == tc1 )
711
    ASSERT( n == length tys2 )
712
    Just (decomposeCo n co)
713 714 715 716 717 718
    -- NB: n might be <> tyConArity tc
    -- e.g.   data family T a :: * -> *
    --        g :: T a b ~ T c d

  | otherwise
  = Nothing
719

720
{-
721 722
Note [Eta for AppCo]
~~~~~~~~~~~~~~~~~~~~
723
Suppose we have
724 725 726 727 728
   g :: s1 t1 ~ s2 t2

Then we can't necessarily make
   left  g :: s1 ~ s2
   right g :: t1 ~ t2
Gabor Greif's avatar
typos  
Gabor Greif committed
729
because it's possible that
730 731 732 733 734
   s1 :: * -> *         t1 :: *
   s2 :: (*->*) -> *    t2 :: * -> *
and in that case (left g) does not have the same
kind on either side.

735
It's enough to check that
736 737 738 739 740
  kind t1 = kind t2
because if g is well-kinded then
  kind (s1 t2) = kind (s2 t2)
and these two imply
  kind s1 = kind s2
741
-}