OptCoercion.lhs 21.8 KB
Newer Older
1 2 3 4 5
%
% (c) The University of Glasgow 2006
%

\begin{code}
6 7
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
Ian Lynagh's avatar
Ian Lynagh committed
8 9 10
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
11
--     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
Ian Lynagh's avatar
Ian Lynagh committed
12 13
-- for details

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
14
module OptCoercion ( optCoercion, checkAxInstCo ) where 
15 16 17 18 19

#include "HsVersions.h"

import Coercion
import Type hiding( substTyVarBndr, substTy, extendTvSubst )
20
import TcType       ( exactTyVarsOfType )
21
import TyCon
22
import CoAxiom
23 24
import Var
import VarSet
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
25
import FamInstEnv   ( flattenTys )
26 27 28 29
import VarEnv
import StaticFlags	( opt_NoOptCoercion )
import Outputable
import Pair
30
import Maybes
31
import FastString
32
import Util
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
33
import Unify
34
import ListSetOps
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
35
import InstEnv
Icelandjack's avatar
Icelandjack committed
36
import Control.Monad   ( zipWithM )
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
\end{code}

%************************************************************************
%*                                                                      *
                 Optimising coercions									
%*                                                                      *
%************************************************************************

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
mkCoPredTy in the ForAll case, where this note appears.  

\begin{code}
optCoercion :: CvSubst -> Coercion -> NormalCo
-- ^ optCoercion applies a substitution to a coercion, 
--   *and* optimises it to reduce its size
optCoercion env co 
  | opt_NoOptCoercion = substCo env co
68
  | otherwise         = opt_co env False Nothing co
69 70 71 72 73 74 75 76 77 78 79 80

type NormalCo = Coercion
  -- Invariants: 
  --  * 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

opt_co, opt_co' :: CvSubst
       		-> Bool	       -- True <=> return (sym co)
81 82
                -> Maybe Role  -- Nothing <=> don't change; otherwise, change
                               -- INVARIANT: the change is always a *downgrade*
83 84
       		-> Coercion
       		-> NormalCo	
85
opt_co = opt_co' 
86 87 88 89 90
{-
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
91 92
   (WARN( not same_co_kind, ppr co  <+> dcolon <+> ppr (coercionType co)
                         $$ ppr co1 <+> dcolon <+> ppr (coercionType co1) )
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
    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
-}

111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
opt_co' env _   mrole (Refl r ty) = Refl (mrole `orElse` r) (substTy env ty)
opt_co' env sym mrole co
  |  mrole == Just Phantom 
  || coercionRole co == Phantom
  , Pair ty1 ty2 <- coercionKind co
  = if sym
    then opt_univ env Phantom ty2 ty1
    else opt_univ env Phantom ty1 ty2

opt_co' env sym mrole (SymCo co)  = opt_co env (not sym) mrole co
opt_co' env sym mrole (TyConAppCo r tc cos)
  = case mrole of
      Nothing -> mkTyConAppCo r  tc (map (opt_co env sym Nothing) cos)
      Just r' -> mkTyConAppCo r' tc (zipWith (opt_co env sym)
                                             (map Just (tyConRolesX r' tc)) cos)
opt_co' env sym mrole (AppCo co1 co2) = mkAppCo (opt_co env sym mrole   co1)
                                                (opt_co env sym Nothing co2)
opt_co' env sym mrole (ForAllCo tv co)
  = case substTyVarBndr env tv of
      (env', tv') -> mkForAllCo tv' (opt_co env' sym mrole co)
131 132
     -- Use the "mk" functions to check for nested Refls

133
opt_co' env sym mrole (CoVarCo cv)
134
  | Just co <- lookupCoVar env cv
135
  = opt_co (zapCvSubstEnv env) sym mrole co
136 137

  | Just cv1 <- lookupInScope (getCvInScope env) cv
138
  = ASSERT( isCoVar cv1 ) wrapRole mrole cv_role $ wrapSym sym (CoVarCo cv1)
139 140 141 142
                -- cv1 might have a substituted kind!

  | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
                ASSERT( isCoVar cv )
143 144
                wrapRole mrole cv_role $ wrapSym sym (CoVarCo cv)
  where cv_role = coVarRole cv
145

146
opt_co' env sym mrole (AxiomInstCo con ind cos)
147 148 149 150
    -- 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) !!
151 152 153
  = wrapRole mrole (coAxiomRole con) $
    wrapSym sym $
    AxiomInstCo con ind (map (opt_co env False Nothing) cos)
154 155
      -- Note that the_co does *not* have sym pushed into it

156 157
opt_co' env sym mrole (UnivCo r oty1 oty2)
  = opt_univ env role a b
158
  where
159 160
    (a,b) = if sym then (oty2,oty1) else (oty1,oty2)
    role = mrole `orElse` r
161

162
opt_co' env sym mrole (TransCo co1 co2)
163 164
  | sym       = opt_trans in_scope opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
  | otherwise = opt_trans in_scope opt_co1 opt_co2
165
  where
166 167
    opt_co1 = opt_co env sym mrole co1
    opt_co2 = opt_co env sym mrole co2
168
    in_scope = getCvInScope env
169

170 171 172 173 174
-- NthCo roles are fiddly!
opt_co' env sym mrole (NthCo n (TyConAppCo _ _ cos))
  = opt_co env sym mrole (getNth cos n)
opt_co' env sym mrole (NthCo n co)
  | TyConAppCo _ _tc cos <- co'
175
  , isDecomposableTyCon tc   -- Not synonym families
176
  = ASSERT( n < length cos )
177 178 179 180 181 182 183 184
    ASSERT( _tc == tc )
    let resultCo = cos !! n
        resultRole = coercionRole resultCo in
    case (mrole, resultRole) of
        -- if we just need an R coercion, try to propagate the SubCo again:
      (Just Representational, Nominal) -> opt_co (zapCvSubstEnv env) False mrole resultCo
      _                                -> resultCo

185
  | otherwise
186
  = wrap_role $ NthCo n co'
187

188 189 190 191 192 193 194 195 196 197 198 199 200 201
  where
    wrap_role wrapped = wrapRole mrole (coercionRole wrapped) wrapped

    tc = tyConAppTyCon $ pFst $ coercionKind co
    co' = opt_co env sym mrole' co
    mrole' = case mrole of
               Just Representational
                 | Representational <- nthRole Representational tc n
                 -> Just Representational
               _ -> Nothing

opt_co' env sym mrole (LRCo lr co)
  | Just pr_co <- splitAppCo_maybe co
  = opt_co env sym mrole (pickLR lr pr_co)
202
  | Just pr_co <- splitAppCo_maybe co'
203 204 205
  = if mrole == Just Representational
    then opt_co (zapCvSubstEnv env) False mrole (pickLR lr pr_co)
    else pickLR lr pr_co
206
  | otherwise
207
  = wrapRole mrole Nominal $ LRCo lr co'
208
  where
209
    co' = opt_co env sym Nothing co
210

211
opt_co' env sym mrole (InstCo co ty)
212 213 214
    -- See if the first arg is already a forall
    -- ...then we can just extend the current substitution
  | Just (tv, co_body) <- splitForAllCo_maybe co
215
  = opt_co (extendTvSubst env tv ty') sym mrole co_body
216

217 218
     -- See if it is a forall after optimization
     -- If so, do an inefficient one-variable substitution
219
  | Just (tv, co'_body) <- splitForAllCo_maybe co'
220
  = substCoWithTy (getCvInScope env) tv ty' co'_body   
221 222 223

  | otherwise = InstCo co' ty'
  where
224
    co' = opt_co env sym mrole co
225 226
    ty' = substTy env ty

227 228
opt_co' env sym _ (SubCo co) = opt_co env sym (Just Representational) co

229 230 231 232 233 234 235 236 237 238
-- XXX: We could add another field to CoAxiomRule that
-- would allow us to do custom simplifications.
opt_co' env sym mrole (AxiomRuleCo co ts cs) =
  wrapRole mrole (coaxrRole co) $
    wrapSym sym $
    AxiomRuleCo co (map (substTy env) ts)
                   (zipWith (opt_co env False) (map Just (coaxrAsmpRoles co)) cs)



239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
-------------
opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
opt_univ env role oty1 oty2
  | Just (tc1, tys1) <- splitTyConApp_maybe oty1
  , Just (tc2, tys2) <- splitTyConApp_maybe oty2
  , tc1 == tc2
  = mkTyConAppCo role tc1 (zipWith3 (opt_univ env) (tyConRolesX role tc1) tys1 tys2)

  | 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
    mkAppCo (opt_univ env role l1 l2) (opt_univ env role' r1 r2)

  | 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
    mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) role ty1' ty2') }

  | otherwise
  = mkUnivCo role (substTy env oty1) (substTy env oty2)

265
-------------
266 267
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
268

269 270
opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans is co1 co2
271
  | isReflCo co1 = co2
272
  | otherwise    = opt_trans1 is co1 co2
273

274
opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
275
-- First arg is not the identity
276
opt_trans1 is co1 co2
277
  | isReflCo co2 = co1
278
  | otherwise    = opt_trans2 is co1 co2
279

280
opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
281
-- Neither arg is the identity
282
opt_trans2 is (TransCo co1a co1b) co2
283
    -- Don't know whether the sub-coercions are the identity
284
  = opt_trans is co1a (opt_trans is co1b co2)  
285

286 287
opt_trans2 is co1 co2 
  | Just co <- opt_trans_rule is co1 co2
288 289
  = co

290 291
opt_trans2 is co1 (TransCo co2a co2b)
  | Just co1_2a <- opt_trans_rule is co1 co2a
292 293
  = if isReflCo co1_2a
    then co2b
294
    else opt_trans1 is co1_2a co2b
295

296
opt_trans2 _ co1 co2
297 298 299 300
  = mkTransCo co1 co2

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

303
-- Push transitivity through matching destructors
304
opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
305 306 307
  | d1 == d2
  , co1 `compatible_co` co2
  = fireTransRule "PushNth" in_co1 in_co2 $
308
    mkNthCo d1 (opt_trans is co1 co2)
309

310 311 312 313 314 315
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)

316
-- Push transitivity inside instantiation
317
opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
318 319 320
  | ty1 `eqType` ty2
  , co1 `compatible_co` co2
  = fireTransRule "TrPushInst" in_co1 in_co2 $
321
    mkInstCo (opt_trans is co1 co2) ty1
322
 
323
-- Push transitivity down through matching top-level constructors.
324
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
325
  | tc1 == tc2 
326 327 328
  = ASSERT( r1 == r2 )
    fireTransRule "PushTyConApp" in_co1 in_co2 $
    TyConAppCo r1 tc1 (opt_transList is cos1 cos2)
329

330
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
331
  = fireTransRule "TrPushApp" in_co1 in_co2 $
332
    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
333

334
-- Eta rules
335
opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
336 337 338
  | Just cos2 <- etaTyConAppCo_maybe tc co2
  = ASSERT( length cos1 == length cos2 )
    fireTransRule "EtaCompL" co1 co2 $
339
    TyConAppCo r tc (opt_transList is cos1 cos2)
340

341
opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
342 343 344
  | Just cos1 <- etaTyConAppCo_maybe tc co1
  = ASSERT( length cos1 == length cos2 )
    fireTransRule "EtaCompR" co1 co2 $
345
    TyConAppCo r tc (opt_transList is cos1 cos2)
346

347 348 349 350 351 352 353 354 355 356
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)

357
-- Push transitivity inside forall
358
opt_trans_rule is co1 co2
359 360
  | Just (tv1,r1) <- splitForAllCo_maybe co1
  , Just (tv2,r2) <- etaForAllCo_maybe co2
361 362
  , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
        is' = is `extendInScopeSet` tv1
363
  = fireTransRule "EtaAllL" co1 co2 $
364
    mkForAllCo tv1 (opt_trans2 is' r1 r2')
365 366 367

  | Just (tv2,r2) <- splitForAllCo_maybe co2
  , Just (tv1,r1) <- etaForAllCo_maybe co1
368 369
  , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
        is' = is `extendInScopeSet` tv2
370
  = fireTransRule "EtaAllR" co1 co2 $
371
    mkForAllCo tv1 (opt_trans2 is' r1' r2)
372 373

-- Push transitivity inside axioms
374
opt_trans_rule is co1 co2
375

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
376
  -- TrPushSymAxR
377 378
  | 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
379 380 381 382
  , True <- sym
  , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
383

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400
  -- 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

  -- TrPushAxL  
401 402
  | 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
403 404 405 406
  , False <- sym
  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
  , Nothing <- checkAxInstCo newAxInst
  = fireTransRule "TrPushAxL" co1 co2 newAxInst
407 408

  -- TrPushAxSym/TrPushSymAx
409 410
  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
411
  , con1 == con2
412
  , ind1 == ind2
413
  , sym1 == not sym2
414 415 416 417
  , let branch = coAxiomNthBranch con1 ind1
        qtvs = coAxBranchTyVars branch
        lhs  = coAxNthLHS con1 ind1
        rhs  = coAxBranchRHS branch
418 419 420 421
        pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
  , all (`elemVarSet` pivot_tvs) qtvs
  = fireTransRule "TrPushAxSym" co1 co2 $
    if sym2
422 423
    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
424 425 426
  where
    co1_is_axiom_maybe = isAxiom_maybe co1
    co2_is_axiom_maybe = isAxiom_maybe co2
427
    role = coercionRole co1 -- should be the same as coercionRole co2!
428

429
opt_trans_rule _ co1 co2	-- Identity rule
430 431 432 433
  | Pair ty1 _ <- coercionKind co1
  , Pair _ ty2 <- coercionKind co2
  , ty1 `eqType` ty2
  = fireTransRule "RedTypeDirRefl" co1 co2 $
434
    Refl (coercionRole co1) ty2
435

436
opt_trans_rule _ _ _ = Nothing
437 438 439 440 441 442

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
\end{code}

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 }

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
464
Note [Branched instance checking] in types/FamInstEnv.lhs.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
465 466 467

\begin{code}
-- | Check to make sure that an AxInstCo is internally consistent.
468
-- Returns the conflicting branch, if it exists
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
469
-- See Note [Conflict checking with AxiomInstCo]
470
checkAxInstCo :: Coercion -> Maybe CoAxBranch
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
471
-- defined here to avoid dependencies in Coercion
472 473
-- 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
474 475 476
checkAxInstCo (AxiomInstCo ax ind cos)
  = let branch = coAxiomNthBranch ax ind
        tvs = coAxBranchTyVars branch
477
        incomps = coAxBranchIncomps branch
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
478 479
        tys = map (pFst . coercionKind) cos 
        subst = zipOpenTvSubst tvs tys
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
480 481 482 483 484
        target = Type.substTys subst (coAxBranchLHS branch)
        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
485
  where
486 487
    check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
    check_no_conflict _    [] = Nothing
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
488 489 490 491
    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
492
      | otherwise
493
      = Just b
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
494 495
checkAxInstCo _ = Nothing

496 497 498 499 500
-----------
wrapSym :: Bool -> Coercion -> Coercion
wrapSym sym co | sym       = SymCo co
               | otherwise = co

501 502 503 504
wrapRole :: Maybe Role   -- desired
         -> Role         -- current
         -> Coercion -> Coercion
wrapRole Nothing        _       = id
505
wrapRole (Just desired) current = downgradeRole desired current
506 507 508 509 510 511 512 513 514 515 516 517 518

-----------
-- 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')
    
zapCvSubstEnv2 :: CvSubst -> CvSubst -> CvSubst
zapCvSubstEnv2 env1 env2 = mkCvSubst (is1 `unionInScope` is2) []
  where is1 = getCvInScope env1
        is2 = getCvInScope env2
519
-----------
520
isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
521
isAxiom_maybe (SymCo co) 
522 523 524 525
  | 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)
526 527 528
isAxiom_maybe _ = Nothing

matchAxiom :: Bool -- True = match LHS, False = match RHS
529
           -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
530 531
-- 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
532
matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
533 534 535 536
  = let (CoAxBranch { cab_tvs   = qtvs
                    , cab_roles = roles
                    , cab_lhs   = lhs
                    , cab_rhs   = rhs }) = coAxiomNthBranch ax ind in
537
    case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
538
      Nothing    -> Nothing
Icelandjack's avatar
Icelandjack committed
539
      Just subst -> zipWithM (liftCoSubstTyVar subst) roles qtvs
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

-------------
compatible_co :: Coercion -> Coercion -> Bool
-- Check whether (co1 . co2) will be well-kinded
compatible_co co1 co2
  = x1 `eqType` x2		
  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

566 567 568 569 570 571 572
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)
573 574
  | Nominal <- coercionRole co
  , Pair ty1 ty2 <- coercionKind co
575 576 577
  , Just (_,t1) <- splitAppTy_maybe ty1
  , Just (_,t2) <- splitAppTy_maybe ty2
  , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
578 579 580 581
  = Just (LRCo CLeft co, LRCo CRight co)
  | otherwise
  = Nothing

582 583 584 585
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
-- If possible, split a coercion 
--       g :: T s1 .. sn ~ T t1 .. tn
-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 
586
etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
587 588 589 590 591 592 593 594 595 596 597
  = 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
  = ASSERT( tc == tc1 ) 
    ASSERT( n == length tys2 )
598
    Just (decomposeCo n co)
599 600 601 602 603 604 605
    -- NB: n might be <> tyConArity tc
    -- e.g.   data family T a :: * -> *
    --        g :: T a b ~ T c d

  | otherwise
  = Nothing
\end{code}  
606 607 608

Note [Eta for AppCo]
~~~~~~~~~~~~~~~~~~~~
Gabor Greif's avatar
typos  
Gabor Greif committed
609
Suppose we have 
610 611 612 613 614
   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
615
because it's possible that
616 617 618 619 620 621 622 623 624 625 626 627
   s1 :: * -> *         t1 :: *
   s2 :: (*->*) -> *    t2 :: * -> *
and in that case (left g) does not have the same
kind on either side.

It's enough to check that 
  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