Fix AMP warnings.
[ghc.git] / compiler / types / OptCoercion.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 {-# OPTIONS -fno-warn-tabs #-}
7 -- The above warning supression flag is a temporary kludge.
8 -- While working on this module you are encouraged to remove it and
9 -- detab the module (please do the detabbing in a separate patch). See
10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
11 -- for details
12
13 module OptCoercion ( optCoercion, checkAxInstCo ) where 
14
15 #include "HsVersions.h"
16
17 import Coercion
18 import Type hiding( substTyVarBndr, substTy, extendTvSubst )
19 import TcType       ( exactTyVarsOfType )
20 import TyCon
21 import CoAxiom
22 import Var
23 import VarSet
24 import FamInstEnv   ( flattenTys )
25 import VarEnv
26 import StaticFlags      ( opt_NoOptCoercion )
27 import Outputable
28 import Pair
29 import Maybes
30 import FastString
31 import Util
32 import Unify
33 import ListSetOps
34 import InstEnv
35 \end{code}
36
37 %************************************************************************
38 %*                                                                      *
39                  Optimising coercions                                                                   
40 %*                                                                      *
41 %************************************************************************
42
43 Note [Subtle shadowing in coercions]
44 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
45 Supose we optimising a coercion
46     optCoercion (forall (co_X5:t1~t2). ...co_B1...)
47 The co_X5 is a wild-card; the bound variable of a coercion for-all
48 should never appear in the body of the forall. Indeed we often
49 write it like this
50     optCoercion ( (t1~t2) => ...co_B1... )
51
52 Just because it's a wild-card doesn't mean we are free to choose
53 whatever variable we like.  For example it'd be wrong for optCoercion
54 to return
55    forall (co_B1:t1~t2). ...co_B1...
56 because now the co_B1 (which is really free) has been captured, and
57 subsequent substitutions will go wrong.  That's why we can't use
58 mkCoPredTy in the ForAll case, where this note appears.  
59
60 \begin{code}
61 optCoercion :: CvSubst -> Coercion -> NormalCo
62 -- ^ optCoercion applies a substitution to a coercion, 
63 --   *and* optimises it to reduce its size
64 optCoercion env co 
65   | opt_NoOptCoercion = substCo env co
66   | otherwise         = opt_co env False Nothing co
67
68 type NormalCo = Coercion
69   -- Invariants: 
70   --  * The substitution has been fully applied
71   --  * For trans coercions (co1 `trans` co2)
72   --       co1 is not a trans, and neither co1 nor co2 is identity
73   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
74
75 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
76
77 opt_co, opt_co' :: CvSubst
78                 -> Bool        -- True <=> return (sym co)
79                 -> Maybe Role  -- Nothing <=> don't change; otherwise, change
80                                -- INVARIANT: the change is always a *downgrade*
81                 -> Coercion
82                 -> NormalCo     
83 opt_co = opt_co' 
84 {-
85 opt_co env sym co
86  = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
87    co1 `seq`
88    pprTrace "opt_co done }" (ppr co1) $
89    (WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (Pair s1 t1)
90                          $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
91     WARN( not (coreEqCoercion co1 simple_result),
92            (text "env=" <+> ppr env) $$
93            (text "input=" <+> ppr co) $$
94            (text "simple=" <+> ppr simple_result) $$
95            (text "opt=" <+> ppr co1) )
96    co1)
97  where
98    co1 = opt_co' env sym co
99    same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
100    Pair s t = coercionKind (substCo env co)
101    (s1,t1) | sym = (t,s)
102            | otherwise = (s,t)
103    Pair s2 t2 = coercionKind co1
104
105    simple_result | sym = mkSymCo (substCo env co)
106                  | otherwise = substCo env co
107 -}
108
109 opt_co' env _   mrole (Refl r ty) = Refl (mrole `orElse` r) (substTy env ty)
110 opt_co' env sym mrole co
111   |  mrole == Just Phantom 
112   || coercionRole co == Phantom
113   , Pair ty1 ty2 <- coercionKind co
114   = if sym
115     then opt_univ env Phantom ty2 ty1
116     else opt_univ env Phantom ty1 ty2
117
118 opt_co' env sym mrole (SymCo co)  = opt_co env (not sym) mrole co
119 opt_co' env sym mrole (TyConAppCo r tc cos)
120   = case mrole of
121       Nothing -> mkTyConAppCo r  tc (map (opt_co env sym Nothing) cos)
122       Just r' -> mkTyConAppCo r' tc (zipWith (opt_co env sym)
123                                              (map Just (tyConRolesX r' tc)) cos)
124 opt_co' env sym mrole (AppCo co1 co2) = mkAppCo (opt_co env sym mrole   co1)
125                                                 (opt_co env sym Nothing co2)
126 opt_co' env sym mrole (ForAllCo tv co)
127   = case substTyVarBndr env tv of
128       (env', tv') -> mkForAllCo tv' (opt_co env' sym mrole co)
129      -- Use the "mk" functions to check for nested Refls
130
131 opt_co' env sym mrole (CoVarCo cv)
132   | Just co <- lookupCoVar env cv
133   = opt_co (zapCvSubstEnv env) sym mrole co
134
135   | Just cv1 <- lookupInScope (getCvInScope env) cv
136   = ASSERT( isCoVar cv1 ) wrapRole mrole cv_role $ wrapSym sym (CoVarCo cv1)
137                 -- cv1 might have a substituted kind!
138
139   | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
140                 ASSERT( isCoVar cv )
141                 wrapRole mrole cv_role $ wrapSym sym (CoVarCo cv)
142   where cv_role = coVarRole cv
143
144 opt_co' env sym mrole (AxiomInstCo con ind cos)
145     -- Do *not* push sym inside top-level axioms
146     -- e.g. if g is a top-level axiom
147     --   g a : f a ~ a
148     -- then (sym (g ty)) /= g (sym ty) !!
149   = wrapRole mrole (coAxiomRole con) $
150     wrapSym sym $
151     AxiomInstCo con ind (map (opt_co env False Nothing) cos)
152       -- Note that the_co does *not* have sym pushed into it
153
154 opt_co' env sym mrole (UnivCo r oty1 oty2)
155   = opt_univ env role a b
156   where
157     (a,b) = if sym then (oty2,oty1) else (oty1,oty2)
158     role = mrole `orElse` r
159
160 opt_co' env sym mrole (TransCo co1 co2)
161   | sym       = opt_trans in_scope opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
162   | otherwise = opt_trans in_scope opt_co1 opt_co2
163   where
164     opt_co1 = opt_co env sym mrole co1
165     opt_co2 = opt_co env sym mrole co2
166     in_scope = getCvInScope env
167
168 -- NthCo roles are fiddly!
169 opt_co' env sym mrole (NthCo n (TyConAppCo _ _ cos))
170   = opt_co env sym mrole (getNth cos n)
171 opt_co' env sym mrole (NthCo n co)
172   | TyConAppCo _ _tc cos <- co'
173   , isDecomposableTyCon tc   -- Not synonym families
174   = ASSERT( n < length cos )
175     ASSERT( _tc == tc )
176     let resultCo = cos !! n
177         resultRole = coercionRole resultCo in
178     case (mrole, resultRole) of
179         -- if we just need an R coercion, try to propagate the SubCo again:
180       (Just Representational, Nominal) -> opt_co (zapCvSubstEnv env) False mrole resultCo
181       _                                -> resultCo
182
183   | otherwise
184   = wrap_role $ NthCo n co'
185
186   where
187     wrap_role wrapped = wrapRole mrole (coercionRole wrapped) wrapped
188
189     tc = tyConAppTyCon $ pFst $ coercionKind co
190     co' = opt_co env sym mrole' co
191     mrole' = case mrole of
192                Just Representational
193                  | Representational <- nthRole Representational tc n
194                  -> Just Representational
195                _ -> Nothing
196
197 opt_co' env sym mrole (LRCo lr co)
198   | Just pr_co <- splitAppCo_maybe co
199   = opt_co env sym mrole (pickLR lr pr_co)
200   | Just pr_co <- splitAppCo_maybe co'
201   = if mrole == Just Representational
202     then opt_co (zapCvSubstEnv env) False mrole (pickLR lr pr_co)
203     else pickLR lr pr_co
204   | otherwise
205   = wrapRole mrole Nominal $ LRCo lr co'
206   where
207     co' = opt_co env sym Nothing co
208
209 opt_co' env sym mrole (InstCo co ty)
210     -- See if the first arg is already a forall
211     -- ...then we can just extend the current substitution
212   | Just (tv, co_body) <- splitForAllCo_maybe co
213   = opt_co (extendTvSubst env tv ty') sym mrole co_body
214
215      -- See if it is a forall after optimization
216      -- If so, do an inefficient one-variable substitution
217   | Just (tv, co'_body) <- splitForAllCo_maybe co'
218   = substCoWithTy (getCvInScope env) tv ty' co'_body   
219
220   | otherwise = InstCo co' ty'
221   where
222     co' = opt_co env sym mrole co
223     ty' = substTy env ty
224
225 opt_co' env sym _ (SubCo co) = opt_co env sym (Just Representational) co
226
227 -------------
228 opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
229 opt_univ env role oty1 oty2
230   | Just (tc1, tys1) <- splitTyConApp_maybe oty1
231   , Just (tc2, tys2) <- splitTyConApp_maybe oty2
232   , tc1 == tc2
233   = mkTyConAppCo role tc1 (zipWith3 (opt_univ env) (tyConRolesX role tc1) tys1 tys2)
234
235   | Just (l1, r1) <- splitAppTy_maybe oty1
236   , Just (l2, r2) <- splitAppTy_maybe oty2
237   , typeKind l1 `eqType` typeKind l2   -- kind(r1) == kind(r2) by consequence
238   = let role' = if role == Phantom then Phantom else Nominal in
239        -- role' is to comform to mkAppCo's precondition
240     mkAppCo (opt_univ env role l1 l2) (opt_univ env role' r1 r2)
241
242   | Just (tv1, ty1) <- splitForAllTy_maybe oty1
243   , Just (tv2, ty2) <- splitForAllTy_maybe oty2
244   , tyVarKind tv1 `eqType` tyVarKind tv2  -- rule out a weird unsafeCo
245   = case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
246     let ty1' = substTy env1 ty1
247         ty2' = substTy env2 ty2 in
248     mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) role ty1' ty2') }
249
250   | otherwise
251   = mkUnivCo role (substTy env oty1) (substTy env oty2)
252
253 -------------
254 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
255 opt_transList is = zipWith (opt_trans is)
256
257 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
258 opt_trans is co1 co2
259   | isReflCo co1 = co2
260   | otherwise    = opt_trans1 is co1 co2
261
262 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
263 -- First arg is not the identity
264 opt_trans1 is co1 co2
265   | isReflCo co2 = co1
266   | otherwise    = opt_trans2 is co1 co2
267
268 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
269 -- Neither arg is the identity
270 opt_trans2 is (TransCo co1a co1b) co2
271     -- Don't know whether the sub-coercions are the identity
272   = opt_trans is co1a (opt_trans is co1b co2)  
273
274 opt_trans2 is co1 co2 
275   | Just co <- opt_trans_rule is co1 co2
276   = co
277
278 opt_trans2 is co1 (TransCo co2a co2b)
279   | Just co1_2a <- opt_trans_rule is co1 co2a
280   = if isReflCo co1_2a
281     then co2b
282     else opt_trans1 is co1_2a co2b
283
284 opt_trans2 _ co1 co2
285   = mkTransCo co1 co2
286
287 ------
288 -- Optimize coercions with a top-level use of transitivity.
289 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
290
291 -- Push transitivity through matching destructors
292 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
293   | d1 == d2
294   , co1 `compatible_co` co2
295   = fireTransRule "PushNth" in_co1 in_co2 $
296     mkNthCo d1 (opt_trans is co1 co2)
297
298 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
299   | d1 == d2
300   , co1 `compatible_co` co2
301   = fireTransRule "PushLR" in_co1 in_co2 $
302     mkLRCo d1 (opt_trans is co1 co2)
303
304 -- Push transitivity inside instantiation
305 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
306   | ty1 `eqType` ty2
307   , co1 `compatible_co` co2
308   = fireTransRule "TrPushInst" in_co1 in_co2 $
309     mkInstCo (opt_trans is co1 co2) ty1
310  
311 -- Push transitivity down through matching top-level constructors.
312 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
313   | tc1 == tc2 
314   = ASSERT( r1 == r2 )
315     fireTransRule "PushTyConApp" in_co1 in_co2 $
316     TyConAppCo r1 tc1 (opt_transList is cos1 cos2)
317
318 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
319   = fireTransRule "TrPushApp" in_co1 in_co2 $
320     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
321
322 -- Eta rules
323 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
324   | Just cos2 <- etaTyConAppCo_maybe tc co2
325   = ASSERT( length cos1 == length cos2 )
326     fireTransRule "EtaCompL" co1 co2 $
327     TyConAppCo r tc (opt_transList is cos1 cos2)
328
329 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
330   | Just cos1 <- etaTyConAppCo_maybe tc co1
331   = ASSERT( length cos1 == length cos2 )
332     fireTransRule "EtaCompR" co1 co2 $
333     TyConAppCo r tc (opt_transList is cos1 cos2)
334
335 opt_trans_rule is co1@(AppCo co1a co1b) co2
336   | Just (co2a,co2b) <- etaAppCo_maybe co2
337   = fireTransRule "EtaAppL" co1 co2 $
338     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
339
340 opt_trans_rule is co1 co2@(AppCo co2a co2b)
341   | Just (co1a,co1b) <- etaAppCo_maybe co1
342   = fireTransRule "EtaAppR" co1 co2 $
343     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
344
345 -- Push transitivity inside forall
346 opt_trans_rule is co1 co2
347   | Just (tv1,r1) <- splitForAllCo_maybe co1
348   , Just (tv2,r2) <- etaForAllCo_maybe co2
349   , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
350         is' = is `extendInScopeSet` tv1
351   = fireTransRule "EtaAllL" co1 co2 $
352     mkForAllCo tv1 (opt_trans2 is' r1 r2')
353
354   | Just (tv2,r2) <- splitForAllCo_maybe co2
355   , Just (tv1,r1) <- etaForAllCo_maybe co1
356   , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
357         is' = is `extendInScopeSet` tv2
358   = fireTransRule "EtaAllR" co1 co2 $
359     mkForAllCo tv1 (opt_trans2 is' r1' r2)
360
361 -- Push transitivity inside axioms
362 opt_trans_rule is co1 co2
363
364   -- TrPushSymAxR
365   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
366   , Just cos2 <- matchAxiom sym con ind co2
367   , True <- sym
368   , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
369   , Nothing <- checkAxInstCo newAxInst
370   = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
371
372   -- TrPushAxR
373   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
374   , Just cos2 <- matchAxiom sym con ind co2
375   , False <- sym
376   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
377   , Nothing <- checkAxInstCo newAxInst
378   = fireTransRule "TrPushAxR" co1 co2 newAxInst
379
380   -- TrPushSymAxL
381   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
382   , Just cos1 <- matchAxiom (not sym) con ind co1
383   , True <- sym
384   , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
385   , Nothing <- checkAxInstCo newAxInst
386   = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
387
388   -- TrPushAxL  
389   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
390   , Just cos1 <- matchAxiom (not sym) con ind co1
391   , False <- sym
392   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
393   , Nothing <- checkAxInstCo newAxInst
394   = fireTransRule "TrPushAxL" co1 co2 newAxInst
395
396   -- TrPushAxSym/TrPushSymAx
397   | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
398   , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
399   , con1 == con2
400   , ind1 == ind2
401   , sym1 == not sym2
402   , let branch = coAxiomNthBranch con1 ind1
403         qtvs = coAxBranchTyVars branch
404         lhs  = coAxNthLHS con1 ind1
405         rhs  = coAxBranchRHS branch
406         pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
407   , all (`elemVarSet` pivot_tvs) qtvs
408   = fireTransRule "TrPushAxSym" co1 co2 $
409     if sym2
410     then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
411     else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
412   where
413     co1_is_axiom_maybe = isAxiom_maybe co1
414     co2_is_axiom_maybe = isAxiom_maybe co2
415     role = coercionRole co1 -- should be the same as coercionRole co2!
416
417 opt_trans_rule _ co1 co2        -- Identity rule
418   | Pair ty1 _ <- coercionKind co1
419   , Pair _ ty2 <- coercionKind co2
420   , ty1 `eqType` ty2
421   = fireTransRule "RedTypeDirRefl" co1 co2 $
422     Refl (coercionRole co1) ty2
423
424 opt_trans_rule _ _ _ = Nothing
425
426 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
427 fireTransRule _rule _co1 _co2 res
428   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
429     Just res
430
431 \end{code}
432
433 Note [Conflict checking with AxiomInstCo]
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
435 Consider the following type family and axiom:
436
437 type family Equal (a :: k) (b :: k) :: Bool
438 type instance where
439   Equal a a = True
440   Equal a b = False
441 --
442 Equal :: forall k::BOX. k -> k -> Bool
443 axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
444            ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
445
446 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is 0-based,
447 so this is the second branch of the axiom.) The problem is that, on the surface, it
448 seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) and that all is
449 OK. But, all is not OK: we want to use the first branch of the axiom in this case,
450 not the second. The problem is that the parameters of the first branch can unify with
451 the supplied coercions, thus meaning that the first branch should be taken. See also
452 Note [Branched instance checking] in types/FamInstEnv.lhs.
453
454 \begin{code}
455 -- | Check to make sure that an AxInstCo is internally consistent.
456 -- Returns the conflicting branch, if it exists
457 -- See Note [Conflict checking with AxiomInstCo]
458 checkAxInstCo :: Coercion -> Maybe CoAxBranch
459 -- defined here to avoid dependencies in Coercion
460 -- If you edit this function, you may need to update the GHC formalism
461 -- See Note [GHC Formalism] in CoreLint
462 checkAxInstCo (AxiomInstCo ax ind cos)
463   = let branch = coAxiomNthBranch ax ind
464         tvs = coAxBranchTyVars branch
465         incomps = coAxBranchIncomps branch
466         tys = map (pFst . coercionKind) cos 
467         subst = zipOpenTvSubst tvs tys
468         target = Type.substTys subst (coAxBranchLHS branch)
469         in_scope = mkInScopeSet $
470                    unionVarSets (map (tyVarsOfTypes . coAxBranchLHS) incomps)
471         flattened_target = flattenTys in_scope target in
472     check_no_conflict flattened_target incomps
473   where
474     check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
475     check_no_conflict _    [] = Nothing
476     check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
477          -- See Note [Apartness] in FamInstEnv
478       | SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
479       = check_no_conflict flat rest
480       | otherwise
481       = Just b
482 checkAxInstCo _ = Nothing
483
484 -----------
485 wrapSym :: Bool -> Coercion -> Coercion
486 wrapSym sym co | sym       = SymCo co
487                | otherwise = co
488
489 wrapRole :: Maybe Role   -- desired
490          -> Role         -- current
491          -> Coercion -> Coercion
492 wrapRole Nothing        _       = id
493 wrapRole (Just desired) current = maybeSubCo2 desired current
494
495 -----------
496 -- takes two tyvars and builds env'ts to map them to the same tyvar
497 substTyVarBndr2 :: CvSubst -> TyVar -> TyVar
498                 -> (CvSubst, CvSubst, TyVar)
499 substTyVarBndr2 env tv1 tv2
500   = case substTyVarBndr env tv1 of
501       (env1, tv1') -> (env1, extendTvSubstAndInScope env tv2 (mkTyVarTy tv1'), tv1')
502     
503 zapCvSubstEnv2 :: CvSubst -> CvSubst -> CvSubst
504 zapCvSubstEnv2 env1 env2 = mkCvSubst (is1 `unionInScope` is2) []
505   where is1 = getCvInScope env1
506         is2 = getCvInScope env2
507 -----------
508 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
509 isAxiom_maybe (SymCo co) 
510   | Just (sym, con, ind, cos) <- isAxiom_maybe co
511   = Just (not sym, con, ind, cos)
512 isAxiom_maybe (AxiomInstCo con ind cos)
513   = Just (False, con, ind, cos)
514 isAxiom_maybe _ = Nothing
515
516 matchAxiom :: Bool -- True = match LHS, False = match RHS
517            -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
518 -- If we succeed in matching, then *all the quantified type variables are bound*
519 -- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
520 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
521   = let (CoAxBranch { cab_tvs   = qtvs
522                     , cab_roles = roles
523                     , cab_lhs   = lhs
524                     , cab_rhs   = rhs }) = coAxiomNthBranch ax ind in
525     case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
526       Nothing    -> Nothing
527       Just subst -> allMaybes (zipWith (liftCoSubstTyVar subst) roles qtvs)
528
529 -------------
530 compatible_co :: Coercion -> Coercion -> Bool
531 -- Check whether (co1 . co2) will be well-kinded
532 compatible_co co1 co2
533   = x1 `eqType` x2              
534   where
535     Pair _ x1 = coercionKind co1
536     Pair x2 _ = coercionKind co2
537
538 -------------
539 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
540 -- Try to make the coercion be of form (forall tv. co)
541 etaForAllCo_maybe co
542   | Just (tv, r) <- splitForAllCo_maybe co
543   = Just (tv, r)
544
545   | Pair ty1 ty2  <- coercionKind co
546   , Just (tv1, _) <- splitForAllTy_maybe ty1
547   , Just (tv2, _) <- splitForAllTy_maybe ty2
548   , tyVarKind tv1 `eqKind` tyVarKind tv2
549   = Just (tv1, mkInstCo co (mkTyVarTy tv1))
550
551   | otherwise
552   = Nothing
553
554 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
555 -- If possible, split a coercion
556 --   g :: t1a t1b ~ t2a t2b
557 -- into a pair of coercions (left g, right g)
558 etaAppCo_maybe co
559   | Just (co1,co2) <- splitAppCo_maybe co
560   = Just (co1,co2)
561   | Nominal <- coercionRole co
562   , Pair ty1 ty2 <- coercionKind co
563   , Just (_,t1) <- splitAppTy_maybe ty1
564   , Just (_,t2) <- splitAppTy_maybe ty2
565   , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
566   = Just (LRCo CLeft co, LRCo CRight co)
567   | otherwise
568   = Nothing
569
570 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
571 -- If possible, split a coercion 
572 --       g :: T s1 .. sn ~ T t1 .. tn
573 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 
574 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
575   = ASSERT( tc == tc2 ) Just cos2
576
577 etaTyConAppCo_maybe tc co
578   | isDecomposableTyCon tc
579   , Pair ty1 ty2     <- coercionKind co
580   , Just (tc1, tys1) <- splitTyConApp_maybe ty1
581   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
582   , tc1 == tc2
583   , let n = length tys1
584   = ASSERT( tc == tc1 ) 
585     ASSERT( n == length tys2 )
586     Just (decomposeCo n co)
587     -- NB: n might be <> tyConArity tc
588     -- e.g.   data family T a :: * -> *
589     --        g :: T a b ~ T c d
590
591   | otherwise
592   = Nothing
593 \end{code}  
594
595 Note [Eta for AppCo]
596 ~~~~~~~~~~~~~~~~~~~~
597 Suppose we have 
598    g :: s1 t1 ~ s2 t2
599
600 Then we can't necessarily make
601    left  g :: s1 ~ s2
602    right g :: t1 ~ t2
603 because it's possible that
604    s1 :: * -> *         t1 :: *
605    s2 :: (*->*) -> *    t2 :: * -> *
606 and in that case (left g) does not have the same
607 kind on either side.
608
609 It's enough to check that 
610   kind t1 = kind t2
611 because if g is well-kinded then
612   kind (s1 t2) = kind (s2 t2)
613 and these two imply
614   kind s1 = kind s2
615