Coercion.lhs 32.1 KB
Newer Older
1
%
2
3
% (c) The University of Glasgow 2006
%
4
5

\begin{code}
6
7
-- | Module for (a) type kinds and (b) type coercions, 
-- as used in System FC. See 'CoreSyn.Expr' for
batterseapower's avatar
batterseapower committed
8
9
10
-- more on System FC and how coercions fit into it.
--
-- Coercions are represented as types, and their kinds tell what types the 
11
12
-- coercion works on. The coercion kind constructor is a special TyCon that 
-- must always be saturated, like so:
batterseapower's avatar
batterseapower committed
13
--
14
-- > typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type]
15
module Coercion (
batterseapower's avatar
batterseapower committed
16
        -- * Main data type
17
18
19
20
        Coercion, Kind,
        typeKind,

        -- ** Deconstructing Kinds 
21
22
        kindFunResult, kindAppResult, synTyConResKind,
        splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
23
24
25
26
27
28
29
30
31
32

        -- ** Predicates on Kinds
        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
        isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
        isCoSuperKind, isSuperKind, isCoercionKind, 
	mkArrowKind, mkArrowKinds,

        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
        isSubKindCon,

33
        mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
34
        coercionKind, coercionKinds, isIdentityCoercion,
35

batterseapower's avatar
batterseapower committed
36
	-- ** Equality predicates
37
38
	isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  

batterseapower's avatar
batterseapower committed
39
	-- ** Coercion transformations
40
	mkCoercion,
41
        mkSymCoercion, mkTransCoercion,
42
        mkLeftCoercion, mkRightCoercion, 
43
44
	mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
        mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
45
        mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
46
        mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, 
47
48
49

	mkClassPPredCo, mkIParamPredCo,
        mkCoVarCoercion, mkCoPredCo, 
50
51
52
53


        unsafeCoercionTyCon, symCoercionTyCon,
        transCoercionTyCon, leftCoercionTyCon, 
TomSchrijvers's avatar
TomSchrijvers committed
54
        rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
55
        csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon, 
TomSchrijvers's avatar
TomSchrijvers committed
56

57
58
        -- ** Decomposition
        decompLR_maybe, decompCsel_maybe, decompInst_maybe,
59
60
        splitCoPredTy_maybe,
        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
61

batterseapower's avatar
batterseapower committed
62
        -- ** Comparison
63
        coreEqCoercion, coreEqCoercion2,
64

batterseapower's avatar
batterseapower committed
65
	-- * CoercionI
TomSchrijvers's avatar
TomSchrijvers committed
66
	CoercionI(..),
67
	isIdentityCoI,
TomSchrijvers's avatar
TomSchrijvers committed
68
69
	mkSymCoI, mkTransCoI, 
	mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
70
	mkForAllTyCoI,
71
	fromCoI, 
72
	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI 
TomSchrijvers's avatar
TomSchrijvers committed
73

74
75
76
77
78
       ) where 

#include "HsVersions.h"

import TypeRep
79
80
import Type
import TyCon
TomSchrijvers's avatar
TomSchrijvers committed
81
import Class
82
import Var
83
import VarEnv
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
84
import VarSet
85
86
87
88
import Name
import PrelNames
import Util
import BasicTypes
89
import Outputable
90
import FastString
91
92
93
94
95
96
97
\end{code}

%************************************************************************
%*									*
	Functions over Kinds		
%*									*
%************************************************************************
98

99
100
101
102
103
\begin{code}
-- | Essentially 'funResultTy' on kinds
kindFunResult :: Kind -> Kind
kindFunResult k = funResultTy k

104
105
106
107
kindAppResult :: Kind -> [arg] -> Kind
kindAppResult k []     = k
kindAppResult k (_:as) = kindAppResult (kindFunResult k) as

108
109
110
111
112
113
114
115
116
117
118
-- | Essentially 'splitFunTys' on kinds
splitKindFunTys :: Kind -> ([Kind],Kind)
splitKindFunTys k = splitFunTys k

splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
splitKindFunTy_maybe = splitFunTy_maybe

-- | Essentially 'splitFunTysN' on kinds
splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
splitKindFunTysN k = splitFunTysN k

119
120
121
122
123
124
125
-- | Find the result 'Kind' of a type synonym, 
-- after applying it to its 'arity' number of type variables
-- Actually this function works fine on data types too, 
-- but they'd always return '*', so we never need to ask
synTyConResKind :: TyCon -> Kind
synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)

126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
        isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool

isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey

isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
isOpenTypeKind _               = False

isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey

isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
isUbxTupleKind _               = False

isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey

isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
isArgTypeKind _               = False

isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey

isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
isUnliftedTypeKind _               = False

isSubOpenTypeKind :: Kind -> Bool
-- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
                                     ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
                                     False
isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
isSubOpenTypeKind other            = ASSERT( isKind other ) False
         -- This is a conservative answer
         -- It matters in the call to isSubKind in
	 -- checkExpectedKind.

isSubArgTypeKindCon kc
  | isUnliftedTypeKindCon kc = True
  | isLiftedTypeKindCon kc   = True
  | isArgTypeKindCon kc      = True
  | otherwise                = False

isSubArgTypeKind :: Kind -> Bool
-- ^ True of any sub-kind of ArgTypeKind 
isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
isSubArgTypeKind _                = False

-- | Is this a super-kind (i.e. a type-of-kinds)?
isSuperKind :: Type -> Bool
isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
isSuperKind _                   = False

-- | Is this a kind (i.e. a type-of-types)?
isKind :: Kind -> Bool
isKind k = isSuperKind (typeKind k)

isSubKind :: Kind -> Kind -> Bool
-- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
isSubKind (FunTy a1 r1) (FunTy a2 r2)	      = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) 
  = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
isSubKind _             _                     = False

eqKind :: Kind -> Kind -> Bool
eqKind = tcEqType

isSubKindCon :: TyCon -> TyCon -> Bool
-- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
isSubKindCon kc1 kc2
  | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
  | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
  | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
  | isOpenTypeKindCon kc2                                  = True 
                           -- we already know kc1 is not a fun, its a TyCon
  | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
  | otherwise                                              = False

defaultKind :: Kind -> Kind
-- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
-- information on what that means

-- When we generalise, we make generic type variables whose kind is
-- simple (* or *->* etc).  So generic type variables (other than
-- built-in constants like 'error') always have simple kinds.  This is important;
-- consider
--	f x = True
-- We want f to get type
--	f :: forall (a::*). a -> Bool
-- Not 
--	f :: forall (a::??). a -> Bool
-- because that would allow a call like (f 3#) as well as (f True),
--and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
defaultKind k 
  | isSubOpenTypeKind k = liftedTypeKind
  | isSubArgTypeKind k  = liftedTypeKind
  | otherwise        = k
\end{code}

%************************************************************************
%*									*
            Coercions
%*									*
%************************************************************************


\begin{code}
batterseapower's avatar
batterseapower committed
233
-- | A 'Coercion' represents a 'Type' something should be coerced to.
234
type Coercion     = Type
batterseapower's avatar
batterseapower committed
235

236
-- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
batterseapower's avatar
batterseapower committed
237
238
-- types that a 'Coercion' will work on.
type CoercionKind = Kind
239

240
------------------------------
batterseapower's avatar
batterseapower committed
241

242
243
-- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
244
245
--
-- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
246
247
248
249
decomposeCo :: Arity -> Coercion -> [Coercion]
decomposeCo n co
  = go n co []
  where
250
    go 0 _  cos = cos
251
252
253
254
255
256
257
    go n co cos = go (n-1) (mkLeftCoercion co)
			   (mkRightCoercion co : cos)


-------------------------------------------------------
-- and some coercion kind stuff

258
259
coVarKind :: CoVar -> (Type,Type) 
-- c :: t1 ~ t2
260
261
262
263
264
265
coVarKind cv = case coVarKind_maybe cv of
                 Just ts -> ts
                 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))

coVarKind_maybe :: CoVar -> Maybe (Type,Type) 
coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv)
266
267
268

-- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
-- Panics if the argument is not a valid 'CoercionKind'
269
270
271
272
splitCoKind_maybe :: Kind -> Maybe (Type, Type)
splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co'
splitCoKind_maybe (PredTy (EqPred ty1 ty2))    = Just (ty1, ty2)
splitCoKind_maybe _                            = Nothing
273

274
275
-- | Makes a 'CoercionKind' from two types: the types whose equality 
-- is proven by the relevant 'Coercion'
276
277
278
279
280
mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)

-- | (mkCoPredTy s t r) produces the type:   (s~t) => r
mkCoPredTy :: Type -> Type -> Type -> Type
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
281
282
283
284
mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) )
                   ForAllTy co_var r
  where
    co_var = mkWildCoVar (mkCoKind s t)
285

286
287
288
289
290
mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion 
-- Creates a coercion between (s1~t1) => r1  and (s2~t2) => r2 
mkCoPredCo = mkCoPredTy 


291
292
293
294
295
296
297
298
299
splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
splitCoPredTy_maybe ty
  | Just (cv,r) <- splitForAllTy_maybe ty
  , isCoVar cv
  , Just (s,t) <- coVarKind_maybe cv
  = Just (s,t,r)
  | otherwise
  = Nothing

batterseapower's avatar
batterseapower committed
300
-- | Tests whether a type is just a type equality predicate
301
isEqPredTy :: Type -> Bool
302
isEqPredTy (PredTy pred) = isEqPred pred
303
isEqPredTy _             = False
304

batterseapower's avatar
batterseapower committed
305
-- | Creates a type equality predicate
306
307
308
mkEqPred :: (Type, Type) -> PredType
mkEqPred (ty1, ty2) = EqPred ty1 ty2

batterseapower's avatar
batterseapower committed
309
310
-- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
-- Panics otherwise
311
312
313
314
getEqPredTys :: PredType -> (Type,Type)
getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
getEqPredTys other	      = pprPanic "getEqPredTys" (ppr other)

315
316
317
318
isIdentityCoercion :: Coercion -> Bool
isIdentityCoercion co  
  = case coercionKind co of
       (t1,t2) -> t1 `coreEqType` t2
319
\end{code}
320

321
322
323
324
325
%************************************************************************
%*									*
            Building coercions
%*									*
%************************************************************************
326

327
328
329
Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)

\begin{code}
batterseapower's avatar
batterseapower committed
330
331
332
-- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
-- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
-- if possible
333
mkCoercion :: TyCon -> [Type] -> Coercion
334
335
336
mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
                        TyConApp coCon args

337
338
339
mkCoVarCoercion :: CoVar -> Coercion 
mkCoVarCoercion cv = mkTyVarTy cv 

340
341
-- | Apply a 'Coercion' to another 'Coercion', which is presumably a
-- 'Coercion' constructor of some kind
batterseapower's avatar
batterseapower committed
342
mkAppCoercion :: Coercion -> Coercion -> Coercion
343
mkAppCoercion co1 co2 = mkAppTy co1 co2
batterseapower's avatar
batterseapower committed
344
345
346
347

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCoercion'
mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
348
349
350
351
352
353
354
355
mkAppsCoercion co1 tys = foldl mkAppTy co1 tys

-- | Apply a type constructor to a list of coercions.
mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
mkTyConCoercion con cos = mkTyConApp con cos

-- | Make a function 'Coercion' between two other 'Coercion's
mkFunCoercion :: Coercion -> Coercion -> Coercion
356
mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds!
batterseapower's avatar
batterseapower committed
357
358
359

-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
mkForAllCoercion :: Var -> Coercion -> Coercion
360
-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
361
mkForAllCoercion tv  co  = ASSERT ( isTyCoVar tv ) mkForAllTy tv co
batterseapower's avatar
batterseapower committed
362

363

364
-------------------------------
batterseapower's avatar
batterseapower committed
365
366

mkSymCoercion :: Coercion -> Coercion
367
368
369
-- ^ Create a symmetric version of the given 'Coercion' that asserts equality
-- between the same types but in the other "direction", so a kind of @t1 ~ t2@ 
-- becomes the kind @t2 ~ t1@.
370
mkSymCoercion g = mkCoercion symCoercionTyCon [g]
batterseapower's avatar
batterseapower committed
371
372
373

mkTransCoercion :: Coercion -> Coercion -> Coercion
-- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
374
mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
batterseapower's avatar
batterseapower committed
375
376
377
378
379
380

mkLeftCoercion :: Coercion -> Coercion
-- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of 
-- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
--
-- > mkLeftCoercion c :: f ~ g
381
mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
382

batterseapower's avatar
batterseapower committed
383
384
385
386
387
mkRightCoercion :: Coercion -> Coercion
-- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of 
-- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then:
--
-- > mkLeftCoercion c :: x ~ y
388
mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
batterseapower's avatar
batterseapower committed
389

390
391
392
393
394
395
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]

-------------------------------
batterseapower's avatar
batterseapower committed
396
397
398
mkInstCoercion :: Coercion -> Type -> Coercion
-- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
-- the resulting beta-reduction, otherwise it creates a suspended instantiation.
399
mkInstCoercion co ty = mkCoercion instCoercionTyCon  [co, ty]
400

batterseapower's avatar
batterseapower committed
401
402
mkInstsCoercion :: Coercion -> [Type] -> Coercion
-- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right
403
404
mkInstsCoercion co tys = foldl mkInstCoercion co tys

batterseapower's avatar
batterseapower committed
405
406
407
-- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
-- but it is used when we know we are dealing with bottom, which is one case in which 
-- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
408
-- Optimise by pushing down through type constructors
409
mkUnsafeCoercion :: Type -> Type -> Coercion
410
411
412
mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2)
  | tc1 == tc2
  = TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2)
413

414
415
416
417
418
419
mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2)
  = FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2)

mkUnsafeCoercion ty1 ty2 
  | ty1 `coreEqType` ty2 = ty1
  | otherwise            = mkCoercion unsafeCoercionTyCon [ty1, ty2]
420

421
-- See note [Newtype coercions] in TyCon
batterseapower's avatar
batterseapower committed
422
423
424
425
426

-- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a
-- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the
-- type the appropriate right hand side of the @newtype@, with the free variables
-- a subset of those 'TyVar's.
427
428
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
mkNewTypeCoercion name tycon tvs rhs_ty
429
  = mkCoercionTyCon name arity desc
430
  where
431
432
433
434
    arity = length tvs
    desc = CoAxiom { co_ax_tvs = tvs 
                   , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
                   , co_ax_rhs = rhs_ty }
435

batterseapower's avatar
batterseapower committed
436
-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
437
-- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 
batterseapower's avatar
batterseapower committed
438
-- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
439
-- representation tycon.
batterseapower's avatar
batterseapower committed
440
441
442
443
444
445
mkFamInstCoercion :: Name	-- ^ Unique name for the coercion tycon
		  -> [TyVar]	-- ^ Type parameters of the coercion (@tvs@)
		  -> TyCon	-- ^ Family tycon (@F@)
		  -> [Type]	-- ^ Type instance (@ts@)
		  -> TyCon	-- ^ Representation tycon (@R@)
		  -> TyCon	-- ^ Coercion tycon (@Co@)
446
447
mkFamInstCoercion name tvs family inst_tys rep_tycon
  = mkCoercionTyCon name arity desc
448
  where
449
450
451
452
    arity = length tvs
    desc = CoAxiom { co_ax_tvs = tvs
                   , co_ax_lhs = mkTyConApp family inst_tys 
                   , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
453
454
455
456
457
458
459
460
461
462


mkClassPPredCo :: Class -> [Coercion] -> Coercion
mkClassPPredCo cls = (PredTy . ClassP cls)

mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion
mkIParamPredCo ipn = (PredTy . IParam ipn)



463
\end{code}
464

465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482

%************************************************************************
%*									*
            Coercion Type Constructors
%*									*
%************************************************************************

Example.  The coercion ((sym c) (sym d) (sym e))
will be represented by (TyConApp sym [c, sym d, sym e])
If sym c :: p1=q1
   sym d :: p2=q2
   sym e :: p3=q3
then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)

\begin{code}
-- | Coercion type constructors: avoid using these directly and instead use 
-- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
--
483
-- Each coercion TyCon is built with the special CoercionTyCon record and
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
484
-- carries its own kinding rule.  Such CoercionTyCons must be fully applied
485
486
-- by any TyConApp in which they are applied, however they may also be over
-- applied (see example above) and the kinding function must deal with this.
487
488
489
490
symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, 
  rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
  csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon

491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
symCoercionTyCon    = mkCoercionTyCon symCoercionTyConName   1 CoSym
transCoercionTyCon  = mkCoercionTyCon transCoercionTyConName 2 CoTrans
leftCoercionTyCon   = mkCoercionTyCon leftCoercionTyConName  1 CoLeft
rightCoercionTyCon  = mkCoercionTyCon rightCoercionTyConName 1 CoRight
instCoercionTyCon   =  mkCoercionTyCon instCoercionTyConName 2 CoInst
csel1CoercionTyCon  = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
csel2CoercionTyCon  = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
cselRCoercionTyCon  = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe

transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, 
   rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
   csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name

transCoercionTyConName 	= mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
symCoercionTyConName   	= mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
leftCoercionTyConName  	= mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
rightCoercionTyConName 	= mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
instCoercionTyConName  	= mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon

mkCoConName :: FastString -> Unique -> TyCon -> Name
mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
                            key (ATyCon coCon) BuiltInSyntax
\end{code}

\begin{code}
------------
decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
523
524
525
-- Helper for left and right.  Finds coercion kind of its input and
-- returns the left and right projections of the coercion...
--
526
-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
527
decompLR_maybe (ty1,ty2)
528
  | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
529
  , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
530
  = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
531
decompLR_maybe _ = Nothing
532

533
534
535
------------
decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
decompInst_maybe (ty1, ty2)
536
537
538
  | Just (tv1,r1) <- splitForAllTy_maybe ty1
  , Just (tv2,r2) <- splitForAllTy_maybe ty2
  = Just ((tv1,tv2), (r1,r2))
539
decompInst_maybe _ = Nothing
540

541
542
------------
decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
543
--   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
544
545
546
-- Then   csel1 co ::            s1 ~ s2
--        csel2 co :: 		 t1 ~ t2
--        cselR co :: 		 r1 ~ r2
547
decompCsel_maybe (ty1, ty2)
548
549
550
  | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
  , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
  = Just ((s1,s2), (t1,t2), (r1,r2))
551
decompCsel_maybe _ = Nothing
552
\end{code}
553
554


555
556
557
558
559
%************************************************************************
%*									*
            Newtypes
%*									*
%************************************************************************
560

561
\begin{code}
562
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
batterseapower's avatar
batterseapower committed
563
564
565
-- ^ If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
566
567
568
569
570
instNewTyCon_maybe tc tys
  | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
  = ASSERT( tys `lengthIs` tyConArity tc )
    Just (substTyWith tvs tys ty, 
	  case mb_co_tc of
571
572
	     Nothing    -> IdCo (mkTyConApp tc    tys)
	     Just co_tc -> ACo  (mkTyConApp co_tc tys))
573
574
575
  | otherwise
  = Nothing

576
577
-- this is here to avoid module loops
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
batterseapower's avatar
batterseapower committed
578
579
580
581
582
583
584
585
-- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
-- This function only strips *one layer* of @newtype@ off, so the caller will usually call
-- itself recursively. Furthermore, this function should only be applied to types of kind @*@,
-- hence the newtype is always saturated. If @co : ty ~ ty'@ then:
--
-- > splitNewTypeRepCo_maybe ty = Just (ty', co)
--
-- The function returns @Nothing@ for non-@newtypes@ or fully-transparent @newtype@s.
586
587
588
splitNewTypeRepCo_maybe ty 
  | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
589
590
591
  | Just (ty', coi) <- instNewTyCon_maybe tc tys
  = case coi of
	ACo co -> Just (ty', co)
592
	IdCo _ -> panic "splitNewTypeRepCo_maybe"
593
			-- This case handled by coreView
594
splitNewTypeRepCo_maybe _
595
  = Nothing
596

batterseapower's avatar
batterseapower committed
597
-- | Determines syntactic equality of coercions
598
599
coreEqCoercion :: Coercion -> Coercion -> Bool
coreEqCoercion = coreEqType
600
601
602

coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
coreEqCoercion2 = coreEqType2
603
\end{code}
TomSchrijvers's avatar
TomSchrijvers committed
604
605


606
607
608
609
610
611
%************************************************************************
%*									*
            CoercionI and its constructors
%*									*
%************************************************************************

TomSchrijvers's avatar
TomSchrijvers committed
612
613
614
615
616
--------------------------------------
-- CoercionI smart constructors
--	lifted smart constructors of ordinary coercions

\begin{code}
batterseapower's avatar
batterseapower committed
617
618
619
620
621
622
-- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
-- can represent either one of:
--
-- 1. A proper 'Coercion'
--
-- 2. The identity coercion
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
data CoercionI = IdCo Type | ACo Coercion

liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
liftCoI f (IdCo ty) = IdCo (f ty)
liftCoI f (ACo ty)  = ACo (f ty)

liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
liftCoI2 f coi1       coi2       = ACo (f (fromCoI coi1) (fromCoI coi2))

liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
liftCoIs f cois = go_id [] cois
  where
    go_id rev_tys []               = IdCo (f (reverse rev_tys))
    go_id rev_tys (IdCo ty : cois) = go_id  (ty:rev_tys) cois
    go_id rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois

    go_aco rev_tys []               = ACo (f (reverse rev_tys))
    go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
    go_aco rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
TomSchrijvers's avatar
TomSchrijvers committed
643

644
instance Outputable CoercionI where
645
  ppr (IdCo _) = ptext (sLit "IdCo")
646
647
  ppr (ACo co) = ppr co

648
isIdentityCoI :: CoercionI -> Bool
649
650
isIdentityCoI (IdCo _) = True
isIdentityCoI (ACo _)  = False
651

batterseapower's avatar
batterseapower committed
652
653
-- | Return either the 'Coercion' contained within the 'CoercionI' or the given
-- 'Type' if the 'CoercionI' is the identity 'Coercion'
654
655
656
fromCoI :: CoercionI -> Type
fromCoI (IdCo ty) = ty	-- Identity coercion represented 
fromCoI (ACo co)  = co	-- 	by the type itself
657

batterseapower's avatar
batterseapower committed
658
-- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
659
mkSymCoI :: CoercionI -> CoercionI
660
661
mkSymCoI (IdCo ty) = IdCo ty
mkSymCoI (ACo co)  = ACo $ mkCoercion symCoercionTyCon [co] 
TomSchrijvers's avatar
TomSchrijvers committed
662
663
664
				-- the smart constructor
				-- is too smart with tyvars

batterseapower's avatar
batterseapower committed
665
-- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
666
mkTransCoI :: CoercionI -> CoercionI -> CoercionI
667
668
mkTransCoI (IdCo _) aco = aco
mkTransCoI aco (IdCo _) = aco
TomSchrijvers's avatar
TomSchrijvers committed
669
670
mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2

batterseapower's avatar
batterseapower committed
671
-- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
672
673
mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
TomSchrijvers's avatar
TomSchrijvers committed
674

batterseapower's avatar
batterseapower committed
675
-- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
676
677
mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
mkAppTyCoI = liftCoI2 mkAppTy
678

679
680
mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
mkFunTyCoI = liftCoI2 mkFunTy
TomSchrijvers's avatar
TomSchrijvers committed
681

batterseapower's avatar
batterseapower committed
682
-- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
683
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
684
mkForAllTyCoI tv = liftCoI (ForAllTy tv)
685

batterseapower's avatar
batterseapower committed
686
687
688
-- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
--
-- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
689
690
mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
TomSchrijvers's avatar
TomSchrijvers committed
691

batterseapower's avatar
batterseapower committed
692
-- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
TomSchrijvers's avatar
TomSchrijvers committed
693
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
694
mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
TomSchrijvers's avatar
TomSchrijvers committed
695

batterseapower's avatar
batterseapower committed
696
-- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
697
698
mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
699
700
701
702
703

mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI 
mkCoPredCoI coi1 coi2 coi3 =   mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3


TomSchrijvers's avatar
TomSchrijvers committed
704
\end{code}
705
706

%************************************************************************
707
708
709
%*									*
	     The kind of a type, and of a coercion
%*									*
710
711
712
%************************************************************************

\begin{code}
713
714
715
typeKind :: Type -> Kind
typeKind ty@(TyConApp tc tys) 
  | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
716
  | otherwise          = kindAppResult (tyConKind tc) tys
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
	-- During coercion optimisation we *do* match a type
	-- against a coercion (see OptCoercion.matchesAxiomLhs)
	-- So the use of typeKind in Unify.match_kind must work on coercions too
	-- Hence the isCoercionTyCon case above

typeKind (PredTy pred)	      = predKind pred
typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
typeKind (ForAllTy _ ty)      = typeKind ty
typeKind (TyVarTy tyvar)      = tyVarKind tyvar
typeKind (FunTy _arg res)
    -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
    --              not unliftedTypKind (#)
    -- The only things that can be after a function arrow are
    --   (a) types (of kind openTypeKind or its sub-kinds)
    --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
    | isTySuperKind k         = k
    | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
    where
      k = typeKind res

------------------
predKind :: PredType -> Kind
predKind (EqPred {}) = coSuperKind	-- A coercion kind!
predKind (ClassP {}) = liftedTypeKind	-- Class and implicitPredicates are
predKind (IParam {}) = liftedTypeKind 	-- always represented by lifted types

------------------
-- | If it is the case that
--
-- > c :: (t1 ~ t2)
--
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
748
749
-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, 
-- then @coercionKind c = (t1, t2)@.
750
751
752
753
754
755
756
757
758
759
760
761
762
763
coercionKind :: Coercion -> (Type, Type)
coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
                            | otherwise = (ty, ty)
coercionKind (AppTy ty1 ty2) 
  = let (s1, t1) = coercionKind ty1
        (s2, t2) = coercionKind ty2 in
    (mkAppTy s1 s2, mkAppTy t1 t2)
coercionKind co@(TyConApp tc args)
  | Just (ar, desc) <- isCoercionTyCon_maybe tc 
    -- CoercionTyCons carry their kinding rule, so we use it here
  = WARN( not (length args >= ar), ppr co )	-- Always saturated
    (let (ty1,  ty2)  = coTyConAppKind desc (take ar args)
	 (tys1, tys2) = coercionKinds (drop ar args)
     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
764

765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
  | otherwise
  = let (lArgs, rArgs) = coercionKinds args in
    (TyConApp tc lArgs, TyConApp tc rArgs)

coercionKind (FunTy ty1 ty2) 
  = let (t1, t2) = coercionKind ty1
        (s1, s2) = coercionKind ty2 in
    (mkFunTy t1 s1, mkFunTy t2 s2)

coercionKind (ForAllTy tv ty)
  | isCoVar tv
--     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
--    ----------------------------------------------
--    c1~c2 => c3  ::  (s1~t1) => r1 ~ (s2~t2) => r2
--      or
--    forall (_:c1~c2)
  = let (c1,c2) = coVarKind tv
    	(s1,s2) = coercionKind c1
    	(t1,t2) = coercionKind c2
    	(r1,r2) = coercionKind ty
    in
    (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
787
788

  | otherwise
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
--     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
--   ----------------------------------------------
--    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
  = let (ty1, ty2) = coercionKind ty in
    (ForAllTy tv ty1, ForAllTy tv ty2)

coercionKind (PredTy (ClassP cl args)) 
  = let (lArgs, rArgs) = coercionKinds args in
    (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
coercionKind (PredTy (IParam name ty))
  = let (ty1, ty2) = coercionKind ty in
    (PredTy (IParam name ty1), PredTy (IParam name ty2))
coercionKind (PredTy (EqPred c1 c2)) 
  = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
  -- These should not show up in coercions at all
  -- becuase they are in the form of for-alls
    let k1 = coercionKindPredTy c1
        k2 = coercionKindPredTy c2 in
    (k1,k2)
808
  where
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
    coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2

------------------
-- | Apply 'coercionKind' to multiple 'Coercion's
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys

------------------
-- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
-- and constructs the types that the resulting coercion relates.
-- Fails (in the monad) if ill-kinded.
-- Typically the monad is 
--   either the Lint monad (with the consistency-check flag = True), 
--   or the ID monad with a panic on failure (and the consistency-check flag = False)
coTyConAppKind 
    :: CoTyConDesc
    -> [Type]	  		-- Exactly right number of args
    -> (Type, Type)		-- Kind of this application
coTyConAppKind CoUnsafe (ty1:ty2:_)
  = (ty1,ty2)
coTyConAppKind CoSym (co:_) 
  | (ty1,ty2) <- coercionKind co = (ty2,ty1)
coTyConAppKind CoTrans (co1:co2:_) 
  = (fst (coercionKind co1), snd (coercionKind co2))
coTyConAppKind CoLeft (co:_) 
  | Just (res,_) <- decompLR_maybe (coercionKind co) = res
coTyConAppKind CoRight (co:_) 
  | Just (_,res) <- decompLR_maybe (coercionKind co) = res
coTyConAppKind CoCsel1 (co:_) 
  | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
coTyConAppKind CoCsel2 (co:_) 
  | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
coTyConAppKind CoCselR (co:_) 
  | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
coTyConAppKind CoInst (co:ty:_) 
  | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
  = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2) 
coTyConAppKind (CoAxiom { co_ax_tvs = tvs 
                        , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
  = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
849
  where
850
    (tys1, tys2) = coercionKinds cos
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
851
852
853
854
coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat 
                             [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
                             | co <- cos ])) $
                          coercionKind (head cos)
855
\end{code}