compiler/types/Coercion.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 Module for type coercions, as in System FC.
   6
   7 Coercions are represented as types, and their kinds tell what types the
   8 coercion works on.
   9
  10 The coercion kind constructor is a special TyCon that must always be saturated
  11
  12   typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
  13
  14 \begin{code}
  15 module Coercion (
  16         Coercion,
  17
  18         mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
  19         coercionKind, coercionKinds, coercionKindPredTy,
  20
  21         -- Equality predicates
  22         isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
  23
  24         -- Coercion transformations
  25         mkSymCoercion, mkTransCoercion,
  26         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
  27         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
  28         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
  29
  30         splitNewTypeRepCo_maybe, decomposeCo,
  31
  32         unsafeCoercionTyCon, symCoercionTyCon,
  33         transCoercionTyCon, leftCoercionTyCon,
  34         rightCoercionTyCon, instCoercionTyCon -- needed by TysWiredIn
  35        ) where
  36
  37 #include "HsVersions.h"
  38
  39 import TypeRep
  40 import Type
  41 import TyCon
  42 import Var
  43 import Name
  44 import OccName
  45 import PrelNames
  46 import Util
  47 import Unique
  48 import BasicTypes
  49 import Outputable
  50
  51
  52 ------------------------------
  53 decomposeCo :: Arity -> Coercion -> [Coercion]
  54 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
  55 -- So this breaks a coercion with kind T A B C :=: T D E F into
  56 -- a list of coercions of kinds A :=: D, B :=: E and E :=: F
  57 decomposeCo n co
  58   = go n co []
  59   where
  60     go 0 co cos = cos
  61     go n co cos = go (n-1) (mkLeftCoercion co)
  62                            (mkRightCoercion co : cos)
  63
  64 ------------------------------
  65
  66 -------------------------------------------------------
  67 -- and some coercion kind stuff
  68
  69 isEqPredTy (PredTy pred) = isEqPred pred
  70 isEqPredTy other         = False
  71
  72 mkEqPred :: (Type, Type) -> PredType
  73 mkEqPred (ty1, ty2) = EqPred ty1 ty2
  74
  75 getEqPredTys :: PredType -> (Type,Type)
  76 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
  77 getEqPredTys other            = pprPanic "getEqPredTys" (ppr other)
  78
  79 mkCoKind :: Type -> Type -> CoercionKind
  80 mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
  81
  82 mkReflCoKind :: Type -> CoercionKind
  83 mkReflCoKind ty = mkCoKind ty ty
  84
  85 splitCoercionKind :: CoercionKind -> (Type, Type)
  86 splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
  87 splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
  88
  89 splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
  90 splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
  91 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
  92 splitCoercionKind_maybe other = Nothing
  93
  94 type Coercion     = Type
  95 type CoercionKind = Kind        -- A CoercionKind is always of form (ty1 :=: ty2)
  96
  97 coercionKind :: Coercion -> (Type, Type)
  98 --      c :: (t1 :=: t2)
  99 -- Then (coercionKind c) = (t1,t2)
 100 coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
 101                             | otherwise = (ty, ty)
 102 coercionKind (AppTy ty1 ty2)
 103   = let (t1, t2) = coercionKind ty1
 104         (s1, s2) = coercionKind ty2 in
 105     (mkAppTy t1 s1, mkAppTy t2 s2)
 106 coercionKind (TyConApp tc args)
 107   | Just (ar, rule) <- isCoercionTyCon_maybe tc
 108     -- CoercionTyCons carry their kinding rule, so we use it here
 109   = ASSERT( length args >= ar ) -- Always saturated
 110     let (ty1,ty2)    = rule (take ar args)      -- Apply the rule to the right number of args
 111         (tys1, tys2) = coercionKinds (drop ar args)
 112     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
 113
 114   | otherwise
 115   = let (lArgs, rArgs) = coercionKinds args in
 116     (TyConApp tc lArgs, TyConApp tc rArgs)
 117 coercionKind (FunTy ty1 ty2)
 118   = let (t1, t2) = coercionKind ty1
 119         (s1, s2) = coercionKind ty2 in
 120     (mkFunTy t1 s1, mkFunTy t2 s2)
 121 coercionKind (ForAllTy tv ty)
 122   = let (ty1, ty2) = coercionKind ty in
 123     (ForAllTy tv ty1, ForAllTy tv ty2)
 124 coercionKind (NoteTy _ ty) = coercionKind ty
 125 coercionKind (PredTy (EqPred c1 c2))
 126   = let k1 = coercionKindPredTy c1
 127         k2 = coercionKindPredTy c2 in
 128     (k1,k2)
 129 coercionKind (PredTy (ClassP cl args))
 130   = let (lArgs, rArgs) = coercionKinds args in
 131     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
 132 coercionKind (PredTy (IParam name ty))
 133   = let (ty1, ty2) = coercionKind ty in
 134     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 135
 136 coercionKindPredTy :: Coercion -> CoercionKind
 137 coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
 138
 139 coercionKinds :: [Coercion] -> ([Type], [Type])
 140 coercionKinds tys = unzip $ map coercionKind tys
 141
 142 -------------------------------------
 143 -- Coercion kind and type mk's
 144 -- (make saturated TyConApp CoercionTyCon{...} args)
 145
 146 mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
 147                         TyConApp coCon args
 148
 149 mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
 150 mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion
 151
 152 mkAppCoercion    co1 co2 = mkAppTy co1 co2
 153 mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
 154 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
 155 mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
 156 mkFunCoercion    co1 co2 = mkFunTy co1 co2
 157
 158
 159 -------------------------------
 160 -- This smart constructor creates a sym'ed version its argument,
 161 -- but tries to push the sym's down to the leaves.  If we come to
 162 -- sym tv or sym tycon then we can drop the sym because tv and tycon
 163 -- are reflexive coercions
 164 mkSymCoercion co
 165   | Just co' <- coreView co = mkSymCoercion co'
 166
 167 mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
 168 mkSymCoercion (AppTy co1 co2)   = AppTy (mkSymCoercion co1) (mkSymCoercion co2)
 169 mkSymCoercion (FunTy co1 co2)   = FunTy (mkSymCoercion co1) (mkSymCoercion co2)
 170
 171 mkSymCoercion (TyConApp tc cos)
 172   | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)
 173
 174 mkSymCoercion (TyConApp tc [co])
 175   | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
 176   | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
 177   | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)
 178
 179 mkSymCoercion (TyConApp tc [co1,co2])
 180   | tc `hasKey` transCoercionTyConKey
 181      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 182      -- Note reversal of arguments!
 183   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 184
 185   | tc `hasKey` instCoercionTyConKey
 186      -- sym (co @ ty) --> (sym co) @ ty
 187      -- Note: sym is not applied to 'ty'
 188   = mkInstCoercion (mkSymCoercion co1) co2
 189
 190 mkSymCoercion (TyConApp tc cos)         -- Other coercion tycons, such as those
 191   = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes
 192
 193 mkSymCoercion (TyVarTy tv)
 194   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 195   | otherwise  = TyVarTy tv     -- Reflexive
 196
 197 -------------------------------
 198 -- ToDo: we should be cleverer about transitivity
 199 mkTransCoercion g1 g2   -- sym g `trans` g = id
 200   | (t1,_) <- coercionKind g1
 201   , (_,t2) <- coercionKind g2
 202   , t1 `coreEqType` t2
 203   = t1
 204
 205   | otherwise
 206   = mkCoercion transCoercionTyCon [g1, g2]
 207
 208
 209 -------------------------------
 210 -- Smart constructors for left and right
 211 mkLeftCoercion co
 212   | Just (co', _) <- splitAppCoercion_maybe co = co'
 213   | otherwise = mkCoercion leftCoercionTyCon [co]
 214
 215 mkRightCoercion  co
 216   | Just (co1, co2) <- splitAppCoercion_maybe co = co2
 217   | otherwise = mkCoercion rightCoercionTyCon [co]
 218
 219 mkInstCoercion co ty
 220   | Just (tv,co') <- splitForAllTy_maybe co
 221   = substTyWith [tv] [ty] co'   -- (forall a.co) @ ty  -->  co[ty/a]
 222   | otherwise
 223   = mkCoercion instCoercionTyCon  [co, ty]
 224
 225 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 226
 227 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 228 splitSymCoercion_maybe (TyConApp tc [co]) =
 229   if tc `hasKey` symCoercionTyConKey
 230   then Just co
 231   else Nothing
 232 splitSymCoercion_maybe co = Nothing
 233
 234 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 235 -- Splits a coercion application, being careful *not* to split (left c), etc
 236 -- which are really sytactic constructs, not applications
 237 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 238 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 239 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 240 splitAppCoercion_maybe (TyConApp tc tys)
 241    | not (isCoercionTyCon tc)
 242    = case snocView tys of
 243        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 244        Nothing          -> Nothing
 245 splitAppCoercion_maybe co = Nothing
 246
 247 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 248 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 249  = if tc `hasKey` transCoercionTyConKey then
 250        Just (ty1, ty2)
 251    else
 252        Nothing
 253 splitTransCoercion_maybe other = Nothing
 254
 255 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 256 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 257  = if tc `hasKey` instCoercionTyConKey then
 258        Just (ty1, ty2)
 259     else
 260        Nothing
 261 splitInstCoercion_maybe other = Nothing
 262
 263 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 264 splitLeftCoercion_maybe (TyConApp tc [co])
 265  = if tc `hasKey` leftCoercionTyConKey then
 266        Just co
 267    else
 268        Nothing
 269 splitLeftCoercion_maybe other = Nothing
 270
 271 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 272 splitRightCoercion_maybe (TyConApp tc [co])
 273  = if tc `hasKey` rightCoercionTyConKey then
 274        Just co
 275    else
 276        Nothing
 277 splitRightCoercion_maybe other = Nothing
 278
 279 -- Unsafe coercion is not safe, it is used when we know we are dealing with
 280 -- bottom, which is one case in which it is safe.  It is also used to
 281 -- implement the unsafeCoerce# primitive.
 282 mkUnsafeCoercion :: Type -> Type -> Coercion
 283 mkUnsafeCoercion ty1 ty2
 284   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 285
 286
 287 -- See note [Newtype coercions] in TyCon
 288 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 289 mkNewTypeCoercion name tycon tvs rhs_ty
 290   = mkCoercionTyCon name co_con_arity rule
 291   where
 292     co_con_arity = length tvs
 293
 294     rule args = ASSERT( co_con_arity == length args )
 295                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 296
 297 -- Coercion identifying a data/newtype/synonym representation type and its
 298 -- family instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is
 299 -- the coercion tycon built here, `F' the family tycon and `R' the (derived)
 300 -- representation tycon.
 301 --
 302 mkFamInstCoercion :: Name       -- unique name for the coercion tycon
 303                   -> [TyVar]    -- type parameters of the coercion (`tvs')
 304                   -> TyCon      -- family tycon (`F')
 305                   -> [Type]     -- type instance (`ts')
 306                   -> TyCon      -- representation tycon (`R')
 307                   -> TyCon      -- => coercion tycon (`Co')
 308 mkFamInstCoercion name tvs family instTys rep_tycon
 309   = mkCoercionTyCon name coArity rule
 310   where
 311     coArity = length tvs
 312     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 313                    TyConApp family instTys,          --       sigma (F ts)
 314                  TyConApp rep_tycon args)            --   :=: R tys
 315
 316 --------------------------------------
 317 -- Coercion Type Constructors...
 318
 319 -- Example.  The coercion ((sym c) (sym d) (sym e))
 320 -- will be represented by (TyConApp sym [c, sym d, sym e])
 321 -- If sym c :: p1=q1
 322 --    sym d :: p2=q2
 323 --    sym e :: p3=q3
 324 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 325
 326 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
 327 -- Each coercion TyCon is built with the special CoercionTyCon record and
 328 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 329 -- by any TyConApp in which they are applied, however they may also be over
 330 -- applied (see example above) and the kinding function must deal with this.
 331 symCoercionTyCon =
 332   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 333   where
 334     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 335         where
 336           (ty1, ty2) = coercionKind co
 337
 338 transCoercionTyCon =
 339   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 340   where
 341     composeCoercionKindsOf (co1:co2:rest)
 342       = ASSERT( null rest )
 343         WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
 344         (a1, r2)
 345       where
 346         (a1, r1) = coercionKind co1
 347         (a2, r2) = coercionKind co2
 348
 349 leftCoercionTyCon =
 350   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 351   where
 352     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 353       where
 354         (ty1,ty2) = fst (splitCoercionKindOf co)
 355
 356 rightCoercionTyCon =
 357   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 358   where
 359     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 360       where
 361         (ty1,ty2) = snd (splitCoercionKindOf co)
 362
 363 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 364 -- Helper for left and right.  Finds coercion kind of its input and
 365 -- returns the left and right projections of the coercion...
 366 --
 367 -- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 368 splitCoercionKindOf co
 369   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 370   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 371   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 372   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 373
 374 instCoercionTyCon
 375   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 376   where
 377     instantiateCo t s =
 378       let Just (tv, ty) = splitForAllTy_maybe t in
 379       substTyWith [tv] [s] ty
 380
 381     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 382                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 383       where (t1, t2) = coercionKind co1
 384
 385 unsafeCoercionTyCon
 386   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 387   where
 388    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 389
 390 --------------------------------------
 391 -- ...and their names
 392
 393 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 394                             key (ATyCon coCon) BuiltInSyntax
 395
 396 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 397 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
 398 leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
 399 rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
 400 instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
 401 unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 402
 403
 404
 405 -- this is here to avoid module loops
 406 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 407 -- Sometimes we want to look through a newtype and get its associated coercion
 408 -- It only strips *one layer* off, so the caller will usually call itself recursively
 409 -- Only applied to types of kind *, hence the newtype is always saturated
 410 splitNewTypeRepCo_maybe ty
 411   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 412 splitNewTypeRepCo_maybe (TyConApp tc tys)
 413   | isClosedNewTyCon tc
 414   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitNewTypeRepCo_maybe only be applied
 415                                                 --      to *types* (of kind *)
 416         case newTyConRhs tc of
 417           (tvs, rep_ty) ->
 418               ASSERT( length tvs == length tys )
 419               Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
 420   where
 421     co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)
 422 splitNewTypeRepCo_maybe other = Nothing
 423 \end{code}