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

\begin{code}
6
7
8
-- 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
9
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
10
11
-- for details

batterseapower's avatar
batterseapower committed
12
13
14
15
16
17
18
-- | 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]
19
module Coercion (
batterseapower's avatar
batterseapower committed
20
        -- * Main data type
21
22
        Coercion,
 
23
        mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
24
        coercionKind, coercionKinds, isIdentityCoercion,
25

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

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

38
        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
39
40
41

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

45
46
47
        -- ** Decomposition
        decompLR_maybe, decompCsel_maybe, decompInst_maybe,

48
49
50
        -- ** Optimisation
	optCoercion,

batterseapower's avatar
batterseapower committed
51
        -- ** Comparison
52
        coreEqCoercion, coreEqCoercion2,
53

batterseapower's avatar
batterseapower committed
54
	-- * CoercionI
TomSchrijvers's avatar
TomSchrijvers committed
55
	CoercionI(..),
56
	isIdentityCoI,
TomSchrijvers's avatar
TomSchrijvers committed
57
58
	mkSymCoI, mkTransCoI, 
	mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
59
	mkForAllTyCoI,
60
61
	fromCoI, fromACo,
	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
TomSchrijvers's avatar
TomSchrijvers committed
62

63
64
65
66
67
       ) where 

#include "HsVersions.h"

import TypeRep
68
69
import Type
import TyCon
TomSchrijvers's avatar
TomSchrijvers committed
70
import Class
71
import Var
72
import VarEnv
73
74
75
import Name
import PrelNames
import Util
76
import Control.Monad
77
import BasicTypes
78
import MonadUtils
79
import Outputable
80
import FastString
81

batterseapower's avatar
batterseapower committed
82
-- | A 'Coercion' represents a 'Type' something should be coerced to.
83
type Coercion     = Type
batterseapower's avatar
batterseapower committed
84

85
-- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the
batterseapower's avatar
batterseapower committed
86
87
-- types that a 'Coercion' will work on.
type CoercionKind = Kind
88

89
------------------------------
batterseapower's avatar
batterseapower committed
90

91
92
-- | 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
93
94
--
-- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
95
96
97
98
decomposeCo :: Arity -> Coercion -> [Coercion]
decomposeCo n co
  = go n co []
  where
99
    go 0 _  cos = cos
100
101
102
103
104
105
106
107
    go n co cos = go (n-1) (mkLeftCoercion co)
			   (mkRightCoercion co : cos)

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

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

108
109
coVarKind :: CoVar -> (Type,Type) 
-- c :: t1 ~ t2
110
111
112
113
114
115
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)
116
117
118

-- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
-- Panics if the argument is not a valid 'CoercionKind'
119
120
121
122
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
123

124
125
-- | Makes a 'CoercionKind' from two types: the types whose equality 
-- is proven by the relevant 'Coercion'
126
127
128
129
130
131
132
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
mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r

133
134
135
136
137
138
139
140
141
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
142
-- | Tests whether a type is just a type equality predicate
143
isEqPredTy :: Type -> Bool
144
isEqPredTy (PredTy pred) = isEqPred pred
145
isEqPredTy _             = False
146

batterseapower's avatar
batterseapower committed
147
-- | Creates a type equality predicate
148
149
150
mkEqPred :: (Type, Type) -> PredType
mkEqPred (ty1, ty2) = EqPred ty1 ty2

batterseapower's avatar
batterseapower committed
151
152
-- | Splits apart a type equality predicate, if the supplied 'PredType' is one.
-- Panics otherwise
153
154
155
156
getEqPredTys :: PredType -> (Type,Type)
getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
getEqPredTys other	      = pprPanic "getEqPredTys" (ppr other)

batterseapower's avatar
batterseapower committed
157
158
-- | If it is the case that
--
159
-- > c :: (t1 ~ t2)
batterseapower's avatar
batterseapower committed
160
161
--
-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
162
coercionKind :: Coercion -> (Type, Type)
163
coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
164
                            | otherwise = (ty, ty)
165
coercionKind (AppTy ty1 ty2) 
166
167
168
169
  = let (s1, t1) = coercionKind ty1
        (s2, t2) = coercionKind ty2 in
    (mkAppTy s1 s2, mkAppTy t1 t2)
coercionKind co@(TyConApp tc args)
170
  | Just (ar, rule) <- isCoercionTyCon_maybe tc 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
171
    -- CoercionTyCons carry their kinding rule, so we use it here
172
173
174
175
176
177
178
179
  = WARN( not (length args >= ar), ppr co )	-- Always saturated
    (let (ty1,ty2) = runID (rule (return . typeKind)
                                (return . coercionKind)
				False (take ar args))
	     	       	      -- Apply the rule to the right number of args
    	     	       	      -- Always succeeds (if term is well-kinded!)
	 (tys1, tys2) = coercionKinds (drop ar args)
     in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
180

181
182
183
184
185
186
187
  | 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)
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206

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)

  | otherwise
--     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
--   ----------------------------------------------
--    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
207
208
  = let (ty1, ty2) = coercionKind ty in
    (ForAllTy tv ty1, ForAllTy tv ty2)
209

210
coercionKind (PredTy (EqPred c1 c2)) 
211
212
  = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
    let k1 = coercionKindPredTy c1
213
214
        k2 = coercionKindPredTy c2 in
    (k1,k2)
215
216
217
218
219
220
221
  -- These should not show up in coercions at all
  -- becuase they are in the form of for-alls
  where
    coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2



222
223
224
225
226
227
228
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
229
-- | Apply 'coercionKind' to multiple 'Coercion's
230
231
232
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys

233
234
235
236
237
-------------------------------------
isIdentityCoercion :: Coercion -> Bool
isIdentityCoercion co  
  = case coercionKind co of
       (t1,t2) -> t1 `coreEqType` t2
238
\end{code}
239

240
241
242
243
244
%************************************************************************
%*									*
            Building coercions
%*									*
%************************************************************************
245

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

\begin{code}
batterseapower's avatar
batterseapower committed
249
250
251
-- | 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
252
mkCoercion :: TyCon -> [Type] -> Coercion
253
254
255
mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
                        TyConApp coCon args

256
257
-- | Apply a 'Coercion' to another 'Coercion', which is presumably a
-- 'Coercion' constructor of some kind
batterseapower's avatar
batterseapower committed
258
mkAppCoercion :: Coercion -> Coercion -> Coercion
259
mkAppCoercion co1 co2 = mkAppTy co1 co2
batterseapower's avatar
batterseapower committed
260
261
262
263

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCoercion'
mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
264
265
266
267
268
269
270
271
272
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
mkFunCoercion co1 co2 = mkFunTy co1 co2
batterseapower's avatar
batterseapower committed
273
274
275

-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
mkForAllCoercion :: Var -> Coercion -> Coercion
276
277
-- 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
278

279

280
-------------------------------
batterseapower's avatar
batterseapower committed
281
282

mkSymCoercion :: Coercion -> Coercion
283
284
285
-- ^ 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@.
286
mkSymCoercion g = mkCoercion symCoercionTyCon [g]
batterseapower's avatar
batterseapower committed
287
288
289

mkTransCoercion :: Coercion -> Coercion -> Coercion
-- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's.
290
mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2]
batterseapower's avatar
batterseapower committed
291
292
293
294
295
296

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
297
mkLeftCoercion co = mkCoercion leftCoercionTyCon [co]
298

batterseapower's avatar
batterseapower committed
299
300
301
302
303
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
304
mkRightCoercion co = mkCoercion rightCoercionTyCon [co]
batterseapower's avatar
batterseapower committed
305

306
307
308
309
310
311
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
312
313
314
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.
315
mkInstCoercion co ty = mkCoercion instCoercionTyCon  [co, ty]
316

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

batterseapower's avatar
batterseapower committed
321
322
323
-- | 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.
324
325
326
327
328
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion ty1 ty2 
  = mkCoercion unsafeCoercionTyCon [ty1, ty2]


329
-- See note [Newtype coercions] in TyCon
batterseapower's avatar
batterseapower committed
330
331
332
333
334

-- | 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.
335
336
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
mkNewTypeCoercion name tycon tvs rhs_ty
337
  = mkCoercionTyCon name co_con_arity rule
338
  where
339
340
    co_con_arity = length tvs

341
    rule :: CoTyConKindChecker
342
    rule kc_ty _kc_co checking args 
343
344
345
346
      = do { ks <- mapM kc_ty args
           ; unless (not checking || kindAppOk (tyConKind tycon) ks) 
                    (fail "Argument kind mis-match")
           ; return (TyConApp tycon args, substTyWith tvs args rhs_ty) }
347

batterseapower's avatar
batterseapower committed
348
-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
349
-- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 
batterseapower's avatar
batterseapower committed
350
-- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
351
-- representation tycon.
batterseapower's avatar
batterseapower committed
352
353
354
355
356
357
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@)
358
mkFamInstCoercion name tvs family instTys rep_tycon
359
  = mkCoercionTyCon name coArity rule
360
361
  where
    coArity = length tvs
362
363

    rule :: CoTyConKindChecker
364
    rule kc_ty _kc_co checking args 
365
366
367
368
369
370
371
372
      = do { ks <- mapM kc_ty args
           ; unless (not checking  || kindAppOk (tyConKind rep_tycon) ks)
                    (fail "Argument kind mis-match")
           ; return (substTyWith tvs args $	     -- with sigma = [tys/tvs],
		     TyConApp family instTys	     --       sigma (F ts)
		    , TyConApp rep_tycon args) }     --   ~ R tys

kindAppOk :: Kind -> [Kind] -> Bool
373
kindAppOk _   [] = True
374
375
376
377
kindAppOk kfn (k:ks) 
  = case splitKindFunTy_maybe kfn of
      Just (kfa, kfb) | k `isSubKind` kfa -> kindAppOk kfb ks
      _other                              -> False
378
\end{code}
379

380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397

%************************************************************************
%*									*
            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.
--
398
-- Each coercion TyCon is built with the special CoercionTyCon record and
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
399
-- carries its own kinding rule.  Such CoercionTyCons must be fully applied
400
401
-- 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.
402
403
404
405
symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, 
  rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
  csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon

406
407
symCoercionTyCon 
  = mkCoercionTyCon symCoercionTyConName 1 kc_sym
408
  where
409
    kc_sym :: CoTyConKindChecker
410
    kc_sym _kc_ty kc_co _ (co:_) 
411
412
      = do { (ty1,ty2) <- kc_co co
           ; return (ty2,ty1) }
413
    kc_sym _ _ _ _ = panic "kc_sym"
414

415
416
transCoercionTyCon 
  = mkCoercionTyCon transCoercionTyConName 2 kc_trans
417
  where
418
    kc_trans :: CoTyConKindChecker
419
    kc_trans _kc_ty kc_co checking (co1:co2:_)
420
421
422
423
424
      = do { (a1, r1) <- kc_co co1
           ; (a2, r2) <- kc_co co2 
	   ; unless (not checking || (r1 `coreEqType` a2))
                    (fail "Trans coercion mis-match")
           ; return (a1, r2) }
425
    kc_trans _ _ _ _ = panic "kc_sym"
426

427
---------------------------------------------------
428
429
430
431
leftCoercionTyCon  = mkCoercionTyCon leftCoercionTyConName  1 (kcLR_help fst)
rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (kcLR_help snd)

kcLR_help :: (forall a. (a,a)->a) -> CoTyConKindChecker
432
kcLR_help select _kc_ty kc_co _checking (co : _)
433
434
435
436
  = do { (ty1, ty2)  <- kc_co co
       ; case decompLR_maybe ty1 ty2 of
           Nothing  -> fail "decompLR" 
           Just res -> return (select res) }
437
kcLR_help _ _ _ _ _ = panic "kcLR_help"
438

439
decompLR_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type))
440
441
442
-- Helper for left and right.  Finds coercion kind of its input and
-- returns the left and right projections of the coercion...
--
443
-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
444
445
decompLR_maybe ty1 ty2
  | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
446
  , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
447
448
  = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
decompLR_maybe _ _ = Nothing
449

450
---------------------------------------------------
451
instCoercionTyCon 
452
  =  mkCoercionTyCon instCoercionTyConName 2 kcInst_help
453
  where
454
455
456
457
458
459
460
461
462
463
464
    kcInst_help :: CoTyConKindChecker
    kcInst_help kc_ty kc_co checking (co : ty : _)
      = do { (t1,t2) <- kc_co co
           ; k <- kc_ty ty
           ; case decompInst_maybe t1 t2 of
               Nothing -> fail "decompInst"
               Just ((tv1,tv2), (ty1,ty2)) -> do
           { unless (not checking || (k `isSubKind` tyVarKind tv1))
                    (fail "Coercion instantation kind mis-match")
           ; return (substTyWith [tv1] [ty] ty1,
                     substTyWith [tv2] [ty] ty2) } }
465
    kcInst_help _ _ _ _ = panic "kcInst_help"
466
467
468
469
470
471

decompInst_maybe :: Type -> Type -> Maybe ((TyVar,TyVar), (Type,Type))
decompInst_maybe ty1 ty2
  | Just (tv1,r1) <- splitForAllTy_maybe ty1
  , Just (tv2,r2) <- splitForAllTy_maybe ty2
  = Just ((tv1,tv2), (r1,r2))
472
decompInst_maybe _ _ = Nothing
473

474
---------------------------------------------------
475
unsafeCoercionTyCon 
476
  = mkCoercionTyCon unsafeCoercionTyConName 2 kc_unsafe
477
  where
478
479
480
   kc_unsafe kc_ty _kc_co _checking (ty1:ty2:_) 
    = do { _ <- kc_ty ty1
         ; _ <- kc_ty ty2
481
         ; return (ty1,ty2) }
482
   kc_unsafe _ _ _ _ = panic "kc_unsafe"
483
        
484
485
---------------------------------------------------
-- The csel* family
486
487
488
489
490
491

csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (kcCsel_help fstOf3)
csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (kcCsel_help sndOf3)
cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (kcCsel_help thirdOf3) 

kcCsel_help :: (forall a. (a,a,a) -> a) -> CoTyConKindChecker
492
kcCsel_help select _kc_ty kc_co _checking (co : _)
493
494
495
496
  = do { (ty1,ty2) <- kc_co co
       ; case decompCsel_maybe ty1 ty2 of
           Nothing  -> fail "decompCsel"
           Just res -> return (select res) }
497
kcCsel_help _ _ _ _ _ = panic "kcCsel_help"
498
499

decompCsel_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type), (Type,Type))
500
--   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
501
502
503
504
505
506
507
508
-- Then   csel1 co ::            s1 ~ s2
--        csel2 co :: 		 t1 ~ t2
--        cselR co :: 		 r1 ~ r2
decompCsel_maybe ty1 ty2
  | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
  , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
  = Just ((s1,s2), (t1,t2), (r1,r2))
decompCsel_maybe _ _ = Nothing
509
510
511
512
513
514
515
516

fstOf3   :: (a,b,c) -> a    
sndOf3   :: (a,b,c) -> b    
thirdOf3 :: (a,b,c) -> c    
fstOf3      (a,_,_) =  a
sndOf3      (_,b,_) =  b
thirdOf3    (_,_,c) =  c

517
--------------------------------------
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
-- Their Names

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
533

534
mkCoConName :: FastString -> Unique -> TyCon -> Name
batterseapower's avatar
batterseapower committed
535
mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
536
                            key (ATyCon coCon) BuiltInSyntax
537
\end{code}
538
539


540
541
542
543
544
%************************************************************************
%*									*
            Newtypes
%*									*
%************************************************************************
545

546
\begin{code}
547
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
batterseapower's avatar
batterseapower committed
548
549
550
-- ^ If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
551
552
553
554
555
556
557
558
559
560
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

561
562
-- this is here to avoid module loops
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
batterseapower's avatar
batterseapower committed
563
564
565
566
567
568
569
570
-- ^ 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.
571
572
573
splitNewTypeRepCo_maybe ty 
  | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
574
575
576
577
578
  | Just (ty', coi) <- instNewTyCon_maybe tc tys
  = case coi of
	ACo co -> Just (ty', co)
	IdCo   -> panic "splitNewTypeRepCo_maybe"
			-- This case handled by coreView
579
splitNewTypeRepCo_maybe _
580
  = Nothing
581

batterseapower's avatar
batterseapower committed
582
-- | Determines syntactic equality of coercions
583
584
coreEqCoercion :: Coercion -> Coercion -> Bool
coreEqCoercion = coreEqType
585
586
587

coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
coreEqCoercion2 = coreEqType2
588
\end{code}
TomSchrijvers's avatar
TomSchrijvers committed
589
590


591
592
593
594
595
596
%************************************************************************
%*									*
            CoercionI and its constructors
%*									*
%************************************************************************

TomSchrijvers's avatar
TomSchrijvers committed
597
598
599
600
601
--------------------------------------
-- CoercionI smart constructors
--	lifted smart constructors of ordinary coercions

\begin{code}
batterseapower's avatar
batterseapower committed
602
603
604
605
606
607
-- | '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
608
data CoercionI = IdCo | ACo Coercion
TomSchrijvers's avatar
TomSchrijvers committed
609

610
611
612
613
instance Outputable CoercionI where
  ppr IdCo     = ptext (sLit "IdCo")
  ppr (ACo co) = ppr co

614
615
616
isIdentityCoI :: CoercionI -> Bool
isIdentityCoI IdCo = True
isIdentityCoI _    = False
TomSchrijvers's avatar
TomSchrijvers committed
617

batterseapower's avatar
batterseapower committed
618
-- | Tests whether all the given 'CoercionI's represent the identity coercion
619
620
allIdCoIs :: [CoercionI] -> Bool
allIdCoIs = all isIdentityCoI
621

batterseapower's avatar
batterseapower committed
622
623
-- | For each 'CoercionI' in the input list, return either the 'Coercion' it
-- contains or the corresponding 'Type' from the other list
624
625
626
zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
zipCoArgs cois tys = zipWith fromCoI cois tys

batterseapower's avatar
batterseapower committed
627
628
-- | Return either the 'Coercion' contained within the 'CoercionI' or the given
-- 'Type' if the 'CoercionI' is the identity 'Coercion'
629
630
fromCoI :: CoercionI -> Type -> Type
fromCoI IdCo ty     = ty	-- Identity coercion represented 
631
fromCoI (ACo co) _  = co	-- 	by the type itself
632

batterseapower's avatar
batterseapower committed
633
-- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
634
635
636
637
638
639
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
640
-- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
641
642
643
644
645
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
646
-- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
647
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
648
mkTyConAppCoI tyCon tys cois
649
650
  | allIdCoIs cois = IdCo
  | otherwise	   = ACo (TyConApp tyCon (zipCoArgs cois tys))
TomSchrijvers's avatar
TomSchrijvers committed
651

batterseapower's avatar
batterseapower committed
652
-- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
653
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
654
mkAppTyCoI _   IdCo _   IdCo = IdCo
TomSchrijvers's avatar
TomSchrijvers committed
655
656
657
mkAppTyCoI ty1 coi1 ty2 coi2 =
	ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)

658

TomSchrijvers's avatar
TomSchrijvers committed
659
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
660
mkFunTyCoI _   IdCo _   IdCo = IdCo
TomSchrijvers's avatar
TomSchrijvers committed
661
662
663
mkFunTyCoI ty1 coi1 ty2 coi2 =
	ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)

batterseapower's avatar
batterseapower committed
664
-- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
TomSchrijvers's avatar
TomSchrijvers committed
665
666
667
668
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co

batterseapower's avatar
batterseapower committed
669
670
-- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
-- panic
671
fromACo :: CoercionI -> Coercion
672
673
fromACo (ACo co)  = co
fromACo (IdCo {}) = panic "fromACo"
674

batterseapower's avatar
batterseapower committed
675
676
677
-- | 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
678
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
679
mkClassPPredCoI cls tys cois 
680
681
  | allIdCoIs cois = IdCo
  | otherwise      = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
TomSchrijvers's avatar
TomSchrijvers committed
682

batterseapower's avatar
batterseapower committed
683
-- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
TomSchrijvers's avatar
TomSchrijvers committed
684
mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
685
mkIParamPredCoI _   IdCo     = IdCo
TomSchrijvers's avatar
TomSchrijvers committed
686
687
mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co

batterseapower's avatar
batterseapower committed
688
-- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
TomSchrijvers's avatar
TomSchrijvers committed
689
690
691
mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkEqPredCoI _    IdCo     _   IdCo      = IdCo
mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
692
mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
TomSchrijvers's avatar
TomSchrijvers committed
693
\end{code}
694
695
696
697
698
699
700
701

%************************************************************************
%*                                                                      *
                 Optimising coercions									
%*                                                                      *
%************************************************************************

\begin{code}
702
703
704
705
706
optCoercion :: TvSubst -> Coercion -> NormalCo
-- ^ optCoercion applies a substitution to a coercion, 
--   *and* optimises it to reduce its size
optCoercion env co = opt_co env False co

707
708
type NormalCo = Coercion
  -- Invariants: 
709
  --  * The substitution has been fully applied
710
711
712
713
714
715
  --  * For trans coercions (co1 `trans` co2)
  --       co1 is not a trans, and neither co1 nor co2 is identity
  --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)

type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity

716
717
718
719
opt_co, opt_co' :: TvSubst
       		-> Bool	       -- True <=> return (sym co)
       		-> Coercion
       		-> NormalCo	
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
opt_co = opt_co'
-- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
--       	        co1 `seq` 
--                pprTrace "opt_co done }" (ppr co1) 
--               WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (s1,t1) 
--                                     $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
--                co1
--  where
--    co1 = opt_co' sym co
--    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
--    (s,t) = coercionKind co
--    (s1,t1) | sym = (t,s)
--            | otherwise = (s,t)
--    (s2,t2) = coercionKind co1

735
736
737
738
739
opt_co' env sym (AppTy ty1 ty2) 	  = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)
opt_co' env sym (FunTy ty1 ty2) 	  = FunTy (opt_co env sym ty1) (opt_co env sym ty2)
opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))
opt_co' env sym (PredTy (IParam n ty))    = PredTy (IParam n (opt_co env sym ty))
opt_co' _   _   co@(PredTy (EqPred {}))   = pprPanic "optCoercion" (ppr co)
740

741
742
opt_co' env sym co@(TyVarTy tv)
  | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty
743
744
745
746
747
748
749
  | not (isCoVar tv)     = co   -- Identity; does not mention a CoVar
  | ty1 `coreEqType` ty2 = ty1	-- Identity; ..ditto..
  | not sym              = co
  | otherwise            = mkSymCoercion co
  where
    (ty1,ty2) = coVarKind tv

750
751
752
753
opt_co' env sym (ForAllTy tv cor) 
  | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)
  | otherwise  = case substTyVarBndr env tv of
                   (env', tv') -> ForAllTy tv' (opt_co env' sym cor)
754
755
756
  where
    (co1,co2) = coVarKind tv

757
opt_co' env sym (TyConApp tc cos)
758
  | isCoercionTyCon tc
759
760
761
  = foldl mkAppTy 
	  (opt_co_tc_app env sym tc (take arity cos))
          (map (opt_co env sym) (drop arity cos))
762
  | otherwise
763
  = TyConApp tc (map (opt_co env sym) cos)
764
765
766
767
  where
    arity = tyConArity tc

--------
768
opt_co_tc_app :: TvSubst -> Bool -> TyCon -> [Coercion] -> NormalCo
769
-- Used for CoercionTyCons only
770
771
-- Arguments are *not* already simplified/substituted
opt_co_tc_app env sym tc cos
772
  | tc `hasKey` symCoercionTyConKey
773
  = opt_co env (not sym) co1
774
775

  | tc `hasKey` transCoercionTyConKey
776
  = if sym then opt_trans opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
777
778
779
           else opt_trans opt_co1 opt_co2

  | tc `hasKey` leftCoercionTyConKey
780
781
782
  , Just (opt_co1_left, _) <- splitAppTy_maybe opt_co1
  = opt_co1_left	-- sym (left g) = left (sym g) 
			-- The opt_co has the sym pushed into it
783
784

  | tc `hasKey` rightCoercionTyConKey
785
786
  , Just (_, opt_co1_right) <- splitAppTy_maybe opt_co1
  = opt_co1_right
787
788
789
790
791
792
793
794
795
796
797
798
799

  | tc `hasKey` csel1CoercionTyConKey
  , Just (s1,_,_) <- splitCoPredTy_maybe opt_co1
  = s1

  | tc `hasKey` csel2CoercionTyConKey
  , Just (_,s2,_) <- splitCoPredTy_maybe opt_co1
  = s2

  | tc `hasKey` cselRCoercionTyConKey
  , Just (_,_,r) <- splitCoPredTy_maybe opt_co1
  = r

800
801
802
803
804
805
806
807
808
809
  | tc `hasKey` instCoercionTyConKey	-- See if the first arg 	
					-- is already a forall
  , Just (tv, co1_body) <- splitForAllTy_maybe co1
  , let ty = substTy env co2
  = opt_co (extendTvSubst env tv ty) sym co1_body

  | tc `hasKey` instCoercionTyConKey	-- See if is *now* a forall
  , Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
  , let ty = substTy env co2
  = substTyWith [tv] [ty] opt_co1_body	-- An inefficient one-variable substitution
810

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
811
  | otherwise	  -- Do *not* push sym inside top-level axioms
812
813
814
815
816
817
818
819
    		  -- e.g. if g is a top-level axiom
    		  --   g a : F a ~ a
		  -- Then (sym (g ty)) /= g (sym ty) !!
  = if sym then mkSymCoercion the_co 
           else the_co
  where
    (co1 : cos1) = cos
    (co2 : _)    = cos1
820
821
822
823
824
825
826

	-- These opt_cos have the sym pushed into them
    opt_co1 = opt_co env sym co1
    opt_co2 = opt_co env sym co2

	-- However the_co does *not* have sym pushed into it
    the_co = TyConApp tc (map (opt_co env False) cos)
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915

-------------
opt_trans :: NormalCo -> NormalCo -> NormalCo
opt_trans co1 co2
  | isIdNormCo co1 = co2
  | otherwise      = opt_trans1 co1 co2

opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
-- First arg is not the identity
opt_trans1 co1 co2
  | isIdNormCo co2 = co1
  | otherwise      = opt_trans2 co1 co2

opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
-- Neither arg is the identity
opt_trans2 (TyConApp tc [co1a,co1b]) co2
  | tc `hasKey` transCoercionTyConKey
  = opt_trans1 co1a (opt_trans2 co1b co2)

opt_trans2 co1 co2 
  | Just co <- opt_trans_rule co1 co2
  = co

opt_trans2 co1 (TyConApp tc [co2a,co2b])
  | tc `hasKey` transCoercionTyConKey
  , Just co1_2a <- opt_trans_rule co1 co2a
  = if isIdNormCo co1_2a
    then co2b
    else opt_trans2 co1_2a co2b

opt_trans2 co1 co2
  = mkTransCoercion co1 co2

------
opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
opt_trans_rule (TyConApp tc [co1]) co2
  | tc `hasKey` symCoercionTyConKey
  , co1 `coreEqType` co2
  , (_,ty2) <- coercionKind co2
  = Just ty2

opt_trans_rule co1 (TyConApp tc [co2])
  | tc `hasKey` symCoercionTyConKey
  , co1 `coreEqType` co2
  , (ty1,_) <- coercionKind co1
  = Just ty1

opt_trans_rule (TyConApp tc1 [co1,ty1]) (TyConApp tc2 [co2,ty2])
  | tc1 `hasKey` instCoercionTyConKey
  , tc1 == tc2
  , ty1 `coreEqType` ty2
  = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) 

opt_trans_rule (TyConApp tc1 cos1) (TyConApp tc2 cos2)
  | not (isCoercionTyCon tc1) || 
    getUnique tc1 `elem` [ leftCoercionTyConKey, rightCoercionTyConKey
                         , csel1CoercionTyConKey, csel2CoercionTyConKey
 			 , cselRCoercionTyConKey ]	--Yuk!
  , tc1 == tc2 		 -- Works for left,right, and csel* family
    	   		 -- BUT NOT equality axioms 
			 -- E.g.        (g Int) `trans` (g Bool)
			 -- 	   /= g (Int . Bool)
  = Just (TyConApp tc1 (zipWith opt_trans cos1 cos2))

opt_trans_rule co1 co2
  | Just (co1a, co1b) <- splitAppTy_maybe co1
  , Just (co2a, co2b) <- splitAppTy_maybe co2
  = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))

  | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
  , Just (s2,t2,r2) <- splitCoPredTy_maybe co1
  = Just (mkCoPredTy (opt_trans s1 s2)
                     (opt_trans t1 t2)
                     (opt_trans r1 r2))

  | Just (tv1,r1) <- splitForAllTy_maybe co1
  , Just (tv2,r2) <- splitForAllTy_maybe co2
  , not (isCoVar tv1)		     -- Both have same kind
  , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
  = Just (ForAllTy tv1 (opt_trans2 r1 r2'))

opt_trans_rule _ _ = Nothing

  
-------------
isIdNormCo :: NormalCo -> Bool
-- Cheap identity test: look for coercions with no coercion variables at all
-- So it'll return False for (sym g `trans` g)
isIdNormCo ty = go ty
916
  where
917
918
919
920
921
922
923
924
    go (TyVarTy tv)  	       = not (isCoVar tv)
    go (AppTy t1 t2) 	       = go t1 && go t2
    go (FunTy t1 t2) 	       = go t1 && go t2
    go (ForAllTy tv ty)        = go (tyVarKind tv) && go ty
    go (TyConApp tc tys)       = not (isCoercionTyCon tc) && all go tys
    go (PredTy (IParam _ ty))  = go ty
    go (PredTy (ClassP _ tys)) = all go tys
    go (PredTy (EqPred t1 t2)) = go t1 && go t2
925
\end{code}