Implement overlapping type family instances.
[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 ) 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 VarEnv
25 import StaticFlags      ( opt_NoOptCoercion )
26 import Outputable
27 import Pair
28 import Maybes( allMaybes )
29 import FastString
30 import Util
31 \end{code}
32
33 %************************************************************************
34 %*                                                                      *
35                  Optimising coercions                                                                   
36 %*                                                                      *
37 %************************************************************************
38
39 Note [Subtle shadowing in coercions]
40 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
41 Supose we optimising a coercion
42     optCoercion (forall (co_X5:t1~t2). ...co_B1...)
43 The co_X5 is a wild-card; the bound variable of a coercion for-all
44 should never appear in the body of the forall. Indeed we often
45 write it like this
46     optCoercion ( (t1~t2) => ...co_B1... )
47
48 Just because it's a wild-card doesn't mean we are free to choose
49 whatever variable we like.  For example it'd be wrong for optCoercion
50 to return
51    forall (co_B1:t1~t2). ...co_B1...
52 because now the co_B1 (which is really free) has been captured, and
53 subsequent substitutions will go wrong.  That's why we can't use
54 mkCoPredTy in the ForAll case, where this note appears.  
55
56 \begin{code}
57 optCoercion :: CvSubst -> Coercion -> NormalCo
58 -- ^ optCoercion applies a substitution to a coercion, 
59 --   *and* optimises it to reduce its size
60 optCoercion env co 
61   | opt_NoOptCoercion = substCo env co
62   | otherwise         = opt_co env False co
63
64 type NormalCo = Coercion
65   -- Invariants: 
66   --  * The substitution has been fully applied
67   --  * For trans coercions (co1 `trans` co2)
68   --       co1 is not a trans, and neither co1 nor co2 is identity
69   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
70
71 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
72
73 opt_co, opt_co' :: CvSubst
74                 -> Bool        -- True <=> return (sym co)
75                 -> Coercion
76                 -> NormalCo     
77 opt_co = opt_co'
78 {-
79 opt_co env sym co
80  = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
81    co1 `seq`
82    pprTrace "opt_co done }" (ppr co1) $
83    (WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (Pair s1 t1)
84                          $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
85     WARN( not (coreEqCoercion co1 simple_result),
86            (text "env=" <+> ppr env) $$
87            (text "input=" <+> ppr co) $$
88            (text "simple=" <+> ppr simple_result) $$
89            (text "opt=" <+> ppr co1) )
90    co1)
91  where
92    co1 = opt_co' env sym co
93    same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
94    Pair s t = coercionKind (substCo env co)
95    (s1,t1) | sym = (t,s)
96            | otherwise = (s,t)
97    Pair s2 t2 = coercionKind co1
98
99    simple_result | sym = mkSymCo (substCo env co)
100                  | otherwise = substCo env co
101 -}
102
103 opt_co' env _   (Refl ty)           = Refl (substTy env ty)
104 opt_co' env sym (SymCo co)          = opt_co env (not sym) co
105 opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)
106 opt_co' env sym (AppCo co1 co2)     = mkAppCo (opt_co env sym co1) (opt_co env sym co2)
107 opt_co' env sym (ForAllCo tv co)    = case substTyVarBndr env tv of
108                                          (env', tv') -> mkForAllCo tv' (opt_co env' sym co)
109      -- Use the "mk" functions to check for nested Refls
110
111 opt_co' env sym (CoVarCo cv)
112   | Just co <- lookupCoVar env cv
113   = opt_co (zapCvSubstEnv env) sym co
114
115   | Just cv1 <- lookupInScope (getCvInScope env) cv
116   = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)
117                 -- cv1 might have a substituted kind!
118
119   | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
120                 ASSERT( isCoVar cv )
121                 wrapSym sym (CoVarCo cv)
122
123 opt_co' env sym (AxiomInstCo con ind cos)
124     -- Do *not* push sym inside top-level axioms
125     -- e.g. if g is a top-level axiom
126     --   g a : f a ~ a
127     -- then (sym (g ty)) /= g (sym ty) !!
128   = wrapSym sym $ AxiomInstCo con ind (map (opt_co env False) cos)
129       -- Note that the_co does *not* have sym pushed into it
130
131 opt_co' env sym (UnsafeCo ty1 ty2)
132   | ty1' `eqType` ty2' = Refl ty1'
133   | sym                = mkUnsafeCo ty2' ty1'
134   | otherwise          = mkUnsafeCo ty1' ty2'
135   where
136     ty1' = substTy env ty1
137     ty2' = substTy env ty2
138
139 opt_co' env sym (TransCo co1 co2)
140   | sym       = opt_trans in_scope opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
141   | otherwise = opt_trans in_scope opt_co1 opt_co2
142   where
143     opt_co1 = opt_co env sym co1
144     opt_co2 = opt_co env sym co2
145     in_scope = getCvInScope env
146
147 opt_co' env sym (NthCo n co)
148   | TyConAppCo tc cos <- co'
149   , isDecomposableTyCon tc   -- Not synonym families
150   = ASSERT( n < length cos )
151     cos !! n
152   | otherwise
153   = NthCo n co'
154   where
155     co' = opt_co env sym co
156
157 opt_co' env sym (LRCo lr co)
158   | Just pr_co <- splitAppCo_maybe co'
159   = pickLR lr pr_co
160   | otherwise
161   = LRCo lr co'
162   where
163     co' = opt_co env sym co
164
165 opt_co' env sym (InstCo co ty)
166     -- See if the first arg is already a forall
167     -- ...then we can just extend the current substitution
168   | Just (tv, co_body) <- splitForAllCo_maybe co
169   = opt_co (extendTvSubst env tv ty') sym co_body
170
171      -- See if it is a forall after optimization
172      -- If so, do an inefficient one-variable substitution
173   | Just (tv, co'_body) <- splitForAllCo_maybe co'
174   = substCoWithTy (getCvInScope env) tv ty' co'_body   
175
176   | otherwise = InstCo co' ty'
177   where
178     co' = opt_co env sym co
179     ty' = substTy env ty
180
181 -------------
182 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
183 opt_transList is = zipWith (opt_trans is)
184
185 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
186 opt_trans is co1 co2
187   | isReflCo co1 = co2
188   | otherwise    = opt_trans1 is co1 co2
189
190 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
191 -- First arg is not the identity
192 opt_trans1 is co1 co2
193   | isReflCo co2 = co1
194   | otherwise    = opt_trans2 is co1 co2
195
196 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
197 -- Neither arg is the identity
198 opt_trans2 is (TransCo co1a co1b) co2
199     -- Don't know whether the sub-coercions are the identity
200   = opt_trans is co1a (opt_trans is co1b co2)  
201
202 opt_trans2 is co1 co2 
203   | Just co <- opt_trans_rule is co1 co2
204   = co
205
206 opt_trans2 is co1 (TransCo co2a co2b)
207   | Just co1_2a <- opt_trans_rule is co1 co2a
208   = if isReflCo co1_2a
209     then co2b
210     else opt_trans1 is co1_2a co2b
211
212 opt_trans2 _ co1 co2
213   = mkTransCo co1 co2
214
215 ------
216 -- Optimize coercions with a top-level use of transitivity.
217 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
218
219 -- Push transitivity through matching destructors
220 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
221   | d1 == d2
222   , co1 `compatible_co` co2
223   = fireTransRule "PushNth" in_co1 in_co2 $
224     mkNthCo d1 (opt_trans is co1 co2)
225
226 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
227   | d1 == d2
228   , co1 `compatible_co` co2
229   = fireTransRule "PushLR" in_co1 in_co2 $
230     mkLRCo d1 (opt_trans is co1 co2)
231
232 -- Push transitivity inside instantiation
233 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
234   | ty1 `eqType` ty2
235   , co1 `compatible_co` co2
236   = fireTransRule "TrPushInst" in_co1 in_co2 $
237     mkInstCo (opt_trans is co1 co2) ty1
238  
239 -- Push transitivity down through matching top-level constructors.
240 opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
241   | tc1 == tc2 
242   = fireTransRule "PushTyConApp" in_co1 in_co2 $
243     TyConAppCo tc1 (opt_transList is cos1 cos2)
244
245 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
246   = fireTransRule "TrPushApp" in_co1 in_co2 $
247     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
248
249 -- Eta rules
250 opt_trans_rule is co1@(TyConAppCo tc cos1) co2
251   | Just cos2 <- etaTyConAppCo_maybe tc co2
252   = ASSERT( length cos1 == length cos2 )
253     fireTransRule "EtaCompL" co1 co2 $
254     TyConAppCo tc (opt_transList is cos1 cos2)
255
256 opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
257   | Just cos1 <- etaTyConAppCo_maybe tc co1
258   = ASSERT( length cos1 == length cos2 )
259     fireTransRule "EtaCompR" co1 co2 $
260     TyConAppCo tc (opt_transList is cos1 cos2)
261
262 opt_trans_rule is co1@(AppCo co1a co1b) co2
263   | Just (co2a,co2b) <- etaAppCo_maybe co2
264   = fireTransRule "EtaAppL" co1 co2 $
265     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
266
267 opt_trans_rule is co1 co2@(AppCo co2a co2b)
268   | Just (co1a,co1b) <- etaAppCo_maybe co1
269   = fireTransRule "EtaAppR" co1 co2 $
270     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
271
272 -- Push transitivity inside forall
273 opt_trans_rule is co1 co2
274   | Just (tv1,r1) <- splitForAllCo_maybe co1
275   , Just (tv2,r2) <- etaForAllCo_maybe co2
276   , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
277         is' = is `extendInScopeSet` tv1
278   = fireTransRule "EtaAllL" co1 co2 $
279     mkForAllCo tv1 (opt_trans2 is' r1 r2')
280
281   | Just (tv2,r2) <- splitForAllCo_maybe co2
282   , Just (tv1,r1) <- etaForAllCo_maybe co1
283   , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
284         is' = is `extendInScopeSet` tv2
285   = fireTransRule "EtaAllR" co1 co2 $
286     mkForAllCo tv1 (opt_trans2 is' r1' r2)
287
288 -- Push transitivity inside axioms
289 opt_trans_rule is co1 co2
290
291   -- TrPushAxR/TrPushSymAxR
292   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
293   , Just cos2 <- matchAxiom sym con ind co2
294   = fireTransRule "TrPushAxR" co1 co2 $
295     if sym 
296     then SymCo $ AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
297     else         AxiomInstCo con ind (opt_transList is cos1 cos2)
298
299   -- TrPushAxL/TrPushSymAxL
300   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
301   , Just cos1 <- matchAxiom (not sym) con ind co1
302   = fireTransRule "TrPushAxL" co1 co2 $
303     if sym 
304     then SymCo $ AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
305     else         AxiomInstCo con ind (opt_transList is cos1 cos2)
306
307   -- TrPushAxSym/TrPushSymAx
308   | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
309   , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
310   , con1 == con2
311   , ind1 == ind2
312   , sym1 == not sym2
313   , let branch = coAxiomNthBranch con1 ind1
314         qtvs = coAxBranchTyVars branch
315         lhs  = coAxNthLHS con1 ind1
316         rhs  = coAxBranchRHS branch
317         pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
318   , all (`elemVarSet` pivot_tvs) qtvs
319   = fireTransRule "TrPushAxSym" co1 co2 $
320     if sym2
321     then liftCoSubstWith qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
322     else liftCoSubstWith qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
323   where
324     co1_is_axiom_maybe = isAxiom_maybe co1
325     co2_is_axiom_maybe = isAxiom_maybe co2
326
327 opt_trans_rule _ co1 co2        -- Identity rule
328   | Pair ty1 _ <- coercionKind co1
329   , Pair _ ty2 <- coercionKind co2
330   , ty1 `eqType` ty2
331   = fireTransRule "RedTypeDirRefl" co1 co2 $
332     Refl ty2
333
334 opt_trans_rule _ _ _ = Nothing
335
336 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
337 fireTransRule _rule _co1 _co2 res
338   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
339     Just res
340
341 -----------
342 wrapSym :: Bool -> Coercion -> Coercion
343 wrapSym sym co | sym       = SymCo co
344                | otherwise = co
345
346 -----------
347 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
348 isAxiom_maybe (SymCo co) 
349   | Just (sym, con, ind, cos) <- isAxiom_maybe co
350   = Just (not sym, con, ind, cos)
351 isAxiom_maybe (AxiomInstCo con ind cos)
352   = Just (False, con, ind, cos)
353 isAxiom_maybe _ = Nothing
354
355 matchAxiom :: Bool -- True = match LHS, False = match RHS
356            -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
357 -- If we succeed in matching, then *all the quantified type variables are bound*
358 -- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
359 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
360   = let (CoAxBranch { cab_tvs = qtvs
361                     , cab_lhs = lhs
362                     , cab_rhs = rhs }) = coAxiomNthBranch ax ind in
363     case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
364       Nothing    -> Nothing
365       Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
366
367 -------------
368 compatible_co :: Coercion -> Coercion -> Bool
369 -- Check whether (co1 . co2) will be well-kinded
370 compatible_co co1 co2
371   = x1 `eqType` x2              
372   where
373     Pair _ x1 = coercionKind co1
374     Pair x2 _ = coercionKind co2
375
376 -------------
377 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
378 -- Try to make the coercion be of form (forall tv. co)
379 etaForAllCo_maybe co
380   | Just (tv, r) <- splitForAllCo_maybe co
381   = Just (tv, r)
382
383   | Pair ty1 ty2  <- coercionKind co
384   , Just (tv1, _) <- splitForAllTy_maybe ty1
385   , Just (tv2, _) <- splitForAllTy_maybe ty2
386   , tyVarKind tv1 `eqKind` tyVarKind tv2
387   = Just (tv1, mkInstCo co (mkTyVarTy tv1))
388
389   | otherwise
390   = Nothing
391
392 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
393 -- If possible, split a coercion
394 --   g :: t1a t1b ~ t2a t2b
395 -- into a pair of coercions (left g, right g)
396 etaAppCo_maybe co
397   | Just (co1,co2) <- splitAppCo_maybe co
398   = Just (co1,co2)
399   | Pair ty1 ty2 <- coercionKind co
400   , Just (_,t1) <- splitAppTy_maybe ty1
401   , Just (_,t2) <- splitAppTy_maybe ty2
402   , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
403   = Just (LRCo CLeft co, LRCo CRight co)
404   | otherwise
405   = Nothing
406
407 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
408 -- If possible, split a coercion 
409 --       g :: T s1 .. sn ~ T t1 .. tn
410 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 
411 etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)
412   = ASSERT( tc == tc2 ) Just cos2
413
414 etaTyConAppCo_maybe tc co
415   | isDecomposableTyCon tc
416   , Pair ty1 ty2     <- coercionKind co
417   , Just (tc1, tys1) <- splitTyConApp_maybe ty1
418   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
419   , tc1 == tc2
420   , let n = length tys1
421   = ASSERT( tc == tc1 ) 
422     ASSERT( n == length tys2 )
423     Just (decomposeCo n co)  
424     -- NB: n might be <> tyConArity tc
425     -- e.g.   data family T a :: * -> *
426     --        g :: T a b ~ T c d
427
428   | otherwise
429   = Nothing
430 \end{code}  
431
432 Note [Eta for AppCo]
433 ~~~~~~~~~~~~~~~~~~~~
434 Supopse we have 
435    g :: s1 t1 ~ s2 t2
436
437 Then we can't necessarily make
438    left  g :: s1 ~ s2
439    right g :: t1 ~ t2
440 becuase it's poossible that
441    s1 :: * -> *         t1 :: *
442    s2 :: (*->*) -> *    t2 :: * -> *
443 and in that case (left g) does not have the same
444 kind on either side.
445
446 It's enough to check that 
447   kind t1 = kind t2
448 because if g is well-kinded then
449   kind (s1 t2) = kind (s2 t2)
450 and these two imply
451   kind s1 = kind s2
452