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

\begin{code}
6
{-# OPTIONS -fno-warn-incomplete-patterns #-}
7
8
9
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
Ian Lynagh's avatar
Ian Lynagh committed
10
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
11
12
-- for details

batterseapower's avatar
batterseapower committed
13
14
15
16
17
18
19
-- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for
-- more on System FC and how coercions fit into it.
--
-- Coercions are represented as types, and their kinds tell what types the 
-- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
--
-- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
20
module Coercion (
batterseapower's avatar
batterseapower committed
21
        -- * Main data type
22
23
24
25
26
        Coercion,
 
        mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
        coercionKind, coercionKinds, coercionKindPredTy,

batterseapower's avatar
batterseapower committed
27
	-- ** Equality predicates
28
29
	isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  

batterseapower's avatar
batterseapower committed
30
	-- ** Coercion transformations
31
	mkCoercion,
32
        mkSymCoercion, mkTransCoercion,
33
34
        mkLeftCoercion, mkRightCoercion, mkRightCoercions,
	mkInstCoercion, mkAppCoercion,
35
        mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
36
        mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
37

38
        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
39
40
41

        unsafeCoercionTyCon, symCoercionTyCon,
        transCoercionTyCon, leftCoercionTyCon, 
TomSchrijvers's avatar
TomSchrijvers committed
42
43
        rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn

batterseapower's avatar
batterseapower committed
44
        -- ** Comparison
45
46
        coreEqCoercion,

batterseapower's avatar
batterseapower committed
47
	-- * CoercionI
TomSchrijvers's avatar
TomSchrijvers committed
48
49
50
51
	CoercionI(..),
	isIdentityCoercion,
	mkSymCoI, mkTransCoI, 
	mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
52
	mkForAllTyCoI,
53
54
	fromCoI, fromACo,
	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
TomSchrijvers's avatar
TomSchrijvers committed
55

56
57
58
59
60
       ) where 

#include "HsVersions.h"

import TypeRep
61
62
import Type
import TyCon
TomSchrijvers's avatar
TomSchrijvers committed
63
import Class
64
import Var
65
66
67
68
69
70
import Name
import OccName
import PrelNames
import Util
import Unique
import BasicTypes
71
import Outputable
72
import FastString
73

batterseapower's avatar
batterseapower committed
74
-- | A 'Coercion' represents a 'Type' something should be coerced to.
75
type Coercion     = Type
batterseapower's avatar
batterseapower committed
76

77
-- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
batterseapower's avatar
batterseapower committed
78
79
-- types that a 'Coercion' will work on.
type CoercionKind = Kind
80

81
------------------------------
batterseapower's avatar
batterseapower committed
82

83
84
-- | 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
85
86
--
-- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
87
88
89
90
decomposeCo :: Arity -> Coercion -> [Coercion]
decomposeCo n co
  = go n co []
  where
91
    go 0 _  cos = cos
92
93
94
95
96
97
98
99
    go n co cos = go (n-1) (mkLeftCoercion co)
			   (mkRightCoercion co : cos)

------------------------------

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

batterseapower's avatar
batterseapower committed
100
-- | Tests whether a type is just a type equality predicate
101
isEqPredTy :: Type -> Bool
102
isEqPredTy (PredTy pred) = isEqPred pred
103
isEqPredTy _             = False
104

batterseapower's avatar
batterseapower committed
105
-- | Creates a type equality predicate
106
107
108
mkEqPred :: (Type, Type) -> PredType
mkEqPred (ty1, ty2) = EqPred ty1 ty2

batterseapower's avatar
batterseapower committed
109
110
-- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
-- Panics otherwise
111
112
113
114
getEqPredTys :: PredType -> (Type,Type)
getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
getEqPredTys other	      = pprPanic "getEqPredTys" (ppr other)

batterseapower's avatar
batterseapower committed
115
-- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
116
117
118
mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)

batterseapower's avatar
batterseapower committed
119
-- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
120
121
122
mkReflCoKind :: Type -> CoercionKind
mkReflCoKind ty = mkCoKind ty ty

batterseapower's avatar
batterseapower committed
123
124
-- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
-- Panics if the argument is not a valid 'CoercionKind'
125
126
127
128
splitCoercionKind :: CoercionKind -> (Type, Type)
splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)

batterseapower's avatar
batterseapower committed
129
-- | Take a 'CoercionKind' apart into the two types it relates, if possible. See also 'splitCoercionKind'
130
131
132
splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
133
splitCoercionKind_maybe _ = Nothing
134

batterseapower's avatar
batterseapower committed
135
136
-- | If it is the case that
--
137
-- > c :: (t1 ~ t2)
batterseapower's avatar
batterseapower committed
138
139
140
--
-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
-- See also 'coercionKindPredTy'
141
coercionKind :: Coercion -> (Type, Type)
142
143
coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
                            | otherwise = (ty, ty)
144
145
146
147
148
149
coercionKind (AppTy ty1 ty2) 
  = let (t1, t2) = coercionKind ty1
        (s1, s2) = coercionKind ty2 in
    (mkAppTy t1 s1, mkAppTy t2 s2)
coercionKind (TyConApp tc args)
  | Just (ar, rule) <- isCoercionTyCon_maybe tc 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
150
    -- CoercionTyCons carry their kinding rule, so we use it here
151
152
153
154
155
  = ASSERT( length args >= ar )	-- Always saturated
    let (ty1,ty2)    = rule (take ar args)	-- Apply the rule to the right number of args
	(tys1, tys2) = coercionKinds (drop ar args)
    in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)

156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
  | 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) 
  = let (ty1, ty2) = coercionKind ty in
    (ForAllTy tv ty1, ForAllTy tv ty2)
coercionKind (PredTy (EqPred c1 c2)) 
  = let k1 = coercionKindPredTy c1
        k2 = coercionKindPredTy c2 in
    (k1,k2)
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))

batterseapower's avatar
batterseapower committed
177
178
-- | Recover the 'CoercionKind' corresponding to a particular 'Coerceion'. See also 'coercionKind'
-- and 'mkCoKind'
179
180
181
coercionKindPredTy :: Coercion -> CoercionKind
coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2

batterseapower's avatar
batterseapower committed
182
-- | Apply 'coercionKind' to multiple 'Coercion's
183
184
185
186
187
188
189
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys

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

batterseapower's avatar
batterseapower committed
190
191
192
-- | 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
193
mkCoercion :: TyCon -> [Type] -> Coercion
194
195
196
mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
                        TyConApp coCon args

batterseapower's avatar
batterseapower committed
197
198
199
-- | Apply a 'Coercion' to another 'Coercion', which is presumably a 'Coercion' constructor of some
-- kind
mkAppCoercion :: Coercion -> Coercion -> Coercion
200
mkAppCoercion    co1 co2 = mkAppTy co1 co2
batterseapower's avatar
batterseapower committed
201
202
203
204

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCoercion'
mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
205
mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
batterseapower's avatar
batterseapower committed
206
207
208

-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
mkForAllCoercion :: Var -> Coercion -> Coercion
209
210
-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
batterseapower's avatar
batterseapower committed
211
212
213

-- | Make a function 'Coercion' between two other 'Coercion's
mkFunCoercion :: Coercion -> Coercion -> Coercion
214
215
mkFunCoercion    co1 co2 = mkFunTy co1 co2

216

217
-------------------------------
batterseapower's avatar
batterseapower committed
218
219
220

mkSymCoercion :: Coercion -> Coercion
-- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
221
222
-- the same types but in the other "direction", so a kind of @t1 ~ t2@ becomes the
-- kind @t2 ~ t1@.
batterseapower's avatar
batterseapower committed
223
224
225
226
--
-- This function attempts to simplify the generated 'Coercion' by removing redundant applications
-- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that 
-- @sym (sym co) = co@.
227
mkSymCoercion co      
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
  | Just co' <- coreView co = mkSymCoercion co'

mkSymCoercion (ForAllTy tv ty)  = ForAllTy tv (mkSymCoercion ty)
mkSymCoercion (AppTy co1 co2) 	= AppTy (mkSymCoercion co1) (mkSymCoercion co2)
mkSymCoercion (FunTy co1 co2) 	= FunTy (mkSymCoercion co1) (mkSymCoercion co2)

mkSymCoercion (TyConApp tc cos) 
  | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos)

mkSymCoercion (TyConApp tc [co]) 
  | tc `hasKey` symCoercionTyConKey   = co    -- sym (sym co) --> co
  | tc `hasKey` leftCoercionTyConKey  = mkLeftCoercion (mkSymCoercion co)
  | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co)

mkSymCoercion (TyConApp tc [co1,co2]) 
  | tc `hasKey` transCoercionTyConKey
244
     -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
245
     -- Note reversal of arguments!
246
  = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
247
248

  | tc `hasKey` instCoercionTyConKey
249
     -- sym (co @ ty) --> (sym co) @ ty
250
251
252
253
254
255
     -- Note: sym is not applied to 'ty'
  = mkInstCoercion (mkSymCoercion co1) co2

mkSymCoercion (TyConApp tc cos) 	-- Other coercion tycons, such as those
  = mkCoercion symCoercionTyCon [TyConApp tc cos]  -- arising from newtypes

256
257
mkSymCoercion (TyVarTy tv) 
  | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
258
259
260
261
  | otherwise  = TyVarTy tv	-- Reflexive

-------------------------------
-- ToDo: we should be cleverer about transitivity
batterseapower's avatar
batterseapower committed
262
263
264
265
266
267

mkTransCoercion :: Coercion -> Coercion -> Coercion
-- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
-- 
-- This function attempts to simplify the generated 'Coercion' by exploiting the fact that
-- @sym g `trans` g = id@.
268
269
270
271
272
273
274
275
mkTransCoercion g1 g2	-- sym g `trans` g = id
  | (t1,_) <- coercionKind g1
  , (_,t2) <- coercionKind g2
  , t1 `coreEqType` t2 
  = t1	

  | otherwise
  = mkCoercion transCoercionTyCon [g1, g2]
276

277
278

-------------------------------
279
-- Smart constructors for left and right
batterseapower's avatar
batterseapower committed
280
281
282
283
284
285

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
286
287
mkLeftCoercion co 
  | Just (co', _) <- splitAppCoercion_maybe co = co'
288
  | otherwise = mkCoercion leftCoercionTyCon [co]
289

batterseapower's avatar
batterseapower committed
290
291
292
293
294
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
295
mkRightCoercion  co      
296
  | Just (_, co2) <- splitAppCoercion_maybe co = co2
297
298
  | otherwise = mkCoercion rightCoercionTyCon [co]

299
mkRightCoercions :: Int -> Coercion -> [Coercion]
batterseapower's avatar
batterseapower committed
300
301
302
-- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@
-- nested application 'Coercion's, manufacturing new left or right cooercions as necessary
-- if suffficiently many are not directly available.
303
304
305
306
307
308
309
310
311
312
313
mkRightCoercions n co
  = go n co []
  where
    go n co acc 
       | n > 0
       = case splitAppCoercion_maybe co of
          Just (co1,co2) -> go (n-1) co1 (co2:acc)
          Nothing        -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc)
       | otherwise
       = acc

batterseapower's avatar
batterseapower committed
314
315
316
317

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.
318
319
320
321
322
mkInstCoercion co ty
  | Just (tv,co') <- splitForAllTy_maybe co
  = substTyWith [tv] [ty] co'	-- (forall a.co) @ ty  -->  co[ty/a]
  | otherwise
  = mkCoercion instCoercionTyCon  [co, ty]
323

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

328
{-
329
330
331
332
333
334
splitSymCoercion_maybe :: Coercion -> Maybe Coercion
splitSymCoercion_maybe (TyConApp tc [co]) = 
  if tc `hasKey` symCoercionTyConKey
  then Just co
  else Nothing
splitSymCoercion_maybe co = Nothing
335
-}
336
337

splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
batterseapower's avatar
batterseapower committed
338
339
-- ^ Splits a coercion application, being careful *not* to split @left c@ etc.
-- This is because those are really syntactic constructs, not applications
340
341
342
343
344
345
346
347
splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
splitAppCoercion_maybe (TyConApp tc tys) 
   | not (isCoercionTyCon tc)
   = case snocView tys of
       Just (tys', ty') -> Just (TyConApp tc tys', ty')
       Nothing          -> Nothing
348
splitAppCoercion_maybe _ = Nothing
349

350
{-
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) 
 = if tc `hasKey` transCoercionTyConKey then
       Just (ty1, ty2)
   else
       Nothing
splitTransCoercion_maybe other = Nothing

splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type)
splitInstCoercion_maybe (TyConApp tc [ty1, ty2])
 = if tc `hasKey` instCoercionTyConKey then
       Just (ty1, ty2)
    else
       Nothing
splitInstCoercion_maybe other = Nothing

splitLeftCoercion_maybe :: Coercion -> Maybe Coercion
splitLeftCoercion_maybe (TyConApp tc [co])
 = if tc `hasKey` leftCoercionTyConKey then
       Just co
   else
       Nothing
splitLeftCoercion_maybe other = Nothing

splitRightCoercion_maybe :: Coercion -> Maybe Coercion
splitRightCoercion_maybe (TyConApp tc [co])
 = if tc `hasKey` rightCoercionTyConKey then
       Just co
   else
       Nothing
splitRightCoercion_maybe other = Nothing
382
-}
383

batterseapower's avatar
batterseapower committed
384
385
386
-- | 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.
387
388
389
390
391
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion ty1 ty2 
  = mkCoercion unsafeCoercionTyCon [ty1, ty2]


392
-- See note [Newtype coercions] in TyCon
batterseapower's avatar
batterseapower committed
393
394
395
396
397

-- | 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.
398
399
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
mkNewTypeCoercion name tycon tvs rhs_ty
400
  = mkCoercionTyCon name co_con_arity rule
401
  where
402
403
    co_con_arity = length tvs

404
405
    rule args = ASSERT( co_con_arity == length args )
		(TyConApp tycon args, substTyWith tvs args rhs_ty)
406

batterseapower's avatar
batterseapower committed
407
-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
408
-- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 
batterseapower's avatar
batterseapower committed
409
-- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
410
-- representation tycon.
batterseapower's avatar
batterseapower committed
411
412
413
414
415
416
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@)
417
mkFamInstCoercion name tvs family instTys rep_tycon
418
  = mkCoercionTyCon name coArity rule
419
420
  where
    coArity = length tvs
421
    rule args = (substTyWith tvs args $		     -- with sigma = [tys/tvs],
422
		   TyConApp family instTys,	     --       sigma (F ts)
423
		 TyConApp rep_tycon args)	     --   ~ R tys
424

425
426
427
428
429
430
431
432
433
434
--------------------------------------
-- 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)

batterseapower's avatar
batterseapower committed
435
436
-- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family
-- of functions if possible.
437
symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
438
-- Each coercion TyCon is built with the special CoercionTyCon record and
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
439
-- carries its own kinding rule.  Such CoercionTyCons must be fully applied
440
441
442
-- 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.
symCoercionTyCon = 
443
  mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
444
  where
445
    flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
446
447
448
449
	where
	  (ty1, ty2) = coercionKind co

transCoercionTyCon = 
450
  mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
451
  where
452
453
    composeCoercionKindsOf (co1:co2:rest)
      = ASSERT( null rest )
454
455
456
457
        WARN( not (r1 `coreEqType` a2), 
              text "Strange! Type mismatch in trans coercion, probably a bug"
              $$
              ppr r1 <+> text "=/=" <+> ppr a2)
458
        (a1, r2)
459
460
461
462
463
      where
        (a1, r1) = coercionKind co1
        (a2, r2) = coercionKind co2 

leftCoercionTyCon =
464
  mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
465
  where
466
    leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
467
468
469
470
      where
        (ty1,ty2) = fst (splitCoercionKindOf co)

rightCoercionTyCon =
471
  mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
472
  where
473
    rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
474
475
476
477
478
479
480
      where
        (ty1,ty2) = snd (splitCoercionKindOf co)

splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
-- Helper for left and right.  Finds coercion kind of its input and
-- returns the left and right projections of the coercion...
--
481
-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
482
483
484
485
486
splitCoercionKindOf co
  | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
  , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
  , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
  = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
487
488
489
splitCoercionKindOf co 
  = pprPanic "Coercion.splitCoercionKindOf" 
             (ppr co $$ ppr (coercionKindPredTy co))
490
491

instCoercionTyCon 
492
  =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
493
494
495
496
497
  where
    instantiateCo t s =
      let Just (tv, ty) = splitForAllTy_maybe t in
      substTyWith [tv] [s] ty

498
499
    instCoercionKind (co1:ty:rest) = ASSERT( null rest )
				     (instantiateCo t1 ty, instantiateCo t2 ty)
500
501
502
      where (t1, t2) = coercionKind co1

unsafeCoercionTyCon 
503
  = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
504
  where
505
   unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 
506
507
508
509
        
--------------------------------------
-- ...and their names

510
mkCoConName :: FastString -> Unique -> TyCon -> Name
batterseapower's avatar
batterseapower committed
511
mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
512
                            key (ATyCon coCon) BuiltInSyntax
513

514
515
transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name

Ian Lynagh's avatar
Ian Lynagh committed
516
517
518
519
520
521
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
unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
522
523
524



525
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
batterseapower's avatar
batterseapower committed
526
527
528
-- ^ If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
529
530
531
532
533
534
535
536
537
538
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
	   Nothing    -> IdCo
	   Just co_tc -> ACo (mkTyConApp co_tc tys))
  | otherwise
  = Nothing

539
540
-- this is here to avoid module loops
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
batterseapower's avatar
batterseapower committed
541
542
543
544
545
546
547
548
-- ^ 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.
549
550
551
splitNewTypeRepCo_maybe ty 
  | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
552
553
554
555
556
  | Just (ty', coi) <- instNewTyCon_maybe tc tys
  = case coi of
	ACo co -> Just (ty', co)
	IdCo   -> panic "splitNewTypeRepCo_maybe"
			-- This case handled by coreView
557
splitNewTypeRepCo_maybe _
558
  = Nothing
559

batterseapower's avatar
batterseapower committed
560
-- | Determines syntactic equality of coercions
561
562
coreEqCoercion :: Coercion -> Coercion -> Bool
coreEqCoercion = coreEqType
563
\end{code}
TomSchrijvers's avatar
TomSchrijvers committed
564
565
566
567
568
569
570


--------------------------------------
-- CoercionI smart constructors
--	lifted smart constructors of ordinary coercions

\begin{code}
batterseapower's avatar
batterseapower committed
571
572
573
574
575
576
-- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
-- can represent either one of:
--
-- 1. A proper 'Coercion'
--
-- 2. The identity coercion
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
577
data CoercionI = IdCo | ACo Coercion
TomSchrijvers's avatar
TomSchrijvers committed
578

579
580
581
582
instance Outputable CoercionI where
  ppr IdCo     = ptext (sLit "IdCo")
  ppr (ACo co) = ppr co

TomSchrijvers's avatar
TomSchrijvers committed
583
584
585
586
isIdentityCoercion :: CoercionI -> Bool
isIdentityCoercion IdCo = True
isIdentityCoercion _    = False

batterseapower's avatar
batterseapower committed
587
-- | Tests whether all the given 'CoercionI's represent the identity coercion
588
589
590
allIdCos :: [CoercionI] -> Bool
allIdCos = all isIdentityCoercion

batterseapower's avatar
batterseapower committed
591
592
-- | For each 'CoercionI' in the input list, return either the 'Coercion' it
-- contains or the corresponding 'Type' from the other list
593
594
595
zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
zipCoArgs cois tys = zipWith fromCoI cois tys

batterseapower's avatar
batterseapower committed
596
597
-- | Return either the 'Coercion' contained within the 'CoercionI' or the given
-- 'Type' if the 'CoercionI' is the identity 'Coercion'
598
599
fromCoI :: CoercionI -> Type -> Type
fromCoI IdCo ty     = ty	-- Identity coercion represented 
600
fromCoI (ACo co) _  = co	-- 	by the type itself
601

batterseapower's avatar
batterseapower committed
602
-- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
603
604
605
606
607
608
mkSymCoI :: CoercionI -> CoercionI
mkSymCoI IdCo = IdCo
mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] 
				-- the smart constructor
				-- is too smart with tyvars

batterseapower's avatar
batterseapower committed
609
-- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
610
611
612
613
614
mkTransCoI :: CoercionI -> CoercionI -> CoercionI
mkTransCoI IdCo aco = aco
mkTransCoI aco IdCo = aco
mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2

batterseapower's avatar
batterseapower committed
615
-- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
616
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
617
618
619
mkTyConAppCoI tyCon tys cois
  | allIdCos cois = IdCo
  | otherwise	  = ACo (TyConApp tyCon (zipCoArgs cois tys))
TomSchrijvers's avatar
TomSchrijvers committed
620

batterseapower's avatar
batterseapower committed
621
-- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
622
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
623
mkAppTyCoI _   IdCo _   IdCo = IdCo
TomSchrijvers's avatar
TomSchrijvers committed
624
625
626
mkAppTyCoI ty1 coi1 ty2 coi2 =
	ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)

batterseapower's avatar
batterseapower committed
627
-- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
628
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
629
mkFunTyCoI _   IdCo _   IdCo = IdCo
TomSchrijvers's avatar
TomSchrijvers committed
630
631
632
mkFunTyCoI ty1 coi1 ty2 coi2 =
	ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)

batterseapower's avatar
batterseapower committed
633
-- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
634
635
636
637
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co

batterseapower's avatar
batterseapower committed
638
639
-- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
-- panic
640
fromACo :: CoercionI -> Coercion
641
642
fromACo (ACo co) = co

batterseapower's avatar
batterseapower committed
643
644
645
-- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
--
-- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
TomSchrijvers's avatar
TomSchrijvers committed
646
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
647
648
649
mkClassPPredCoI cls tys cois 
  | allIdCos cois = IdCo
  | otherwise     = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
TomSchrijvers's avatar
TomSchrijvers committed
650

batterseapower's avatar
batterseapower committed
651
-- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
TomSchrijvers's avatar
TomSchrijvers committed
652
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
653
mkIParamPredCoI _   IdCo     = IdCo
TomSchrijvers's avatar
TomSchrijvers committed
654
655
mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co

batterseapower's avatar
batterseapower committed
656
-- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
TomSchrijvers's avatar
TomSchrijvers committed
657
658
659
mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkEqPredCoI _    IdCo     _   IdCo      = IdCo
mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
660
mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
TomSchrijvers's avatar
TomSchrijvers committed
661
\end{code}