Coercion.lhs 39.3 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
-- more on System FC and how coercions fit into it.
--
10
module Coercion (
batterseapower's avatar
batterseapower committed
11
        -- * Main data type
12
        Coercion(..), Var, CoVar,
batterseapower's avatar
batterseapower committed
13
        LCoercion,
14
15

        -- ** Deconstructing Kinds 
16
17
        kindFunResult, kindAppResult, synTyConResKind,
        splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
18
19
20
21

        -- ** Predicates on Kinds
        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
        isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
22
        isSuperKind, 
23
24
25
26
27
	mkArrowKind, mkArrowKinds,

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

batterseapower's avatar
batterseapower committed
28
        coVarKind, coVarKind_maybe,
29
        coercionType, coercionKind, coercionKinds, isReflCo,
batterseapower's avatar
batterseapower committed
30
        mkCoercionType,
31

32
	-- ** Constructing coercions
batterseapower's avatar
batterseapower committed
33
        mkReflCo, mkCoVarCo, mkEqVarLCo,
34
35
36
37
        mkAxInstCo, mkPiCo, mkPiCos,
        mkSymCo, mkTransCo, mkNthCo,
	mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
        mkForAllCo, mkUnsafeCo,
batterseapower's avatar
batterseapower committed
38
        mkNewTypeCo, mkFamInstCo,
TomSchrijvers's avatar
TomSchrijvers committed
39

40
        -- ** Decomposition
41
        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
        getCoVar_maybe,

        splitTyConAppCo_maybe,
        splitAppCo_maybe,
        splitForAllCo_maybe,

	-- ** Coercion variables
	mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,

        -- ** Free variables
        tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize,
	
        -- ** Substitution
        CvSubstEnv, emptyCvSubstEnv, 
 	CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar,
	isEmptyCvSubst, zapCvSubstEnv, getCvInScope,
        substCo, substCos, substCoVar, substCoVars,
        substCoWithTy, substCoWithTys, 
	cvTvSubst, tvCvSubst, zipOpenCvSubst,
        substTy, extendTvSubst,
	substTyVarBndr, substCoVarBndr,

	-- ** Lifting
65
	liftCoMatch, liftCoSubstTyVar, liftCoSubstWith, 
66
        
batterseapower's avatar
batterseapower committed
67
        -- ** Comparison
68
        coreEqCoercion, coreEqCoercion2,
69

70
71
72
73
        -- ** Forcing evaluation of coercions
        seqCo,
        
        -- * Pretty-printing
74
        pprCo, pprParendCo, pprCoAxiom,
TomSchrijvers's avatar
TomSchrijvers committed
75

76
        -- * Other
batterseapower's avatar
batterseapower committed
77
        applyCo
78
79
80
81
       ) where 

#include "HsVersions.h"

82
import Unify	( MatchEnv(..), matchList )
83
import TypeRep
84
85
86
import qualified Type
import Type hiding( substTy, substTyVarBndr, extendTvSubst )
import Kind
87
import TyCon
88
import Var
89
import VarEnv
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
90
import VarSet
91
92
import Maybes	( orElse )
import Name	( Name, NamedThing(..), nameUnique )
93
import OccName 	( parenSymOcc )
94
95
import Util
import BasicTypes
96
import Outputable
97
98
import Unique
import Pair
batterseapower's avatar
batterseapower committed
99
import PrelNames	( funTyConKey, eqPrimTyConKey )
100
101
102
import Control.Applicative
import Data.Traversable (traverse, sequenceA)
import Control.Arrow (second)
103
import FastString
104
105

import qualified Data.Data as Data hiding ( TyCon )
106
107
108
109
\end{code}

%************************************************************************
%*									*
110
            Coercions
111
112
%*									*
%************************************************************************
113

114
\begin{code}
115
116
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
117

118
119
120
121
122
123
124
125
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
data Coercion 
  -- These ones mirror the shape of types
  = Refl Type  -- See Note [Refl invariant]
          -- Invariant: applications of (Refl T) to a bunch of identity coercions
          --            always show up as Refl.
          -- For example  (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).

          -- Applications of (Refl T) to some coercions, at least one of
          -- which is NOT the identity, show up as TyConAppCo.
          -- (They may not be fully saturated however.)
          -- ConAppCo coercions (like all coercions other than Refl)
          -- are NEVER the identity.

  -- These ones simply lift the correspondingly-named 
  -- Type constructors into Coercions
  | TyConAppCo TyCon [Coercion]    -- lift TyConApp 
    	       -- The TyCon is never a synonym; 
	       -- we expand synonyms eagerly

  | AppCo Coercion Coercion        -- lift AppTy

  -- See Note [Forall coercions]
  | ForAllCo TyVar Coercion       -- forall a. g

  -- These are special
  | CoVarCo CoVar
  | AxiomInstCo CoAxiom [Coercion]  -- The coercion arguments always *precisely*
                                    -- saturate arity of CoAxiom.
                                    -- See [Coercion axioms applied to coercions]
  | UnsafeCo Type Type
  | SymCo Coercion
  | TransCo Coercion Coercion

  -- These are destructors
  | NthCo Int Coercion          -- Zero-indexed
  | InstCo Coercion Type
  deriving (Data.Data, Data.Typeable)
155
156
\end{code}

batterseapower's avatar
batterseapower committed
157
\begin{code}
158
159
160
161
162
163
-- Note [LCoercions]
-- ~~~~~~~~~~~~~~~~~
-- | LCoercions are a hack used by the typechecker. Normally,
-- Coercions have free variables of type (a ~# b): we call these
-- CoVars. However, the type checker passes around equality evidence
-- (boxed up) at type (a ~ b).
batterseapower's avatar
batterseapower committed
164
--
165
166
167
168
-- An LCoercion is simply a Coercion whose free variables have the
-- boxed type (a ~ b). After we are done with typechecking the
-- desugarer finds the free variables, unboxes them, and creates a
-- resulting real Coercion with kosher free variables.
batterseapower's avatar
batterseapower committed
169
170
171
172
173
174
--
-- We can use most of the Coercion "smart constructors" to build LCoercions. However,
-- mkCoVarCo will not work! The equivalent is mkEqVarLCo.
type LCoercion = Coercion
\end{code}

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
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
Coercions have the following invariant 
     Refl is always lifted as far as possible.  

You might think that a consequencs is:
     Every identity coercions has Refl at the root

But that's not quite true because of coercion variables.  Consider
     g         where g :: Int~Int
     Left h    where h :: Maybe Int ~ Maybe Int
etc.  So the consequence is only true of coercions that
have no coercion variables.

Note [Coercion axioms applied to coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The reason coercion axioms can be applied to coercions and not just
types is to allow for better optimization.  There are some cases where
we need to be able to "push transitivity inside" an axiom in order to
expose further opportunities for optimization.  

For example, suppose we have

  C a : t[a] ~ F a
  g   : b ~ c

and we want to optimize

  sym (C b) ; t[g] ; C c

which has the kind

  F b ~ F c

(stopping through t[b] and t[c] along the way).

We'd like to optimize this to just F g -- but how?  The key is
that we need to allow axioms to be instantiated by *coercions*,
not just by types.  Then we can (in certain cases) push
transitivity inside the axiom instantiations, and then react
opposite-polarity instantiations of the same axiom.  In this
case, e.g., we match t[g] against the LHS of (C c)'s kind, to
obtain the substitution  a |-> g  (note this operation is sort
of the dual of lifting!) and hence end up with

  C g : t[b] ~ F c

which indeed has the same kind as  t[g] ; C c.

Now we have

  sym (C b) ; C g

which can be optimized to F g.


Note [Forall coercions]
~~~~~~~~~~~~~~~~~~~~~~~
Constructing coercions between forall-types can be a bit tricky.
Currently, the situation is as follows:

  ForAllCo TyVar Coercion

represents a coercion between polymorphic types, with the rule

           v : k       g : t1 ~ t2
  ----------------------------------------------
  ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)

Note that it's only necessary to coerce between polymorphic types
where the type variables have identical kinds, because equality on
kinds is trivial.

248
249
250
251
252
253
254
255
256
Note [Predicate coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
   g :: a~b
How can we coerce between types
   ([c]~a) => [a] -> c
and
   ([c]~b) => [b] -> c
where the equality predicate *itself* differs?
257

258
259
Answer: we simply treat (~) as an ordinary type constructor, so these
types really look like
260

261
262
   ((~) [c] a) -> [a] -> c
   ((~) [c] b) -> [b] -> c
263

264
So the coercion between the two is obviously
265

266
   ((~) [c] g) -> [g] -> c
267

268
269
Another way to see this to say that we simply collapse predicates to
their representation type (see Type.coreView and Type.predTypeRep).
270

271
272
273
274
275
This collapse is done by mkPredCo; there is no PredCo constructor
in Coercion.  This is important because we need Nth to work on 
predicates too:
    Nth 1 ((~) [c] g) = g
See Simplify.simplCoercionF, which generates such selections.
276

277
278
%************************************************************************
%*									*
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
\subsection{Coercion variables}
%*									*
%************************************************************************

\begin{code}
coVarName :: CoVar -> Name
coVarName = varName

setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique

setCoVarName :: CoVar -> Name -> CoVar
setCoVarName   = setVarName

isCoVar :: Var -> Bool
isCoVar v = isCoVarType (varType v)

isCoVarType :: Type -> Bool
297
isCoVarType ty 
batterseapower's avatar
batterseapower committed
298
  | Just tc <- tyConAppTyCon_maybe ty = tc `hasKey` eqPrimTyConKey
299
  | otherwise                         = False
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
\end{code}


\begin{code}
tyCoVarsOfCo :: Coercion -> VarSet
-- Extracts type and coercion variables from a coercion
tyCoVarsOfCo (Refl ty)           = tyVarsOfType ty
tyCoVarsOfCo (TyConAppCo _ cos)  = tyCoVarsOfCos cos
tyCoVarsOfCo (AppCo co1 co2)     = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (ForAllCo tv co)    = tyCoVarsOfCo co `delVarSet` tv
tyCoVarsOfCo (CoVarCo v)         = unitVarSet v
tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos
tyCoVarsOfCo (UnsafeCo ty1 ty2)  = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyCoVarsOfCo (SymCo co)          = tyCoVarsOfCo co
tyCoVarsOfCo (TransCo co1 co2)   = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (NthCo _ co)        = tyCoVarsOfCo co
tyCoVarsOfCo (InstCo co ty)      = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty

tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos

coVarsOfCo :: Coercion -> VarSet
-- Extract *coerction* variables only.  Tiresome to repeat the code, but easy.
coVarsOfCo (Refl _)            = emptyVarSet
coVarsOfCo (TyConAppCo _ cos)  = coVarsOfCos cos
coVarsOfCo (AppCo co1 co2)     = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (ForAllCo _ co)     = coVarsOfCo co
coVarsOfCo (CoVarCo v)         = unitVarSet v
coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
coVarsOfCo (UnsafeCo _ _)      = emptyVarSet
coVarsOfCo (SymCo co)          = coVarsOfCo co
coVarsOfCo (TransCo co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (NthCo _ co)        = coVarsOfCo co
coVarsOfCo (InstCo co _)       = coVarsOfCo co

coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos

coercionSize :: Coercion -> Int
coercionSize (Refl ty)           = typeSize ty
coercionSize (TyConAppCo _ cos)  = 1 + sum (map coercionSize cos)
coercionSize (AppCo co1 co2)     = coercionSize co1 + coercionSize co2
coercionSize (ForAllCo _ co)     = 1 + coercionSize co
coercionSize (CoVarCo _)         = 1
coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos)
coercionSize (UnsafeCo ty1 ty2)  = typeSize ty1 + typeSize ty2
coercionSize (SymCo co)          = 1 + coercionSize co
coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
coercionSize (NthCo _ co)        = 1 + coercionSize co
coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
\end{code}

%************************************************************************
353
%*									*
354
355
                   Pretty-printing coercions
%*                                                                      *
356
357
%************************************************************************

358
359
360
361
362
@pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
function is defined to use this.  @pprParendCo@ is the same, except it
puts parens around the type, except for the atomic cases.
@pprParendCo@ works just by setting the initial context precedence
very high.
363
364

\begin{code}
365
366
367
368
369
370
371
372
373
374
375
376
instance Outputable Coercion where
  ppr = pprCo

pprCo, pprParendCo :: Coercion -> SDoc
pprCo       co = ppr_co TopPrec   co
pprParendCo co = ppr_co TyConPrec co

ppr_co :: Prec -> Coercion -> SDoc
ppr_co _ (Refl ty) = angles (ppr ty)

ppr_co p co@(TyConAppCo tc cos)
  | tc `hasKey` funTyConKey = ppr_fun_co p co
377
  | otherwise               = pprTcApp   p ppr_co tc cos
378
379
380
381
382

ppr_co p (AppCo co1 co2)    = maybeParen p TyConPrec $
                              pprCo co1 <+> ppr_co TyConPrec co2

ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
batterseapower's avatar
batterseapower committed
383

384
ppr_co _ (CoVarCo cv)     = parenSymOcc (getOccName cv) (ppr cv)
385

386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos


ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
                             ppr_co FunPrec co1
                             <+> ptext (sLit ";")
                             <+> ppr_co FunPrec co2
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
                          pprParendCo co <> ptext (sLit "@") <> pprType ty

ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) [pprParendType ty1, pprParendType ty2]
ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]


angles :: SDoc -> SDoc
angles p = char '<' <> p <> char '>'

ppr_fun_co :: Prec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
  where
    split (TyConAppCo f [arg,res])
      | f `hasKey` funTyConKey
      = ppr_co FunPrec arg : split res
    split co = [ppr_co TopPrec co]

ppr_forall_co :: Prec -> Coercion -> SDoc
ppr_forall_co p ty
  = maybeParen p FunPrec $
415
    sep [pprForAll tvs, ppr_co TopPrec rho]
416
417
418
419
420
421
  where
    (tvs,  rho) = split1 [] ty
    split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
    split1 tvs ty               = (reverse tvs, ty)
\end{code}

422
423
424
425
426
427
\begin{code}
pprCoAxiom :: CoAxiom -> SDoc
pprCoAxiom ax
  = sep [ ptext (sLit "axiom") <+> ppr ax <+> ppr (co_ax_tvs ax)
        , nest 2 (dcolon <+> pprEqPred (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
\end{code}
428
429
430
431
432
433

%************************************************************************
%*									*
	Functions over Kinds		
%*									*
%************************************************************************
batterseapower's avatar
batterseapower committed
434

435
436
\begin{code}
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
437
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
438
--
439
-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
440
decomposeCo :: Arity -> Coercion -> [Coercion]
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ]

-- | Attempts to obtain the type variable underlying a 'Coercion'
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe (CoVarCo cv) = Just cv  
getCoVar_maybe _            = Nothing

-- | Attempts to tease a coercion apart into a type constructor and the application
-- of a number of coercion arguments to that constructor
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
splitTyConAppCo_maybe (Refl ty)           = (fmap . second . map) Refl (splitTyConApp_maybe ty)
splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos)
splitTyConAppCo_maybe _                   = Nothing

splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
splitAppCo_maybe (TyConAppCo tc cos)
459
460
461
  | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc 
  , Just (cos', co') <- snocView cos
  = Just (mkTyConAppCo tc cos', co')    -- Never create unsaturated type family apps!
462
463
464
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl
splitAppCo_maybe (Refl ty) 
465
466
  | Just (ty1, ty2) <- splitAppTy_maybe ty 
  = Just (Refl ty1, Refl ty2)
467
468
469
470
471
splitAppCo_maybe _ = Nothing

splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
splitForAllCo_maybe _                = Nothing
472
473
474
475

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

476
477
coVarKind :: CoVar -> (Type,Type) 
-- c :: t1 ~ t2
478
479
480
481
482
coVarKind cv = case coVarKind_maybe cv of
                 Just ts -> ts
                 Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))

coVarKind_maybe :: CoVar -> Maybe (Type,Type) 
483
coVarKind_maybe cv = case splitTyConApp_maybe (varType cv) of
batterseapower's avatar
batterseapower committed
484
  Just (tc, [ty1, ty2]) | tc `hasKey` eqPrimTyConKey -> Just (ty1, ty2)
485
  _ -> Nothing
486

487
-- | Makes a coercion type from two types: the types whose equality 
488
-- is proven by the relevant 'Coercion'
batterseapower's avatar
batterseapower committed
489
490
mkCoercionType :: Type -> Type -> Type
mkCoercionType = curry mkPrimEqType
491

492
493
494
495
496
497
498
isReflCo :: Coercion -> Bool
isReflCo (Refl {}) = True
isReflCo _         = False

isReflCo_maybe :: Coercion -> Maybe Type
isReflCo_maybe (Refl ty) = Just ty
isReflCo_maybe _         = Nothing
499
\end{code}
500

501
502
503
504
505
%************************************************************************
%*									*
            Building coercions
%*									*
%************************************************************************
506

507
\begin{code}
508
509
510
511
512
513
mkCoVarCo :: CoVar -> Coercion
mkCoVarCo cv
  | ty1 `eqType` ty2 = Refl ty1
  | otherwise        = CoVarCo cv
  where
    (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
514

batterseapower's avatar
batterseapower committed
515
516
517
518
519
520
521
522
523
mkEqVarLCo :: EqVar -> LCoercion
mkEqVarLCo ipv
  | ty1 `eqType` ty2 = Refl ty1
  | otherwise        = CoVarCo ipv
  where
    (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
        Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)
        Just tys -> tys

524
525
mkReflCo :: Type -> Coercion
mkReflCo = Refl
526

527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
mkAxInstCo :: CoAxiom -> [Type] -> Coercion
mkAxInstCo ax tys
  | arity == n_tys = AxiomInstCo ax rtys
  | otherwise      = ASSERT( arity < n_tys )
                     foldl AppCo (AxiomInstCo ax (take arity rtys))
                                 (drop arity rtys)
  where
    n_tys = length tys
    arity = coAxiomArity ax
    rtys  = map Refl tys

-- | Apply a 'Coercion' to another 'Coercion'.
mkAppCo :: Coercion -> Coercion -> Coercion
mkAppCo (Refl ty1) (Refl ty2)       = Refl (mkAppTy ty1 ty2)
mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co])
mkAppCo (TyConAppCo tc cos) co      = TyConAppCo tc (cos ++ [co])
mkAppCo co1 co2                     = AppCo co1 co2
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
-- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs.
batterseapower's avatar
batterseapower committed
547
548

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
549
550
551
-- See also 'mkAppCo'
mkAppCos :: Coercion -> [Coercion] -> Coercion
mkAppCos co1 tys = foldl mkAppCo co1 tys
552
553

-- | Apply a type constructor to a list of coercions.
554
555
556
557
mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
mkTyConAppCo tc cos
	       -- Expand type synonyms
  | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
558
  = mkAppCos (liftCoSubst tv_co_prs rhs_ty) leftover_cos
559
560
561
562
563

  | Just tys <- traverse isReflCo_maybe cos 
  = Refl (mkTyConApp tc tys)	-- See Note [Refl invariant]

  | otherwise = TyConAppCo tc cos
564
565

-- | Make a function 'Coercion' between two other 'Coercion's
566
567
mkFunCo :: Coercion -> Coercion -> Coercion
mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
batterseapower's avatar
batterseapower committed
568
569

-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
570
mkForAllCo :: Var -> Coercion -> Coercion
571
-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
572
573
mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty)
mkForAllCo tv  co       = ASSERT ( isTyVar tv ) ForAllCo tv co
batterseapower's avatar
batterseapower committed
574

575
-------------------------------
batterseapower's avatar
batterseapower committed
576

577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
-- | 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@.
mkSymCo :: Coercion -> Coercion

-- Do a few simple optimizations, but don't bother pushing occurrences
-- of symmetry to the leaves; the optimizer will take care of that.
mkSymCo co@(Refl {})              = co
mkSymCo    (UnsafeCo ty1 ty2)    = UnsafeCo ty2 ty1
mkSymCo    (SymCo co)            = co
mkSymCo co                       = SymCo co

-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo (Refl _) co = co
mkTransCo co (Refl _) = co
mkTransCo co1 co2     = TransCo co1 co2

mkNthCo :: Int -> Coercion -> Coercion
mkNthCo n (Refl ty) = Refl (getNth n ty)
mkNthCo n co        = NthCo n co

599
-- | Instantiates a 'Coercion' with a 'Type' argument. 
600
mkInstCo :: Coercion -> Type -> Coercion
601
mkInstCo co ty = InstCo co ty
602
603
604
605
606
607
608
609
610

-- | Manufacture a coercion from thin 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
--   to implement the @unsafeCoerce#@ primitive.  Optimise by pushing
--   down through type constructors.
mkUnsafeCo :: Type -> Type -> Coercion
mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1
mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2)
611
  | tc1 == tc2
612
  = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
613

614
615
mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
  = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
616

617
mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
618

619
-- See note [Newtype coercions] in TyCon
batterseapower's avatar
batterseapower committed
620

621
622
623
624
625
626
627
628
629
630
631
632
-- | Create a coercion constructor (axiom) suitable for the given
--   newtype 'TyCon'. The 'Name' should be that of a new coercion
--   'CoAxiom', 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.
mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
mkNewTypeCo name tycon tvs rhs_ty
  = CoAxiom { co_ax_unique = nameUnique name
            , co_ax_name   = name
            , co_ax_tvs    = tvs
            , co_ax_lhs    = mkTyConApp tycon (mkTyVarTys tvs)
            , co_ax_rhs    = rhs_ty }
633

batterseapower's avatar
batterseapower committed
634
-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
635
-- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 
636
-- the coercion constructor built here, @F@ the family tycon and @R@ the (derived)
637
-- representation tycon.
638
mkFamInstCo :: Name	-- ^ Unique name for the coercion tycon
batterseapower's avatar
batterseapower committed
639
640
641
642
		  -> [TyVar]	-- ^ Type parameters of the coercion (@tvs@)
		  -> TyCon	-- ^ Family tycon (@F@)
		  -> [Type]	-- ^ Type instance (@ts@)
		  -> TyCon	-- ^ Representation tycon (@R@)
643
644
645
646
647
648
649
650
651
652
653
654
655
656
		  -> CoAxiom	-- ^ Coercion constructor (@Co@)
mkFamInstCo name tvs family inst_tys rep_tycon
  = CoAxiom { co_ax_unique = nameUnique name
            , co_ax_name   = name
            , co_ax_tvs    = tvs
            , co_ax_lhs    = mkTyConApp family inst_tys 
            , co_ax_rhs    = mkTyConApp rep_tycon (mkTyVarTys tvs) }

mkPiCos :: [Var] -> Coercion -> Coercion
mkPiCos vs co = foldr mkPiCo co vs

mkPiCo  :: Var -> Coercion -> Coercion
mkPiCo v co | isTyVar v = mkForAllCo v co
            | otherwise = mkFunCo (mkReflCo (varType v)) co
657
\end{code}
658

659
660
661
662
663
%************************************************************************
%*									*
            Newtypes
%*									*
%************************************************************************
664

665
\begin{code}
666
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
batterseapower's avatar
batterseapower committed
667
668
669
-- ^ If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
670
instNewTyCon_maybe tc tys
671
  | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc
672
  = ASSERT( tys `lengthIs` tyConArity tc )
673
    Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys)
674
675
676
  | otherwise
  = Nothing

677
678
-- this is here to avoid module loops
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
batterseapower's avatar
batterseapower committed
679
680
681
682
683
684
685
686
-- ^ 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.
687
688
689
splitNewTypeRepCo_maybe ty 
  | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
690
691
692
  | Just (ty', co) <- instNewTyCon_maybe tc tys
  = case co of
	Refl _ -> panic "splitNewTypeRepCo_maybe"
693
			-- This case handled by coreView
694
	_      -> Just (ty', co)
695
splitNewTypeRepCo_maybe _
696
  = Nothing
697

batterseapower's avatar
batterseapower committed
698
-- | Determines syntactic equality of coercions
699
coreEqCoercion :: Coercion -> Coercion -> Bool
700
701
coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
  where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
702
703

coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2
coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2)
  = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2

coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22)
  = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22

coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2)
  = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2

coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2)
  = rnOccL env cv1 == rnOccR env cv2

coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2)
  = con1 == con2
    && all2 (coreEqCoercion2 env) cos1 cos2

coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22)
  = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
TomSchrijvers's avatar
TomSchrijvers committed
723

724
725
726
727
728
729
730
731
732
733
734
735
736
737
coreEqCoercion2 env (SymCo co1) (SymCo co2)
  = coreEqCoercion2 env co1 co2

coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22)
  = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22

coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2)
  = d1 == d2 && coreEqCoercion2 env co1 co2

coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2)
  = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2

coreEqCoercion2 _ _ _ = False
\end{code}
TomSchrijvers's avatar
TomSchrijvers committed
738

739
740
%************************************************************************
%*									*
741
742
                   Substitution of coercions
%*                                                                      *
743
744
%************************************************************************

745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
\begin{code}
-- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
--   doing a \"lifting\" substitution)
type CvSubstEnv = VarEnv Coercion

emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv = emptyVarEnv

data CvSubst 		
  = CvSubst InScopeSet 	-- The in-scope type variables
	    TvSubstEnv	-- Substitution of types
            CvSubstEnv  -- Substitution of coercions

instance Outputable CvSubst where
  ppr (CvSubst ins tenv cenv)
    = brackets $ sep[ ptext (sLit "CvSubst"),
		      nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
		      nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
		      nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]

emptyCvSubst :: CvSubst
emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv

isEmptyCvSubst :: CvSubst -> Bool
isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv

getCvInScope :: CvSubst -> InScopeSet
getCvInScope (CvSubst in_scope _ _) = in_scope

zapCvSubstEnv :: CvSubst -> CvSubst
zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv

cvTvSubst :: CvSubst -> TvSubst
cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs

tvCvSubst :: TvSubst -> CvSubst
tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv

extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
extendTvSubst (CvSubst in_scope tenv cenv) tv ty
  = CvSubst in_scope (extendVarEnv tenv tv ty) cenv

substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
  = ASSERT( isCoVar old_var )
    (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
  where
    -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
    -- In that case, mkCoVarCo will return a ReflCoercion, and
    -- we want to substitute that (not new_var) for old_var
    new_co    = mkCoVarCo new_var
    no_change = new_var == old_var && not (isReflCo new_co)

    new_cenv | no_change = delVarEnv cenv old_var
             | otherwise = extendVarEnv cenv old_var new_co

    new_var = uniqAway in_scope subst_old_var
    subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
		  -- It's important to do the substitution for coercions,
		  -- because only they can have free type variables

substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
substTyVarBndr (CvSubst in_scope tenv cenv) old_var
  = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
      (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)

zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
zipOpenCvSubst vs cos
  | debugIsOn && (length vs /= length cos)
  = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
  | otherwise 
  = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)

818
819
substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
820

821
822
substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithTys in_scope tvs tys co
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
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
  | debugIsOn && (length tvs /= length tys)
  = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
  | otherwise 
  = ASSERT( length tvs == length tys )
    substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co

-- | Substitute within a 'Coercion'
substCo :: CvSubst -> Coercion -> Coercion
substCo subst co | isEmptyCvSubst subst = co
                 | otherwise            = subst_co subst co

-- | Substitute within several 'Coercion's
substCos :: CvSubst -> [Coercion] -> [Coercion]
substCos subst cos | isEmptyCvSubst subst = cos
                   | otherwise            = map (substCo subst) cos

substTy :: CvSubst -> Type -> Type
substTy subst = Type.substTy (cvTvSubst subst)

subst_co :: CvSubst -> Coercion -> Coercion
subst_co subst co
  = go co
  where
    go_ty :: Type -> Type
    go_ty = Coercion.substTy subst

    go :: Coercion -> Coercion
    go (Refl ty)             = Refl $! go_ty ty
    go (TyConAppCo tc cos)   = let args = map go cos
                               in  args `seqList` TyConAppCo tc args
    go (AppCo co1 co2)       = mkAppCo (go co1) $! go co2
    go (ForAllCo tv co)      = case substTyVarBndr subst tv of
                                 (subst', tv') ->
                                   ForAllCo tv' $! subst_co subst' co
    go (CoVarCo cv)          = substCoVar subst cv
    go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
    go (UnsafeCo ty1 ty2)    = (UnsafeCo $! go_ty ty1) $! go_ty ty2
    go (SymCo co)            = mkSymCo (go co)
    go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
    go (NthCo d co)          = mkNthCo d (go co)
    go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty

substCoVar :: CvSubst -> CoVar -> Coercion
substCoVar (CvSubst in_scope _ cenv) cv
  | Just co  <- lookupVarEnv cenv cv      = co
  | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
869
  | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
                ASSERT( isCoVar cv ) CoVarCo cv

substCoVars :: CvSubst -> [CoVar] -> [Coercion]
substCoVars subst cvs = map (substCoVar subst) cvs

lookupTyVar :: CvSubst -> TyVar  -> Maybe Type
lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv

lookupCoVar :: CvSubst -> Var  -> Maybe Coercion
lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
\end{code}

%************************************************************************
%*									*
                   "Lifting" substitution
	   [(TyVar,Coercion)] -> Type -> Coercion
%*                                                                      *
%************************************************************************
TomSchrijvers's avatar
TomSchrijvers committed
888
889

\begin{code}
890
891
892
893
894
895
data LiftCoSubst = LCS InScopeSet LiftCoEnv

type LiftCoEnv = VarEnv Coercion
     -- Maps *type variables* to *coercions*
     -- That's the whole point of this function!

896
liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
897
898
899
900
901
902
903
904
liftCoSubstWith tvs cos ty
  = liftCoSubst (zipEqual "liftCoSubstWith" tvs cos) ty

liftCoSubst :: [(TyVar,Coercion)] -> Type -> Coercion
liftCoSubst prs ty
 | null prs  = Refl ty
 | otherwise = ty_co_subst (LCS (mkInScopeSet (tyCoVarsOfCos (map snd prs)))
                                (mkVarEnv prs)) ty
905
906
907

-- | The \"lifting\" operation which substitutes coercions for type
--   variables in a type to produce a coercion.
batterseapower's avatar
batterseapower committed
908
--
909
--   For the inverse operation, see 'liftCoMatch' 
910
ty_co_subst :: LiftCoSubst -> Type -> Coercion
911
912
913
914
ty_co_subst subst ty
  = go ty
  where
    go (TyVarTy tv)      = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
915
916
       			     -- A type variable from a non-cloned forall
			     -- won't be in the substitution
917
918
919
920
921
922
923
    go (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2)
    go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
    go (FunTy ty1 ty2)   = mkFunCo (go ty1) (go ty2)
    go (ForAllTy v ty)   = mkForAllCo v' $! (ty_co_subst subst' ty)
                         where
                           (subst', v') = liftCoSubstTyVarBndr subst v

924
925
926
927
928
929
liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv 

liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
liftCoSubstTyVarBndr (LCS in_scope cenv) old_var
  = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)		
930
  where
931
932
    new_cenv | no_change = delVarEnv cenv old_var
	     | otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
933
934
935
936
937
938
939
940
941
942
943

    no_change = new_var == old_var
    new_var = uniqAway in_scope old_var
\end{code}

\begin{code}
-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
--   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
--   That is, it matches a type against a coercion of the same
--   "shape", and returns a lifting substitution which could have been
--   used to produce the given coercion from the given type.
944
liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
945
liftCoMatch tmpls ty co 
946
947
948
  = case ty_co_match menv emptyVarEnv ty co of
      Just cenv -> Just (LCS in_scope cenv)
      Nothing   -> Nothing
949
950
951
952
953
954
955
  where
    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
    in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
    -- Like tcMatchTy, assume all the interesting variables 
    -- in ty are in tmpls

-- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
956
957
958
ty_co_match :: MatchEnv -> LiftCoEnv -> Type -> Coercion -> Maybe LiftCoEnv
ty_co_match menv subst ty co 
  | Just ty' <- coreView ty = ty_co_match menv subst ty' co
959
960

  -- Match a type variable against a non-refl coercion
961
ty_co_match menv cenv (TyVarTy tv1) co
962
963
  | Just co1' <- lookupVarEnv cenv tv1'      -- tv1' is already bound to co1
  = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
964
    then Just cenv
965
966
967
968
969
    else Nothing       -- no match since tv1 matches two different coercions

  | tv1' `elemVarSet` me_tmpls menv           -- tv1' is a template var
  = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
    then Nothing      -- occurs check failed
970
    else return (extendVarEnv cenv tv1' co)
971
972
973
974
975
976
977
        -- BAY: I don't think we need to do any kind matching here yet
        -- (compare 'match'), but we probably will when moving to SHE.

  | otherwise    -- tv1 is not a template ty var, so the only thing it
                 -- can match is a reflexivity coercion for itself.
		 -- But that case is dealt with already
  = Nothing
978
979

  where
980
981
982
    rn_env = me_env menv
    tv1' = rnOccL rn_env tv1

983
984
ty_co_match menv subst (AppTy ty1 ty2) co
  | Just (co1, co2) <- splitAppCo_maybe co	-- c.f. Unify.match on AppTy
985
986
  = do { subst' <- ty_co_match menv subst ty1 co1 
       ; ty_co_match menv subst' ty2 co2 }
TomSchrijvers's avatar
TomSchrijvers committed
987

988
989
ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
  | tc1 == tc2 = ty_co_matches menv subst tys cos
TomSchrijvers's avatar
TomSchrijvers committed
990

991
992
ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
  | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
993

994
995
996
997
ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co) 
  = ty_co_match menv' subst ty co
  where
    menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
998

999
1000
1001
ty_co_match menv subst ty co
  | Just co' <- pushRefl co = ty_co_match menv subst ty co'
  | otherwise               = Nothing
1002

1003
ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1004
ty_co_matches menv = matchList (ty_co_match menv)
1005
1006
1007
1008
1009
1010
1011

pushRefl :: Coercion -> Maybe Coercion
pushRefl (Refl (AppTy ty1 ty2))   = Just (AppCo (Refl ty1) (Refl ty2))
pushRefl (Refl (FunTy ty1 ty2))   = Just (TyConAppCo funTyCon [Refl ty1, Refl ty2])
pushRefl (Refl (TyConApp tc tys)) = Just (TyConAppCo tc (map Refl tys))
pushRefl (Refl (ForAllTy tv ty))  = Just (ForAllCo tv (Refl ty))
pushRefl _                        = Nothing
TomSchrijvers's avatar
TomSchrijvers committed
1012
\end{code}
1013
1014

%************************************************************************
1015
%*									*
1016
            Sequencing on coercions
1017
%*									*
1018
1019
1020
%************************************************************************

\begin{code}
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
seqCo :: Coercion -> ()
seqCo (Refl ty)             = seqType ty
seqCo (TyConAppCo tc cos)   = tc `seq` seqCos cos
seqCo (AppCo co1 co2)       = seqCo co1 `seq` seqCo co2
seqCo (ForAllCo tv co)      = tv `seq` seqCo co
seqCo (CoVarCo cv)          = cv `seq` ()
seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
seqCo (UnsafeCo ty1 ty2)    = seqType ty1 `seq` seqType ty2
seqCo (SymCo co)            = seqCo co
seqCo (TransCo co1 co2)     = seqCo co1 `seq` seqCo co2
seqCo (NthCo _ co)          = seqCo co
seqCo (InstCo co ty)        = seqCo co `seq` seqType ty

seqCos :: [Coercion] -> ()
seqCos []       = ()
seqCos (co:cos) = seqCo co `seq` seqCos cos
\end{code}
1038

1039
1040
1041
1042
1043
1044
1045
1046
1047
1048

%************************************************************************
%*									*
	     The kind of a type, and of a coercion
%*									*
%************************************************************************

\begin{code}
coercionType :: Coercion -> Type
coercionType co = case coercionKind co of
batterseapower's avatar
batterseapower committed
1049
                    Pair ty1 ty2 -> mkCoercionType ty1 ty2
1050
1051
1052
1053
1054
1055

------------------
-- | If it is the case that
--
-- > c :: (t1 ~ t2)
--
1056
1057
-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
coercionKind :: Coercion -> Pair Type
1058
1059
1060
1061
coercionKind (Refl ty)            = Pair ty ty
coercionKind (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
coercionKind (AppCo co1 co2)      = mkAppTy <$> coercionKind co1 <*> coercionKind co2
coercionKind (ForAllCo tv co)     = mkForAllTy tv <$> coercionKind co
1062
1063
1064
1065
1066
1067
1068
1069
coercionKind (CoVarCo cv)         = ASSERT( isCoVar cv ) toPair $ coVarKind cv
coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
                                    in  Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax)) 
                                             (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
coercionKind (UnsafeCo ty1 ty2)   = Pair ty1 ty2
coercionKind (SymCo co)           = swap $ coercionKind co
coercionKind (TransCo co1 co2)    = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
coercionKind (NthCo d co)         = getNth d <$> coercionKind co
1070
coercionKind co@(InstCo aco ty)    | Just ks <- splitForAllTy_maybe `traverse` coercionKind aco
1071
                                  = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
1072
				  | otherwise = pprPanic "coercionKind" (ppr co)
1073
1074

-- | Apply 'coercionKind' to multiple 'Coercion's
1075
1076
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds tys = sequenceA $ map coercionKind tys
1077

1078
getNth :: Int -> Type -> Type
1079
getNth n ty | Just tys <- tyConAppArgs_maybe ty
1080
1081
            = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
1082
\end{code}
1083
1084
1085
1086
1087
1088
1089

\begin{code}
applyCo :: Type -> Coercion -> Type
-- Gives the type of (e co) where e :: (a~b) => ty
applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
applyCo (FunTy _ ty) _ = ty
applyCo _            _ = panic "applyCo"
batterseapower's avatar
batterseapower committed
1090
\end{code}