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