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

3
{-# LANGUAGE CPP #-}
4 5 6
 -- This module used to take 10GB of memory to compile with the new
 -- (Nov '15) pattern-match check. In order to be able to compile it,
 -- do not enable -ffull-guard-reasoning. Instead, simplify the guards
7
 -- (default behaviour when guards are too many).
Ian Lynagh's avatar
Ian Lynagh committed
8

9
module OptCoercion ( optCoercion, checkAxInstCo ) where
10 11 12

#include "HsVersions.h"

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

31
{-
32 33
%************************************************************************
%*                                                                      *
34
                 Optimising coercions
35 36
%*                                                                      *
%************************************************************************
37

38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
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.
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81

Note [Optimising InstCo]
~~~~~~~~~~~~~~~~~~~~~~~~
When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.

Let's look at the typing rules.

h : k1 ~ k2
tv:k1 |- g : t1 ~ t2
-----------------------------
ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])

g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
g2 : s1 ~ s2
--------------------
InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]

We thus want some coercion proving this:

  (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])

If we substitute the *type* tv for the *coercion*
(g2 `mkCoherenceRightCo` sym h) in g, we'll get this result exactly.
This is bizarre,
though, because we're substituting a type variable with a coercion. However,
this operation already exists: it's called *lifting*, and defined in Coercion.
We just need to enhance the lifting operation to be able to deal with
an ambient substitution, which is why a LiftingContext stores a TCvSubst.

82
-}
83

84
optCoercion :: TCvSubst -> Coercion -> NormalCo
85
-- ^ optCoercion applies a substitution to a coercion,
86
--   *and* optimises it to reduce its size
87
optCoercion env co
88
  | opt_NoOptCoercion = substCo env co
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
89 90 91 92 93
  | debugIsOn
  = let out_co = opt_co1 lc False co
        (Pair in_ty1  in_ty2,  in_role)  = coercionKindRole co
        (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
    in
94 95
    ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
             substTyUnchecked env in_ty2 `eqType` out_ty2 &&
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
96 97 98 99 100 101 102 103 104 105 106
             in_role == out_role
           , text "optCoercion changed types!"
             $$ hang (text "in_co:") 2 (ppr co)
             $$ hang (text "in_ty1:") 2 (ppr in_ty1)
             $$ hang (text "in_ty2:") 2 (ppr in_ty2)
             $$ hang (text "out_co:") 2 (ppr out_co)
             $$ hang (text "out_ty1:") 2 (ppr out_ty1)
             $$ hang (text "out_ty2:") 2 (ppr out_ty2)
             $$ hang (text "subst:") 2 (ppr env) )
    out_co

107 108 109
  | otherwise         = opt_co1 lc False co
  where
    lc = mkSubstLiftingContext env
110

111
type NormalCo    = Coercion
112
  -- Invariants:
113 114 115 116 117 118
  --  * The substitution has been fully applied
  --  * For trans coercions (co1 `trans` co2)
  --       co1 is not a trans, and neither co1 nor co2 is identity

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

119 120 121 122 123 124
-- | Do we apply a @sym@ to the result?
type SymFlag = Bool

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

125 126 127
-- | Optimize a coercion, making no assumptions. All coercions in
-- the lifting context are already optimized (and sym'd if nec'y)
opt_co1 :: LiftingContext
128 129
        -> SymFlag
        -> Coercion -> NormalCo
130
opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
131

132 133
-- See Note [Optimising coercion optimisation]
-- | Optimize a coercion, knowing the coercion's role. No other assumptions.
134
opt_co2 :: LiftingContext
135 136 137
        -> SymFlag
        -> Role   -- ^ The role of the input coercion
        -> Coercion -> NormalCo
138 139
opt_co2 env sym Phantom co = opt_phantom env sym co
opt_co2 env sym r       co = opt_co3 env sym Nothing r co
140 141 142

-- See Note [Optimising coercion optimisation]
-- | Optimize a coercion, knowing the coercion's non-Phantom role.
143 144 145
opt_co3 :: LiftingContext -> 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_wrap env sym True  r co
146
  -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
147
opt_co3 env sym _                       r co = opt_co4_wrap env sym False r co
148 149 150

-- See Note [Optimising coercion optimisation]
-- | Optimize a non-phantom coercion.
151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo

opt_co4_wrap = opt_co4
{-
opt_co4_wrap env sym rep r co
  = pprTrace "opt_co4_wrap {"
    ( vcat [ text "Sym:" <+> ppr sym
           , text "Rep:" <+> ppr rep
           , text "Role:" <+> ppr r
           , text "Co:" <+> ppr co ]) $
    ASSERT( r == coercionRole co )
    let result = opt_co4 env sym rep r co in
    pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
    result
-}
166 167

opt_co4 env _   rep r (Refl _r ty)
168 169 170 171
  = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
                      text "Found role:" <+> ppr _r   $$
                      text "Type:" <+> ppr ty )
    liftCoSubst (chooseRole rep r) env ty
172

173 174 175 176 177
opt_co4 env sym rep r (SymCo co)  = opt_co4_wrap env (not sym) rep r co
  -- surprisingly, we don't have to do anything to the env here. This is
  -- because any "lifting" substitutions in the env are tied to ForAllCos,
  -- which treat their left and right sides differently. We don't want to
  -- exchange them.
178 179 180 181 182 183 184 185 186 187 188

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) ->
189
        mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
190 191 192
      (_, Representational) ->
                      -- must use opt_co2 here, because some roles may be P
                      -- See Note [Optimising coercion optimisation]
193
        mkTyConAppCo r tc (zipWith (opt_co2 env sym)
194 195 196 197
                                   (tyConRolesX r tc)  -- the current roles
                                   cos)
      (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)

198 199 200 201 202 203 204 205
opt_co4 env sym rep r (AppCo co1 co2)
  = mkAppCo (opt_co4_wrap env sym rep r co1)
            (opt_co4_wrap env sym False Nominal co2)

opt_co4 env sym rep r (ForAllCo tv k_co co)
  = case optForAllCoBndr env sym tv k_co of
      (env', tv', k_co') -> mkForAllCo tv' k_co' $
                            opt_co4_wrap env' sym rep r co
206 207
     -- Use the "mk" functions to check for nested Refls

208
opt_co4 env sym rep r (CoVarCo cv)
209 210
  | Just co <- lookupCoVar (lcTCvSubst env) cv
  = opt_co4_wrap (zapLiftingContext env) sym rep r co
211

212
  | Just cv1 <- lookupInScope (lcInScopeSet env) cv
213
  = ASSERT( isCoVar cv1 ) wrapRole rep r $ wrapSym sym (CoVarCo cv1)
214 215
                -- cv1 might have a substituted kind!

216
  | otherwise = WARN( True, text "opt_co: not in scope:" <+> ppr cv $$ ppr env)
217
                ASSERT( isCoVar cv )
218
                wrapRole rep r $ wrapSym sym (CoVarCo cv)
219

220
opt_co4 env sym rep r (AxiomInstCo con ind cos)
221 222 223 224
    -- 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) !!
225 226
  = ASSERT( r == coAxiomRole con )
    wrapRole rep (coAxiomRole con) $
227
    wrapSym sym $
228 229
                       -- some sub-cos might be P: use opt_co2
                       -- See Note [Optimising coercion optimisation]
230
    AxiomInstCo con ind (zipWith (opt_co2 env False)
231 232
                                 (coAxBranchRoles (coAxiomNthBranch con ind))
                                 cos)
233 234
      -- Note that the_co does *not* have sym pushed into it

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
235
opt_co4 env sym rep r (UnivCo prov _r t1 t2)
236
  = ASSERT( r == _r )
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
237
    opt_univ env sym prov (chooseRole rep r) t1 t2
238

239 240 241 242
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'
243
  where
244 245 246 247
    co1' = opt_co4_wrap env sym rep r co1
    co2' = opt_co4_wrap env sym rep r co2
    in_scope = lcInScopeSet env

248

249
opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co
250

251
opt_co4 env sym rep r (LRCo lr co)
252
  | Just pr_co <- splitAppCo_maybe co
253
  = ASSERT( r == Nominal )
254
    opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
255
  | Just pr_co <- splitAppCo_maybe co'
256 257
  = ASSERT( r == Nominal )
    if rep
258 259
    then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
    else pick_lr lr pr_co
260
  | otherwise
261
  = wrapRole rep Nominal $ LRCo lr co'
262
  where
263
    co' = opt_co4_wrap env sym False Nominal co
264

265 266
    pick_lr CLeft  (l, _) = l
    pick_lr CRight (_, r) = r
267

268 269 270 271 272 273 274
-- See Note [Optimising InstCo]
opt_co4 env sym rep r (InstCo co1 arg)
    -- forall over type...
  | Just (tv, kind_co, co_body) <- splitForAllCo_maybe co1
  = opt_co4_wrap (extendLiftingContext env tv
                    (arg' `mkCoherenceRightCo` mkSymCo kind_co))
                 sym rep r co_body
275

276 277 278 279 280 281 282 283 284 285
    -- See if it is a forall after optimization
    -- If so, do an inefficient one-variable substitution, then re-optimize

    -- forall over type...
  | Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1'
  = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
                    (arg' `mkCoherenceRightCo` mkSymCo kind_co'))
            False False r' co_body'

  | otherwise = InstCo co1' arg'
286
  where
287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314
    co1' = opt_co4_wrap env sym rep r co1
    r'   = chooseRole rep r
    arg' = opt_co4_wrap env sym False Nominal arg

opt_co4 env sym rep r (CoherenceCo co1 co2)
  | TransCo col1 cor1 <- co1
  = opt_co4_wrap env sym rep r (mkTransCo (mkCoherenceCo col1 co2) cor1)

  | TransCo col1' cor1' <- co1'
  = if sym then opt_trans in_scope col1'
                  (optCoercion (zapTCvSubst (lcTCvSubst env))
                               (mkCoherenceRightCo cor1' co2'))
           else opt_trans in_scope (mkCoherenceCo col1' co2') cor1'

  | otherwise
  = wrapSym sym $ CoherenceCo (opt_co4_wrap env False rep r co1) co2'
  where co1' = opt_co4_wrap env sym   rep   r       co1
        co2' = opt_co4_wrap env False False Nominal co2
        in_scope = lcInScopeSet env

opt_co4 env sym _rep r (KindCo co)
  = ASSERT( r == Nominal )
    let kco' = promoteCoercion co in
    case kco' of
      KindCo co' -> promoteCoercion (opt_co1 env sym co')
      _          -> opt_co4_wrap env sym False Nominal kco'
  -- This might be able to be optimized more to do the promotion
  -- and substitution/optimization at the same time
315

316 317
opt_co4 env sym _ r (SubCo co)
  = ASSERT( r == Representational )
318
    opt_co4_wrap env sym True Nominal co
319

320 321
-- This could perhaps be optimized more.
opt_co4 env sym rep r (AxiomRuleCo co cs)
322 323
  = ASSERT( r == coaxrRole co )
    wrapRole rep r $
324
    wrapSym sym $
325
    AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
326

327
-------------
328 329
-- | Optimize a phantom coercion. The input coercion may not necessarily
-- be a phantom, but the output sure will be.
330
opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
331
opt_phantom env sym co
332
  = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
333 334 335
  where
    Pair ty1 ty2 = coercionKind co

336 337 338 339 340 341 342 343 344 345 346
opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
         -> Type -> Type -> Coercion
opt_univ env sym (PhantomProv h) _r ty1 ty2
  | sym       = mkPhantomCo h' ty2' ty1'
  | otherwise = mkPhantomCo h' ty1' ty2'
  where
    h' = opt_co4 env sym False Nominal h
    ty1' = substTy (lcSubstLeft  env) ty1
    ty2' = substTy (lcSubstRight env) ty2

opt_univ env sym prov role oty1 oty2
347 348 349
  | Just (tc1, tys1) <- splitTyConApp_maybe oty1
  , Just (tc2, tys2) <- splitTyConApp_maybe oty2
  , tc1 == tc2
350 351 352 353 354 355 356
      -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
      -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
  = let roles    = tyConRolesX role tc1
        arg_cos  = zipWith3 (mkUnivCo prov) roles tys1 tys2
        arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
    in
    mkTyConAppCo role tc1 arg_cos'
357

358
  -- can't optimize the AppTy case because we can't build the kind coercions.
359 360 361

  | Just (tv1, ty1) <- splitForAllTy_maybe oty1
  , Just (tv2, ty2) <- splitForAllTy_maybe oty2
362 363 364 365 366 367 368 369 370 371
      -- NB: prov isn't interesting here either
  = let k1   = tyVarKind tv1
        k2   = tyVarKind tv2
        eta  = mkUnivCo prov Nominal k1 k2
          -- eta gets opt'ed soon, but not yet.
        ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2

        (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
    in
    mkForAllCo tv1' eta' (opt_univ env' sym prov role ty1 ty2')
372 373

  | otherwise
374 375
  = let ty1 = substTyUnchecked (lcSubstLeft  env) oty1
        ty2 = substTyUnchecked (lcSubstRight env) oty2
376 377 378 379 380 381 382 383 384 385 386 387 388
        (a, b) | sym       = (ty2, ty1)
               | otherwise = (ty1, ty2)
    in
    mkUnivCo prov' role a b

  where
    prov' = case prov of
      UnsafeCoerceProv   -> prov
      PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
      ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
      PluginProv _       -> prov
      HoleProv h         -> pprPanic "opt_univ fell into a hole" (ppr h)

389

390 391 392 393 394
-------------
-- 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.
395
opt_nth_co :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
396 397 398 399 400 401 402 403 404
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

405 406 407 408 409 410 411 412 413 414 415 416 417
      -- try to resolve 1 Nth
    push_nth n (Refl r1 ty)
      | Just (tc, args) <- splitTyConApp_maybe ty
      = Just (Refl (nthRole r1 tc n) (args `getNth` n))
      | n == 0
      , Just (tv, _) <- splitForAllTy_maybe ty
      = Just (Refl Nominal (tyVarKind tv))
    push_nth n (TyConAppCo _ _ cos)
      = Just (cos `getNth` n)
    push_nth 0 (ForAllCo _ eta _)
      = Just eta
    push_nth _ _ = Nothing

418
      -- input coercion is *not* yet sym'd or opt'd
419 420 421 422
    opt_nths [] co = opt_co4_wrap env sym rep r co
    opt_nths (n:ns) co
      | Just co' <- push_nth n co
      = opt_nths ns co'
423 424 425 426 427 428 429

      -- 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.
430
    opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
431 432 433 434 435

      -- input coercion *is* sym'd and opt'd
    opt_nths' [] co
      = if rep && (r == Nominal)
            -- propagate the SubCo:
436
        then opt_co4_wrap (zapLiftingContext env) False True r co
437
        else co
438 439 440
    opt_nths' (n:ns) co
      | Just co' <- push_nth n co
      = opt_nths' ns co'
441 442 443 444 445
    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)

446
-------------
447 448
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
449

450 451
opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans is co1 co2
452
  | isReflCo co1 = co2
453
  | otherwise    = opt_trans1 is co1 co2
454

455
opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
456
-- First arg is not the identity
457
opt_trans1 is co1 co2
458
  | isReflCo co2 = co1
459
  | otherwise    = opt_trans2 is co1 co2
460

461
opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
462
-- Neither arg is the identity
463
opt_trans2 is (TransCo co1a co1b) co2
464
    -- Don't know whether the sub-coercions are the identity
465
  = opt_trans is co1a (opt_trans is co1b co2)
466

467
opt_trans2 is co1 co2
468
  | Just co <- opt_trans_rule is co1 co2
469 470
  = co

471 472
opt_trans2 is co1 (TransCo co2a co2b)
  | Just co1_2a <- opt_trans_rule is co1 co2a
473 474
  = if isReflCo co1_2a
    then co2b
475
    else opt_trans1 is co1_2a co2b
476

477
opt_trans2 _ co1 co2
478 479 480 481
  = mkTransCo co1 co2

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

484
-- Push transitivity through matching destructors
485
opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
486 487 488
  | d1 == d2
  , co1 `compatible_co` co2
  = fireTransRule "PushNth" in_co1 in_co2 $
489
    mkNthCo d1 (opt_trans is co1 co2)
490

491 492 493 494 495 496
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)

497
-- Push transitivity inside instantiation
498
opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
499
  | ty1 `eqCoercion` ty2
500 501
  , co1 `compatible_co` co2
  = fireTransRule "TrPushInst" in_co1 in_co2 $
502
    mkInstCo (opt_trans is co1 co2) ty1
503

504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519
opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
                  in_co2@(UnivCo p2 r2 _tyl2 tyr2)
  | Just prov' <- opt_trans_prov p1 p2
  = ASSERT( r1 == r2 )
    fireTransRule "UnivCo" in_co1 in_co2 $
    mkUnivCo prov' r1 tyl1 tyr2
  where
    -- if the provenances are different, opt'ing will be very confusing
    opt_trans_prov UnsafeCoerceProv      UnsafeCoerceProv      = Just UnsafeCoerceProv
    opt_trans_prov (PhantomProv kco1)    (PhantomProv kco2)
      = Just $ PhantomProv $ opt_trans is kco1 kco2
    opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
      = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
    opt_trans_prov (PluginProv str1)     (PluginProv str2)     | str1 == str2 = Just p1
    opt_trans_prov _ _ = Nothing

520
-- Push transitivity down through matching top-level constructors.
521
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
522
  | tc1 == tc2
523 524
  = ASSERT( r1 == r2 )
    fireTransRule "PushTyConApp" in_co1 in_co2 $
525
    mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
526

527
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
528
  = fireTransRule "TrPushApp" in_co1 in_co2 $
529 530
    mkAppCo (opt_trans is co1a co2a)
            (opt_trans is co1b co2b)
531

532
-- Eta rules
533
opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
534 535 536
  | Just cos2 <- etaTyConAppCo_maybe tc co2
  = ASSERT( length cos1 == length cos2 )
    fireTransRule "EtaCompL" co1 co2 $
537
    mkTyConAppCo r tc (opt_transList is cos1 cos2)
538

539
opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
540 541 542
  | Just cos1 <- etaTyConAppCo_maybe tc co1
  = ASSERT( length cos1 == length cos2 )
    fireTransRule "EtaCompR" co1 co2 $
543
    mkTyConAppCo r tc (opt_transList is cos1 cos2)
544

545 546 547
opt_trans_rule is co1@(AppCo co1a co1b) co2
  | Just (co2a,co2b) <- etaAppCo_maybe co2
  = fireTransRule "EtaAppL" co1 co2 $
548 549
    mkAppCo (opt_trans is co1a co2a)
            (opt_trans is co1b co2b)
550 551 552 553

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

557
-- Push transitivity inside forall
558
opt_trans_rule is co1 co2
559 560 561 562 563 564 565 566 567 568 569 570 571 572 573
  | ForAllCo tv1 eta1 r1 <- co1
  , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2
  = push_trans tv1 eta1 r1 tv2 eta2 r2

  | ForAllCo tv2 eta2 r2 <- co2
  , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1
  = push_trans tv1 eta1 r1 tv2 eta2 r2

  where
  push_trans tv1 eta1 r1 tv2 eta2 r2
    = fireTransRule "EtaAllTy" co1 co2 $
      mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
    where
      is' = is `extendInScopeSet` tv1
      r2' = substCoWith [tv2] [TyVarTy tv1] r2
574 575

-- Push transitivity inside axioms
576
opt_trans_rule is co1 co2
577

578
  -- See Note [Why call checkAxInstCo during optimisation]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
579
  -- TrPushSymAxR
580
  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
581
  , True <- sym
582
  , Just cos2 <- matchAxiom sym con ind co2
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
583 584 585
  , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
586

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
587 588 589
  -- TrPushAxR
  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
  , False <- sym
590
  , Just cos2 <- matchAxiom sym con ind co2
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
591 592 593 594 595 596 597
  , 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
  , True <- sym
598
  , Just cos1 <- matchAxiom (not sym) con ind co1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
599 600 601 602
  , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst

603
  -- TrPushAxL
604
  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
605
  , False <- sym
606
  , Just cos1 <- matchAxiom (not sym) con ind co1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
607 608 609
  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushAxL" co1 co2 newAxInst
610 611

  -- TrPushAxSym/TrPushSymAx
612 613
  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
614
  , con1 == con2
615
  , ind1 == ind2
616
  , sym1 == not sym2
617
  , let branch = coAxiomNthBranch con1 ind1
618
        qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
619 620
        lhs  = coAxNthLHS con1 ind1
        rhs  = coAxBranchRHS branch
621
        pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
622 623 624
  , all (`elemVarSet` pivot_tvs) qtvs
  = fireTransRule "TrPushAxSym" co1 co2 $
    if sym2
625 626 627 628
       -- TrPushAxSym
    then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
       -- TrPushSymAx
    else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
629 630 631
  where
    co1_is_axiom_maybe = isAxiom_maybe co1
    co2_is_axiom_maybe = isAxiom_maybe co2
632
    role = coercionRole co1 -- should be the same as coercionRole co2!
633

634 635 636 637 638 639
opt_trans_rule is co1 co2
  | Just (lco, lh) <- isCohRight_maybe co1
  , Just (rco, rh) <- isCohLeft_maybe co2
  , (coercionType lh) `eqType` (coercionType rh)
  = opt_trans_rule is lco rco

640
opt_trans_rule _ co1 co2        -- Identity rule
641
  | (Pair ty1 _, r) <- coercionKindRole co1
642 643 644
  , Pair _ ty2 <- coercionKind co2
  , ty1 `eqType` ty2
  = fireTransRule "RedTypeDirRefl" co1 co2 $
645
    Refl r ty2
646

647
opt_trans_rule _ _ _ = Nothing
648 649 650 651 652 653

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

654
{-
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
655 656 657 658 659 660 661 662 663
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
--
664 665 666
Equal :: forall k::*. k -> k -> Bool
axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
           ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
667

668 669 670 671 672 673
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
Jan Stolarek's avatar
Jan Stolarek committed
674 675
the first branch should be taken. See also Note [Apartness] in
types/FamInstEnv.hs.
676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708

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.
709
-}
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
710 711

-- | Check to make sure that an AxInstCo is internally consistent.
712
-- Returns the conflicting branch, if it exists
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
713
-- See Note [Conflict checking with AxiomInstCo]
714
checkAxInstCo :: Coercion -> Maybe CoAxBranch
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
715
-- defined here to avoid dependencies in Coercion
716 717
-- 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
718
checkAxInstCo (AxiomInstCo ax ind cos)
719 720 721 722 723 724 725 726
  = let branch       = coAxiomNthBranch ax ind
        tvs          = coAxBranchTyVars branch
        cvs          = coAxBranchCoVars branch
        incomps      = coAxBranchIncomps branch
        (tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
        co_args      = map stripCoercionTy cotys
        subst        = zipOpenTCvSubst tvs tys `composeTCvSubst`
                       zipOpenTCvSubstCoVars cvs co_args
727
        target   = Type.substTys subst (coAxBranchLHS branch)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
728
        in_scope = mkInScopeSet $
729
                   unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
730 731
        flattened_target = flattenTys in_scope target in
    check_no_conflict flattened_target incomps
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
732
  where
733 734
    check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
    check_no_conflict _    [] = Nothing
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
735 736 737 738
    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
739
      | otherwise
740
      = Just b
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
741 742
checkAxInstCo _ = Nothing

743

744
-----------
745
wrapSym :: SymFlag -> Coercion -> Coercion
746 747 748
wrapSym sym co | sym       = SymCo co
               | otherwise = co

749 750 751
-- | Conditionally set a role to be representational
wrapRole :: ReprFlag
         -> Role         -- ^ current role
752
         -> Coercion -> Coercion
753 754 755 756 757 758 759 760 761 762
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
763

764
-----------
765
isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
766
isAxiom_maybe (SymCo co)
767 768 769 770
  | 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)
771 772 773
isAxiom_maybe _ = Nothing

matchAxiom :: Bool -- True = match LHS, False = match RHS
774 775
           -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800
  | CoAxBranch { cab_tvs = qtvs
               , cab_cvs = []   -- can't infer these, so fail if there are any
               , cab_roles = roles
               , cab_lhs = lhs
               , cab_rhs = rhs } <- coAxiomNthBranch ax ind
  , Just subst <- liftCoMatch (mkVarSet qtvs)
                              (if sym then (mkTyConApp tc lhs) else rhs)
                              co
  , all (`isMappedByLC` subst) qtvs
  = zipWithM (liftCoSubstTyVar subst) roles qtvs

  | otherwise
  = Nothing

-------------
-- destruct a CoherenceCo
isCohLeft_maybe :: Coercion -> Maybe (Coercion, Coercion)
isCohLeft_maybe (CoherenceCo co1 co2) = Just (co1, co2)
isCohLeft_maybe _                     = Nothing

-- destruct a (sym (co1 |> co2)).
-- if isCohRight_maybe co = Just (co1, co2), then (sym co1) `mkCohRightCo` co2 = co
isCohRight_maybe :: Coercion -> Maybe (Coercion, Coercion)
isCohRight_maybe (SymCo (CoherenceCo co1 co2)) = Just (mkSymCo co1, co2)
isCohRight_maybe _                             = Nothing
801 802 803 804 805

-------------
compatible_co :: Coercion -> Coercion -> Bool
-- Check whether (co1 . co2) will be well-kinded
compatible_co co1 co2
806
  = x1 `eqType` x2
807 808 809 810 811
  where
    Pair _ x1 = coercionKind co1
    Pair x2 _ = coercionKind co2

-------------
812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838
{-
etaForAllCo_maybe
~~~~~~~~~~~~~~~~~
Suppose we have

  g : all a1:k1.t1  ~  all a2:k2.t2

but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:

  g' = all a1:(ForAllKindCo g).(InstCo g (a1 `mkCoherenceRightCo` ForAllKindCo g))

Call the kind coercion h1 and the body coercion h2. We can see that

  h2 : t1 ~ t2[a2 |-> (a1 |> h2)]

According to the typing rule for ForAllCo, we get that

  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h2)][a1 |-> a1 |> sym h2])

or

  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> a1])

as desired.
-}
etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
-- Try to make the coercion be of form (forall tv:kind_co. co)
839
etaForAllCo_maybe co
840 841
  | ForAllCo tv kind_co r <- co
  = Just (tv, kind_co, r)
842 843 844

  | Pair ty1 ty2  <- coercionKind co
  , Just (tv1, _) <- splitForAllTy_maybe ty1
845 846 847 848
  , isForAllTy ty2
  , let kind_co = mkNthCo 0 co
  = Just ( tv1, kind_co
         , mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_co) )
849 850 851 852

  | otherwise
  = Nothing

853 854 855 856 857 858 859
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)
860
  | (Pair ty1 ty2, Nominal) <- coercionKindRole co
861 862
  , Just (_,t1) <- splitAppTy_maybe ty1
  , Just (_,t2) <- splitAppTy_maybe ty2
863 864 865
  , let isco1 = isCoercionTy t1
  , let isco2 = isCoercionTy t2
  , isco1 == isco2
866 867 868 869
  = Just (LRCo CLeft co, LRCo CRight co)
  | otherwise
  = Nothing

870
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
871
-- If possible, split a coercion
872
--       g :: T s1 .. sn ~ T t1 .. tn
873
-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
874
etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
875 876 877
  = ASSERT( tc == tc2 ) Just cos2

etaTyConAppCo_maybe tc co
878
  | mightBeUnsaturatedTyCon tc
879 880 881 882 883
  , Pair ty1 ty2     <- coercionKind co
  , Just (tc1, tys1) <- splitTyConApp_maybe ty1
  , Just (tc2, tys2) <- splitTyConApp_maybe ty2
  , tc1 == tc2
  , let n = length tys1
884
  = ASSERT( tc == tc1 )
885
    ASSERT( n == length tys2 )
886
    Just (decomposeCo n co)
887 888 889 890 891 892
    -- NB: n might be <> tyConArity tc
    -- e.g.   data family T a :: * -> *
    --        g :: T a b ~ T c d

  | otherwise
  = Nothing
893

894
{-
895 896
Note [Eta for AppCo]
~~~~~~~~~~~~~~~~~~~~
897
Suppose we have
898 899 900 901 902
   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
903
because it's possible that
904 905 906 907 908
   s1 :: * -> *         t1 :: *
   s2 :: (*->*) -> *    t2 :: * -> *
and in that case (left g) does not have the same
kind on either side.

909
It's enough to check that
910 911 912 913 914
  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
915

916
-}
917 918 919 920 921

optForAllCoBndr :: LiftingContext -> Bool
                -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
optForAllCoBndr env sym
  = substForAllCoBndrCallbackLC sym (opt_co4_wrap env sym False Nominal) env