compiler/types/OptCoercion.lhs

   1 %\r
   2 % (c) The University of Glasgow 2006\r
   3 %\r
   4 \r
   5 \begin{code}\r
   6 {-# OPTIONS_GHC -w #-}\r
   7 module OptCoercion (\r
   8         optCoercion\r
   9    ) where \r
  10 \r
  11 #include "HsVersions.h"\r
  12 \r
  13 import Unify    ( tcMatchTy )\r
  14 import Coercion\r
  15 import Type\r
  16 import TypeRep\r
  17 import TyCon\r
  18 import Var\r
  19 import VarSet\r
  20 import PrelNames\r
  21 import Util\r
  22 import Outputable\r
  23 \end{code}\r
  24 \r
  25 %************************************************************************\r
  26 %*                                                                      *\r
  27                  Optimising coercions                                                                   \r
  28 %*                                                                      *\r
  29 %************************************************************************\r
  30 \r
  31 \begin{code}\r
  32 optCoercion :: TvSubst -> Coercion -> NormalCo\r
  33 -- ^ optCoercion applies a substitution to a coercion, \r
  34 --   *and* optimises it to reduce its size\r
  35 optCoercion env co = opt_co env False co\r
  36 \r
  37 type NormalCo = Coercion\r
  38   -- Invariants: \r
  39   --  * The substitution has been fully applied\r
  40   --  * For trans coercions (co1 `trans` co2)\r
  41   --       co1 is not a trans, and neither co1 nor co2 is identity\r
  42   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)\r
  43 \r
  44 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity\r
  45 \r
  46 opt_co, opt_co' :: TvSubst\r
  47                 -> Bool        -- True <=> return (sym co)\r
  48                 -> Coercion\r
  49                 -> NormalCo     \r
  50 opt_co = opt_co'\r
  51 -- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
  52 --                      co1 `seq` \r
  53 --                pprTrace "opt_co done }" (ppr co1) \r
  54 --               WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (s1,t1) \r
  55 --                                     $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
  56 --                co1\r
  57 --  where\r
  58 --    co1 = opt_co' sym co\r
  59 --    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
  60 --    (s,t) = coercionKind co\r
  61 --    (s1,t1) | sym = (t,s)\r
  62 --            | otherwise = (s,t)\r
  63 --    (s2,t2) = coercionKind co1\r
  64 \r
  65 opt_co' env sym (AppTy ty1 ty2)           = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)\r
  66 opt_co' env sym (FunTy ty1 ty2)           = FunTy (opt_co env sym ty1) (opt_co env sym ty2)\r
  67 opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))\r
  68 opt_co' env sym (PredTy (IParam n ty))    = PredTy (IParam n (opt_co env sym ty))\r
  69 opt_co' _   _   co@(PredTy (EqPred {}))   = pprPanic "optCoercion" (ppr co)\r
  70 \r
  71 opt_co' env sym co@(TyVarTy tv)\r
  72   | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty\r
  73   | not (isCoVar tv)     = co   -- Identity; does not mention a CoVar\r
  74   | ty1 `coreEqType` ty2 = ty1  -- Identity; ..ditto..\r
  75   | not sym              = co\r
  76   | otherwise            = mkSymCoercion co\r
  77   where\r
  78     (ty1,ty2) = coVarKind tv\r
  79 \r
  80 opt_co' env sym (ForAllTy tv cor) \r
  81   | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)\r
  82   | otherwise  = case substTyVarBndr env tv of\r
  83                    (env', tv') -> ForAllTy tv' (opt_co env' sym cor)\r
  84   where\r
  85     (co1,co2) = coVarKind tv\r
  86 \r
  87 opt_co' env sym (TyConApp tc cos)\r
  88   | Just (arity, desc) <- isCoercionTyCon_maybe tc\r
  89   = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))\r
  90              (map (opt_co env sym) (drop arity cos))\r
  91   | otherwise\r
  92   = TyConApp tc (map (opt_co env sym) cos)\r
  93 \r
  94 --------\r
  95 opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
  96 -- Used for CoercionTyCons only\r
  97 -- Arguments are *not* already simplified/substituted\r
  98 opt_co_tc_app env sym tc desc cos\r
  99   = case desc of\r
 100       CoAxiom {} -- Do *not* push sym inside top-level axioms\r
 101                  -- e.g. if g is a top-level axiom\r
 102                  --   g a : F a ~ a\r
 103                  -- Then (sym (g ty)) /= g (sym ty) !!\r
 104         | sym       -> mkSymCoercion the_co  \r
 105         | otherwise -> the_co\r
 106         where\r
 107            the_co = TyConApp tc (map (opt_co env False) cos)\r
 108            -- Note that the_co does *not* have sym pushed into it\r
 109     \r
 110       CoTrans \r
 111         | sym       -> opt_trans opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g\r
 112         | otherwise -> opt_trans opt_co1 opt_co2\r
 113 \r
 114       CoUnsafe\r
 115         | sym       -> mkUnsafeCoercion ty2' ty1'\r
 116         | otherwise -> mkUnsafeCoercion ty1' ty2'\r
 117 \r
 118       CoSym   -> opt_co env (not sym) co1\r
 119       CoLeft  -> opt_lr fst\r
 120       CoRight -> opt_lr snd\r
 121       CoCsel1 -> opt_csel fstOf3\r
 122       CoCsel2 -> opt_csel sndOf3\r
 123       CoCselR -> opt_csel thirdOf3\r
 124 \r
 125       CoInst        -- See if the first arg is already a forall\r
 126                     -- ...then we can just extend the current substitution\r
 127         | Just (tv, co1_body) <- splitForAllTy_maybe co1\r
 128         -> opt_co (extendTvSubst env tv ty2') sym co1_body\r
 129 \r
 130                     -- See if is *now* a forall\r
 131         | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
 132         -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
 133 \r
 134         | otherwise\r
 135         -> TyConApp tc [opt_co1, ty2']\r
 136 \r
 137   where\r
 138     (co1 : cos1) = cos\r
 139     (co2 : _)    = cos1\r
 140 \r
 141     ty1' = substTy env co1\r
 142     ty2' = substTy env co2\r
 143 \r
 144         -- These opt_cos have the sym pushed into them\r
 145     opt_co1 = opt_co env sym co1\r
 146     opt_co2 = opt_co env sym co2\r
 147 \r
 148     the_unary_opt_co = TyConApp tc [opt_co1]\r
 149 \r
 150     opt_lr   sel = case splitAppTy_maybe opt_co1 of\r
 151                      Nothing -> the_unary_opt_co \r
 152                      Just lr -> sel lr\r
 153     opt_csel sel = case splitCoPredTy_maybe opt_co1 of\r
 154                      Nothing -> the_unary_opt_co \r
 155                      Just lr -> sel lr\r
 156 \r
 157 -------------\r
 158 opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
 159 opt_transL = zipWith opt_trans\r
 160 \r
 161 opt_trans :: NormalCo -> NormalCo -> NormalCo\r
 162 opt_trans co1 co2\r
 163   | isIdNormCo co1 = co2\r
 164   | otherwise      = opt_trans1 co1 co2\r
 165 \r
 166 opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo\r
 167 -- First arg is not the identity\r
 168 opt_trans1 co1 co2\r
 169   | isIdNormCo co2 = co1\r
 170   | otherwise      = opt_trans2 co1 co2\r
 171 \r
 172 opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo\r
 173 -- Neither arg is the identity\r
 174 opt_trans2 (TyConApp tc [co1a,co1b]) co2\r
 175   | tc `hasKey` transCoercionTyConKey\r
 176   = opt_trans1 co1a (opt_trans2 co1b co2)\r
 177 \r
 178 opt_trans2 co1 co2 \r
 179   | Just co <- opt_trans_rule co1 co2\r
 180   = co\r
 181 \r
 182 opt_trans2 co1 (TyConApp tc [co2a,co2b])\r
 183   | tc `hasKey` transCoercionTyConKey\r
 184   , Just co1_2a <- opt_trans_rule co1 co2a\r
 185   = if isIdNormCo co1_2a\r
 186     then co2b\r
 187     else opt_trans2 co1_2a co2b\r
 188 \r
 189 opt_trans2 co1 co2\r
 190   = mkTransCoercion co1 co2\r
 191 \r
 192 ------\r
 193 opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo\r
 194 opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)\r
 195   | tc1 == tc2\r
 196   = case isCoercionTyCon_maybe tc1 of\r
 197       Nothing \r
 198         -> Just (TyConApp tc1 (opt_transL args1 args2))\r
 199       Just (arity, desc) \r
 200         | arity == length args1\r
 201         -> opt_trans_rule_equal_tc desc args1 args2\r
 202         | otherwise\r
 203         -> case opt_trans_rule_equal_tc desc \r
 204                          (take arity args1) \r
 205                          (take arity args2) of\r
 206               Just co -> Just $ mkAppTys co $ \r
 207                          opt_transL (drop arity args1) (drop arity args2)\r
 208               Nothing -> Nothing \r
 209  \r
 210 -- Push transitivity inside apply\r
 211 opt_trans_rule co1 co2\r
 212   | Just (co1a, co1b) <- splitAppTy_maybe co1\r
 213   , Just (co2a, co2b) <- etaApp_maybe co2\r
 214   = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
 215 \r
 216   | Just (co2a, co2b) <- splitAppTy_maybe co2\r
 217   , Just (co1a, co1b) <- etaApp_maybe co1\r
 218   = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
 219 \r
 220 -- Push transitivity inside (s~t)=>r\r
 221 opt_trans_rule co1 co2\r
 222   | Just (s1,t1,r1) <- splitCoPredTy_maybe co1\r
 223   , Just (s2,t2,r2) <- etaCoPred_maybe co2\r
 224   = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))\r
 225 \r
 226   | Just (s2,t2,r2) <- splitCoPredTy_maybe co2\r
 227   , Just (s1,t1,r1) <- etaCoPred_maybe co1\r
 228   = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))\r
 229 \r
 230 -- Push transitivity inside forall\r
 231 opt_trans_rule co1 co2\r
 232   | Just (tv1,r1) <- splitTypeForAll_maybe co1\r
 233   , Just (tv2,r2) <- etaForAll_maybe co2\r
 234   , let r2' = substTyWith [tv2] [TyVarTy tv1] r2\r
 235   = Just (ForAllTy tv1 (opt_trans2 r1 r2'))\r
 236 \r
 237   | Just (tv2,r2) <- splitTypeForAll_maybe co2\r
 238   , Just (tv1,r1) <- etaForAll_maybe co1\r
 239   , let r1' = substTyWith [tv1] [TyVarTy tv2] r1\r
 240   = Just (ForAllTy tv1 (opt_trans2 r1' r2))\r
 241 \r
 242 opt_trans_rule co1 co2\r
 243 {-      Omitting for now, because unsound\r
 244   | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe\r
 245   , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe\r
 246   , ax_tc1 == ax_tc2\r
 247   , sym1 /= sym2\r
 248   = Just $\r
 249     if sym1 \r
 250     then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs\r
 251     else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs\r
 252 -}\r
 253 \r
 254   | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe\r
 255   , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2\r
 256   = Just $ \r
 257     if sym \r
 258     then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)\r
 259     else                 TyConApp ax_tc (opt_transL ax_args cos)\r
 260 \r
 261   | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2\r
 262   , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1\r
 263   = Just $ \r
 264     if sym \r
 265     then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))\r
 266     else                 TyConApp ax_tc (opt_transL cos ax_args)\r
 267   where\r
 268     co1_is_axiom_maybe = isAxiom_maybe co1\r
 269     co2_is_axiom_maybe = isAxiom_maybe co2\r
 270 \r
 271 opt_trans_rule co1 co2  -- Identity rule\r
 272   | (ty1,_) <- coercionKind co1\r
 273   , (_,ty2) <- coercionKind co2\r
 274   , ty1 `coreEqType` ty2\r
 275   = Just ty2\r
 276 \r
 277 opt_trans_rule _ _ = Nothing\r
 278 \r
 279 -----------  \r
 280 isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))\r
 281 isAxiom_maybe co\r
 282   | Just (tc, args) <- splitTyConApp_maybe co\r
 283   , Just (_, desc)  <- isCoercionTyCon_maybe tc\r
 284   = case desc of\r
 285       CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs } \r
 286             -> Just (False, (tc, args, tvs, lhs, rhs))\r
 287       CoSym | (arg1:_) <- args  \r
 288             -> case isAxiom_maybe arg1 of\r
 289                  Nothing           -> Nothing\r
 290                  Just (sym, stuff) -> Just (not sym, stuff)\r
 291       _ -> Nothing\r
 292   | otherwise\r
 293   = Nothing\r
 294 \r
 295 matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]\r
 296 matchesAxiomLhs tvs ty_tmpl ty \r
 297   = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of\r
 298       Nothing    -> Nothing\r
 299       Just subst -> Just (map (substTyVar subst) tvs)\r
 300 \r
 301 -----------  \r
 302 opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion\r
 303 -- Rules for Coercion TyCons only\r
 304 \r
 305 -- Push transitivity inside instantiation\r
 306 opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]\r
 307   | CoInst <- desc\r
 308   , ty1 `coreEqType` ty2\r
 309   , co1 `compatible_co` co2\r
 310   = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) \r
 311 \r
 312 opt_trans_rule_equal_tc desc [co1] [co2]\r
 313   | CoLeft  <- desc, is_compat = Just (mkLeftCoercion res_co)\r
 314   | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)\r
 315   | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)\r
 316   | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)\r
 317   | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)\r
 318   where\r
 319     is_compat = co1 `compatible_co` co2\r
 320     res_co    = opt_trans2 co1 co2\r
 321 \r
 322 opt_trans_rule_equal_tc _ _ _ = Nothing\r
 323 \r
 324 -------------\r
 325 compatible_co :: Coercion -> Coercion -> Bool\r
 326 -- Check whether (co1 . co2) will be well-kinded\r
 327 compatible_co co1 co2\r
 328   = x1 `coreEqType` x2          \r
 329   where\r
 330     (_,x1) = coercionKind co1\r
 331     (x2,_) = coercionKind co2\r
 332 \r
 333 -------------\r
 334 etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
 335 -- Try to make the coercion be of form (forall tv. co)\r
 336 etaForAll_maybe co\r
 337   | Just (tv, r) <- splitForAllTy_maybe co\r
 338   , not (isCoVar tv)    -- Check it is a *type* forall, not a (t1~t2)=>co\r
 339   = Just (tv, r)\r
 340 \r
 341   | (ty1,ty2) <- coercionKind co\r
 342   , Just (tv1, _) <- splitTypeForAll_maybe ty1\r
 343   , Just (tv2, _) <- splitTypeForAll_maybe ty2\r
 344   , tyVarKind tv1 `eqKind` tyVarKind tv2\r
 345   = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))\r
 346 \r
 347   | otherwise\r
 348   = Nothing\r
 349 \r
 350 etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)\r
 351 etaCoPred_maybe co \r
 352   | Just (s,t,r) <- splitCoPredTy_maybe co\r
 353   = Just (s,t,r)\r
 354   \r
 355   --  co :: (s1~t1)=>r1 ~ (s2~t2)=>r2\r
 356   | (ty1,ty2) <- coercionKind co        -- We know ty1,ty2 have same kind\r
 357   , Just (s1,_,_) <- splitCoPredTy_maybe ty1\r
 358   , Just (s2,_,_) <- splitCoPredTy_maybe ty2\r
 359   , typeKind s1 `eqKind` typeKind s2    -- t1,t2 have same kinds\r
 360   = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)\r
 361   \r
 362   | otherwise\r
 363   = Nothing\r
 364 \r
 365 etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)\r
 366 -- Split a coercion g :: t1a t1b ~ t2a t2b\r
 367 -- into (left g, right g) if possible\r
 368 etaApp_maybe co\r
 369   | Just (co1, co2) <- splitAppTy_maybe co\r
 370   = Just (co1, co2)\r
 371 \r
 372   | (ty1,ty2) <- coercionKind co\r
 373   , Just (ty1a, _) <- splitAppTy_maybe ty1\r
 374   , Just (ty2a, _) <- splitAppTy_maybe ty2\r
 375   , typeKind ty1a `eqKind` typeKind ty2a\r
 376   = Just (mkLeftCoercion co, mkRightCoercion co)\r
 377 \r
 378   | otherwise\r
 379   = Nothing\r
 380 \r
 381 -------------\r
 382 splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)\r
 383 -- Returns Just only for a *type* forall, not a (t1~t2)=>co\r
 384 splitTypeForAll_maybe ty\r
 385   | Just (tv, rty) <- splitForAllTy_maybe ty\r
 386   , not (isCoVar tv)\r
 387   = Just (tv, rty)\r
 388 \r
 389   | otherwise\r
 390   = Nothing\r
 391 \r
 392 -------------\r
 393 isIdNormCo :: NormalCo -> Bool\r
 394 -- Cheap identity test: look for coercions with no coercion variables at all\r
 395 -- So it'll return False for (sym g `trans` g)\r
 396 isIdNormCo ty = go ty\r
 397   where\r
 398     go (TyVarTy tv)            = not (isCoVar tv)\r
 399     go (AppTy t1 t2)           = go t1 && go t2\r
 400     go (FunTy t1 t2)           = go t1 && go t2\r
 401     go (ForAllTy tv ty)        = go (tyVarKind tv) && go ty\r
 402     go (TyConApp tc tys)       = not (isCoercionTyCon tc) && all go tys\r
 403     go (PredTy (IParam _ ty))  = go ty\r
 404     go (PredTy (ClassP _ tys)) = all go tys\r
 405     go (PredTy (EqPred t1 t2)) = go t1 && go t2\r
 406 \end{code}  \r