compiler/types/OptCoercion.lhs

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