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, mkDataInstCoercion, 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 -- This smart constructor creates a sym'ed version its argument,
 160 -- but tries to push the sym's down to the leaves.  If we come to
 161 -- sym tv or sym tycon then we can drop the sym because tv and tycon
 162 -- are reflexive coercions
 163 mkSymCoercion co
 164   | Just co2 <- splitSymCoercion_maybe co = co2
 165      -- sym (sym co) --> co
 166   | Just (co1, arg_tys) <- splitTyConApp_maybe co
 167   , not (isCoercionTyCon co1) = mkTyConApp co1 (map mkSymCoercion arg_tys)
 168      -- we can drop the sym for a TyCon
 169      -- sym (ty [t1, ..., tn]) --> ty [sym t1, ..., sym tn]
 170   | (co1, arg_tys) <- splitAppTys co
 171   , isTyVarTy co1 = mkAppTys (maybe_drop co1) (map mkSymCoercion arg_tys)
 172      -- sym (tv [t1, ..., tn]) --> tv [sym t1, ..., sym tn]
 173      --   if tv type variable
 174      -- sym (cv [t1, ..., tn]) --> (sym cv) [sym t1, ..., sym tn]
 175      --   if cv is a coercion variable
 176      -- fall through if head is a CoercionTyCon
 177   | Just (co1, co2) <- splitTransCoercion_maybe co
 178      -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
 179   = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
 180   | Just (co, ty) <- splitInstCoercion_maybe co
 181      -- sym (co @ ty) --> (sym co) @ ty
 182   = mkInstCoercion (mkSymCoercion co) ty
 183   | Just co <- splitLeftCoercion_maybe co
 184      -- sym (left co) --> left (sym co)
 185   = mkLeftCoercion (mkSymCoercion co)
 186   | Just co <- splitRightCoercion_maybe co
 187      -- sym (right co) --> right (sym co)
 188   = mkRightCoercion (mkSymCoercion co)
 189   where
 190     maybe_drop (TyVarTy tv)
 191         | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 192         | otherwise  = TyVarTy tv
 193     maybe_drop other = other
 194 mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty)
 195 -- for atomic types and constructors, we can just ignore sym since these
 196 -- are reflexive coercions
 197 mkSymCoercion (TyVarTy tv)
 198   | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
 199   | otherwise  = TyVarTy tv
 200 mkSymCoercion co = mkCoercion symCoercionTyCon [co]
 201
 202 -- Smart constructors for left and right
 203 mkLeftCoercion co
 204   | Just (co', _) <- splitAppCoercion_maybe co = co'
 205   | otherwise                            = mkCoercion leftCoercionTyCon [co]
 206
 207 mkRightCoercion  co
 208   | Just (co1, co2) <- splitAppCoercion_maybe co = co2
 209   | otherwise = mkCoercion rightCoercionTyCon [co]
 210
 211 mkTransCoercion co1 co2 = mkCoercion transCoercionTyCon [co1, co2]
 212
 213 mkInstCoercion  co ty = mkCoercion instCoercionTyCon  [co, ty]
 214
 215 mkInstsCoercion co tys = foldl mkInstCoercion co tys
 216
 217 splitSymCoercion_maybe :: Coercion -> Maybe Coercion
 218 splitSymCoercion_maybe (TyConApp tc [co]) =
 219   if tc `hasKey` symCoercionTyConKey
 220   then Just co
 221   else Nothing
 222 splitSymCoercion_maybe co = Nothing
 223
 224 splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 225 -- Splits a coercion application, being careful *not* to split (left c), etc
 226 -- which are really sytactic constructs, not applications
 227 splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
 228 splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 229 splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 230 splitAppCoercion_maybe (TyConApp tc tys)
 231    | not (isCoercionTyCon tc)
 232    = case snocView tys of
 233        Just (tys', ty') -> Just (TyConApp tc tys', ty')
 234        Nothing          -> Nothing
 235 splitAppCoercion_maybe co = Nothing
 236
 237 splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
 238 splitTransCoercion_maybe (TyConApp tc [ty1, ty2])
 239  = if tc `hasKey` transCoercionTyConKey then
 240        Just (ty1, ty2)
 241    else
 242        Nothing
 243 splitTransCoercion_maybe other = Nothing
 244
 245 splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
 246 splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 247  = if tc `hasKey` instCoercionTyConKey then
 248        Just (ty1, ty2)
 249     else
 250        Nothing
 251 splitInstCoercion_maybe other = Nothing
 252
 253 splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
 254 splitLeftCoercion_maybe (TyConApp tc [co])
 255  = if tc `hasKey` leftCoercionTyConKey then
 256        Just co
 257    else
 258        Nothing
 259 splitLeftCoercion_maybe other = Nothing
 260
 261 splitRightCoercion_maybe :: Coercion -> Maybe Coercion
 262 splitRightCoercion_maybe (TyConApp tc [co])
 263  = if tc `hasKey` rightCoercionTyConKey then
 264        Just co
 265    else
 266        Nothing
 267 splitRightCoercion_maybe other = Nothing
 268
 269 -- Unsafe coercion is not safe, it is used when we know we are dealing with
 270 -- bottom, which is one case in which it is safe.  It is also used to
 271 -- implement the unsafeCoerce# primitive.
 272 mkUnsafeCoercion :: Type -> Type -> Coercion
 273 mkUnsafeCoercion ty1 ty2
 274   = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 275
 276
 277 -- See note [Newtype coercions] in TyCon
 278 mkNewTypeCoercion :: Name -> TyCon -> ([TyVar], Type) -> TyCon
 279 mkNewTypeCoercion name tycon (tvs, rhs_ty)
 280   = mkCoercionTyCon name co_con_arity rule
 281   where
 282     co_con_arity = length tvs
 283
 284     rule args = ASSERT( co_con_arity == length args )
 285                 (TyConApp tycon args, substTyWith tvs args rhs_ty)
 286
 287 -- Coercion identifying a data/newtype representation type and its family
 288 -- instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the
 289 -- coercion tycon built here, `F' the family tycon and `R' the (derived)
 290 -- representation tycon.
 291 --
 292 mkDataInstCoercion :: Name      -- unique name for the coercion tycon
 293                    -> [TyVar]   -- type parameters of the coercion (`tvs')
 294                    -> TyCon     -- family tycon (`F')
 295                    -> [Type]    -- type instance (`ts')
 296                    -> TyCon     -- representation tycon (`R')
 297                    -> TyCon     -- => coercion tycon (`Co')
 298 mkDataInstCoercion name tvs family instTys rep_tycon
 299   = mkCoercionTyCon name coArity rule
 300   where
 301     coArity = length tvs
 302     rule args = (substTyWith tvs args $              -- with sigma = [tys/tvs],
 303                    TyConApp family instTys,          --       sigma (F ts)
 304                  TyConApp rep_tycon args)            --   :=: R tys
 305
 306 --------------------------------------
 307 -- Coercion Type Constructors...
 308
 309 -- Example.  The coercion ((sym c) (sym d) (sym e))
 310 -- will be represented by (TyConApp sym [c, sym d, sym e])
 311 -- If sym c :: p1=q1
 312 --    sym d :: p2=q2
 313 --    sym e :: p3=q3
 314 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 315
 316 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
 317 -- Each coercion TyCon is built with the special CoercionTyCon record and
 318 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 319 -- by any TyConApp in which they are applied, however they may also be over
 320 -- applied (see example above) and the kinding function must deal with this.
 321 symCoercionTyCon =
 322   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
 323   where
 324     flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
 325         where
 326           (ty1, ty2) = coercionKind co
 327
 328 transCoercionTyCon =
 329   mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
 330   where
 331     composeCoercionKindsOf (co1:co2:rest)
 332       = ASSERT( null rest )
 333         WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
 334         (a1, r2)
 335       where
 336         (a1, r1) = coercionKind co1
 337         (a2, r2) = coercionKind co2
 338
 339 leftCoercionTyCon =
 340   mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
 341   where
 342     leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 343       where
 344         (ty1,ty2) = fst (splitCoercionKindOf co)
 345
 346 rightCoercionTyCon =
 347   mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
 348   where
 349     rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
 350       where
 351         (ty1,ty2) = snd (splitCoercionKindOf co)
 352
 353 splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
 354 -- Helper for left and right.  Finds coercion kind of its input and
 355 -- returns the left and right projections of the coercion...
 356 --
 357 -- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
 358 splitCoercionKindOf co
 359   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
 360   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 361   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
 362   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 363
 364 instCoercionTyCon
 365   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
 366   where
 367     instantiateCo t s =
 368       let Just (tv, ty) = splitForAllTy_maybe t in
 369       substTyWith [tv] [s] ty
 370
 371     instCoercionKind (co1:ty:rest) = ASSERT( null rest )
 372                                      (instantiateCo t1 ty, instantiateCo t2 ty)
 373       where (t1, t2) = coercionKind co1
 374
 375 unsafeCoercionTyCon
 376   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
 377   where
 378    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
 379
 380 --------------------------------------
 381 -- ...and their names
 382
 383 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 384                             key (ATyCon coCon) BuiltInSyntax
 385
 386 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 387 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
 388 leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
 389 rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
 390 instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
 391 unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
 392
 393
 394
 395 -- this is here to avoid module loops
 396 splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 397 -- Sometimes we want to look through a newtype and get its associated coercion
 398 -- It only strips *one layer* off, so the caller will usually call itself recursively
 399 -- Only applied to types of kind *, hence the newtype is always saturated
 400 splitNewTypeRepCo_maybe ty
 401   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 402 splitNewTypeRepCo_maybe (TyConApp tc tys)
 403   | isClosedNewTyCon tc
 404   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitNewTypeRepCo_maybe only be applied
 405                                                 --      to *types* (of kind *)
 406         case newTyConRhs tc of
 407           (tvs, rep_ty) ->
 408               ASSERT( length tvs == length tys )
 409               Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
 410   where
 411     co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)
 412 splitNewTypeRepCo_maybe other = Nothing
 413 \end{code}