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

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
6
7
8
9
10
11
12
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

13
14
-- | Module for (a) type kinds and (b) type coercions, 
-- as used in System FC. See 'CoreSyn.Expr' for
batterseapower's avatar
batterseapower committed
15
16
-- more on System FC and how coercions fit into it.
--
17
module Coercion (
batterseapower's avatar
batterseapower committed
18
        -- * Main data type
19
        Coercion(..), Var, CoVar,
20
        LeftOrRight(..), pickLR,
21

dreixel's avatar
dreixel committed
22
        -- ** Functions over coercions
23
        coVarKind,
24
        coercionType, coercionKind, coercionKinds, isReflCo,
25
        isReflCo_maybe,
batterseapower's avatar
batterseapower committed
26
        mkCoercionType,
27

28
	-- ** Constructing coercions
29
        mkReflCo, mkCoVarCo, 
30
        mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstLHS, mkAxInstRHS,
31
        mkUnbranchedAxInstRHS,
32
        mkPiCo, mkPiCos, mkCoCast,
33
        mkSymCo, mkTransCo, mkNthCo, mkLRCo,
34
35
	mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
        mkForAllCo, mkUnsafeCo,
36
        mkNewTypeCo, 
TomSchrijvers's avatar
TomSchrijvers committed
37

38
        -- ** Decomposition
39
40
        splitNewTypeRepCo_maybe, instNewTyCon_maybe, 
        topNormaliseNewType, topNormaliseNewTypeX,
41

42
        decomposeCo, getCoVar_maybe,
43
44
45
46
47
        splitTyConAppCo_maybe,
        splitAppCo_maybe,
        splitForAllCo_maybe,

	-- ** Coercion variables
48
	mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique,
49
50
51
52
53
54
55
56
57
58

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

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

69
70
71
72
        -- ** Forcing evaluation of coercions
        seqCo,
        
        -- * Pretty-printing
Simon Peyton Jones's avatar
Simon Peyton Jones committed
73
74
75
76
77
        pprCo, pprParendCo, 
        pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr, 

        -- * Tidying
        tidyCo, tidyCos,
TomSchrijvers's avatar
TomSchrijvers committed
78

79
        -- * Other
batterseapower's avatar
batterseapower committed
80
        applyCo
81
82
83
84
       ) where 

#include "HsVersions.h"

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

import qualified Data.Data as Data hiding ( TyCon )
111
112
113
114
\end{code}

%************************************************************************
%*									*
115
            Coercions
116
117
%*									*
%************************************************************************
118

119
\begin{code}
120
121
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
122

123
124
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
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
143
	       -- But it can be a type function
144
145
146
147
148
149
150
151

  | AppCo Coercion Coercion        -- lift AppTy

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

  -- These are special
  | CoVarCo CoVar
152
  | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
153
     -- See also [CoAxiom index]
154
155
156
157
158
     -- The coercion arguments always *precisely* saturate 
     -- arity of (that branch of) the CoAxiom.  If there are
     -- any left over, we use AppCo.  See 
     -- See [Coercion axioms applied to coercions]

159
160
161
162
163
  | UnsafeCo Type Type
  | SymCo Coercion
  | TransCo Coercion Coercion

  -- These are destructors
164
165
  | NthCo  Int         Coercion     -- Zero-indexed; decomposes (T t0 ... tn)
  | LRCo   LeftOrRight Coercion     -- Decomposes (t_left t_right)
166
167
  | InstCo Coercion Type
  deriving (Data.Data, Data.Typeable)
168

169
170
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
171
172
173
data LeftOrRight = CLeft | CRight 
                 deriving( Eq, Data.Data, Data.Typeable )

174
175
176
177
178
179
180
181
182
instance Binary LeftOrRight where
   put_ bh CLeft  = putByte bh 0
   put_ bh CRight = putByte bh 1

   get bh = do { h <- getByte bh
               ; case h of
                   0 -> return CLeft
                   _ -> return CRight }

183
184
185
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft  (l,_) = l
pickLR CRight (_,r) = r
186
187
\end{code}

batterseapower's avatar
batterseapower committed
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
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.

244
245
246
247
248
249
250
251
252
253
254
255
Note [CoAxiom index]
~~~~~~~~~~~~~~~~~~~~
A CoAxiom has 1 or more branches. Each branch has contains a list
of the free type variables in that branch, the LHS type patterns,
and the RHS type for that branch. When we apply an axiom to a list
of coercions, we must choose which branch of the axiom we wish to
use, as the different branches may have different numbers of free
type variables. (The number of type patterns is always the same
among branches, but that doesn't quite concern us here.)

The Int in the AxiomInstCo constructor is the 0-indexed number
of the chosen branch.
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273

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.

274
275
276
277
278
279
280
281
282
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?
283

284
285
Answer: we simply treat (~) as an ordinary type constructor, so these
types really look like
286

287
288
   ((~) [c] a) -> [a] -> c
   ((~) [c] b) -> [b] -> c
289

290
So the coercion between the two is obviously
291

292
   ((~) [c] g) -> [g] -> c
293

294
295
Another way to see this to say that we simply collapse predicates to
their representation type (see Type.coreView and Type.predTypeRep).
296

297
298
299
300
301
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.
302

dreixel's avatar
dreixel committed
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
Note [Kind coercions]
~~~~~~~~~~~~~~~~~~~~~
Suppose T :: * -> *, and g :: A ~ B
Then the coercion
   TyConAppCo T [g]      T g : T A ~ T B

Now suppose S :: forall k. k -> *, and g :: A ~ B
Then the coercion
   TyConAppCo S [Refl *, g]   T <*> g : T * A ~ T * B

Notice that the arguments to TyConAppCo are coercions, but the first
represents a *kind* coercion. Now, we don't allow any non-trivial kind
coercions, so it's an invariant that any such kind coercions are Refl.
Lint checks this. 

However it's inconvenient to insist that these kind coercions are always
*structurally* (Refl k), because the key function exprIsConApp_maybe
pushes coercions into constructor arguments, so 
       C k ty e |> g
may turn into
       C (Nth 0 g) ....
Now (Nth 0 g) will optimise to Refl, but perhaps not instantly.

326
327
%************************************************************************
%*									*
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
\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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
346
isCoVarType ty 	    -- Tests for t1 ~# t2, the unboxed equality
347
348
349
  = case splitTyConApp_maybe ty of
      Just (tc,tys) -> tc `hasKey` eqPrimTyConKey && tys `lengthAtLeast` 2
      Nothing       -> False
350
351
352
353
354
355
356
357
358
359
360
\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
361
tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
362
363
364
365
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
366
tyCoVarsOfCo (LRCo _ co)         = tyCoVarsOfCo co
367
368
369
370
371
372
373
374
375
376
377
378
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
379
coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
380
381
382
383
coVarsOfCo (UnsafeCo _ _)      = emptyVarSet
coVarsOfCo (SymCo co)          = coVarsOfCo co
coVarsOfCo (TransCo co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (NthCo _ co)        = coVarsOfCo co
384
coVarsOfCo (LRCo _ co)         = coVarsOfCo co
385
386
387
388
389
390
391
392
393
394
395
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
396
coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
397
398
399
400
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
401
coercionSize (LRCo  _ co)        = 1 + coercionSize co
402
403
404
coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
\end{code}

Simon Peyton Jones's avatar
Simon Peyton Jones committed
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
%************************************************************************
%*									*
                            Tidying coercions
%*									*
%************************************************************************

\begin{code}
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env@(_, subst) co
  = go co
  where
    go (Refl ty)             = Refl (tidyType env ty)
    go (TyConAppCo tc cos)   = let args = map go cos
                               in args `seqList` TyConAppCo tc args
    go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
    go (ForAllCo tv co)      = ForAllCo tvp $! (tidyCo envp co)
                               where
                                 (envp, tvp) = tidyTyVarBndr env tv
    go (CoVarCo cv)          = case lookupVarEnv subst cv of
                                 Nothing  -> CoVarCo cv
                                 Just cv' -> CoVarCo cv'
    go (AxiomInstCo con ind cos) = let args = tidyCos env cos
                               in  args `seqList` AxiomInstCo con ind args
    go (UnsafeCo ty1 ty2)    = (UnsafeCo $! tidyType env ty1) $! tidyType env ty2
    go (SymCo co)            = SymCo $! go co
    go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
    go (NthCo d co)          = NthCo d $! go co
    go (LRCo lr co)          = LRCo lr $! go co
    go (InstCo co ty)        = (InstCo $! go co) $! tidyType env ty

tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
\end{code}

439
%************************************************************************
440
%*									*
441
442
                   Pretty-printing coercions
%*                                                                      *
443
444
%************************************************************************

445
446
447
448
449
@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.
450
451

\begin{code}
452
453
454
455
456
457
458
459
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
460
ppr_co _ (Refl ty) = angleBrackets (ppr ty)
461

462
ppr_co p co@(TyConAppCo tc [_,_])
463
  | tc `hasKey` funTyConKey = ppr_fun_co p co
464

465
466
467
468
469
ppr_co p (TyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos
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
ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
470
ppr_co p (AxiomInstCo con index cos)
471
472
  = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
                   (map (ppr_co TyConPrec) cos)
473

474
475
476
477
478
ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
                           case trans_co_list co [] of
                             [] -> panic "ppr_co"
                             (co:cos) -> sep ( ppr_co FunPrec co
                                             : [ char ';' <+> ppr_co FunPrec co | co <- cos])
479
480
481
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
                          pprParendCo co <> ptext (sLit "@") <> pprType ty

482
483
ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) 
                                           [pprParendType ty1, pprParendType ty2]
484
ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
485
486
ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
ppr_co p (LRCo sel co)      = pprPrefixApp p (ppr sel) [pprParendCo co]
487

488
489
490
491
trans_co_list :: Coercion -> [Coercion] -> [Coercion]
trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
trans_co_list co                cos = co : cos

492
493
494
instance Outputable LeftOrRight where
  ppr CLeft    = ptext (sLit "Left")
  ppr CRight   = ptext (sLit "Right")
495
496
497
498

ppr_fun_co :: Prec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
  where
499
    split :: Coercion -> [SDoc]
500
501
502
503
504
505
506
507
    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 $
508
    sep [pprForAll tvs, ppr_co TopPrec rho]
509
510
511
512
513
514
  where
    (tvs,  rho) = split1 [] ty
    split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
    split1 tvs ty               = (reverse tvs, ty)
\end{code}

515
\begin{code}
516
517
518
519
520
521
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
  = hang (ptext (sLit "axiom") <+> ppr ax <+> dcolon)
       2 (vcat (map (pprCoAxBranch tc) $ fromBranchList branches))

pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
522
523
pprCoAxBranch fam_tc (CoAxBranch { cab_tvs = tvs
                                 , cab_lhs = lhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
524
                                 , cab_rhs = rhs })
525
526
  = hang (ifPprDebug (pprForAll tvs))
       2 (hang (pprTypeApp fam_tc lhs) 2 (equals <+> (ppr rhs)))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
527
528
529
530
531
532
533
534
535
536
537
538
539
540

pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
  | CoAxBranch { cab_lhs = tys, cab_loc = loc } <- coAxiomNthBranch ax index
  = hang (pprTypeApp fam_tc tys)
       2 (ptext (sLit "-- Defined") <+> ppr_loc loc)
  where
        ppr_loc loc
          | isGoodSrcSpan loc
          = ptext (sLit "at") <+> ppr (srcSpanStart loc)
    
          | otherwise
          = ptext (sLit "in") <+>
              quotes (ppr (nameModule name))
541
\end{code}
542
543
544
545
546
547

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

549
550
\begin{code}
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
551
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
batterseapower's avatar
batterseapower committed
552
--
553
-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
554
decomposeCo :: Arity -> Coercion -> [Coercion]
555
556
557
decomposeCo arity co 
  = [mkNthCo n co | n <- [0..(arity-1)] ]
           -- Remember, Nth is zero-indexed
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574

-- | 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)
575
576
577
  | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc 
  , Just (cos', co') <- snocView cos
  = Just (mkTyConAppCo tc cos', co')    -- Never create unsaturated type family apps!
578
579
580
       -- Use mkTyConAppCo to preserve the invariant
       --  that identity coercions are always represented by Refl
splitAppCo_maybe (Refl ty) 
581
582
  | Just (ty1, ty2) <- splitAppTy_maybe ty 
  = Just (Refl ty1, Refl ty2)
583
584
585
586
587
splitAppCo_maybe _ = Nothing

splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
splitForAllCo_maybe _                = Nothing
588
589
590
591

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

592
coVarKind :: CoVar -> (Type,Type) 
593
594
coVarKind cv
 | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
595
 = ASSERT(tc `hasKey` eqPrimTyConKey)
596
597
598
   (ty1,ty2)
 | otherwise = panic "coVarKind, non coercion variable"

599
-- | Makes a coercion type from two types: the types whose equality 
600
-- is proven by the relevant 'Coercion'
batterseapower's avatar
batterseapower committed
601
mkCoercionType :: Type -> Type -> Type
602
mkCoercionType = mkPrimEqPred
603

604
605
606
607
608
609
610
isReflCo :: Coercion -> Bool
isReflCo (Refl {}) = True
isReflCo _         = False

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

613
614
615
616
617
%************************************************************************
%*									*
            Building coercions
%*									*
%************************************************************************
618

619
\begin{code}
620
mkCoVarCo :: CoVar -> Coercion
621
-- cv :: s ~# t
622
623
624
625
626
mkCoVarCo cv
  | ty1 `eqType` ty2 = Refl ty1
  | otherwise        = CoVarCo cv
  where
    (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv
627

628
629
mkReflCo :: Type -> Coercion
mkReflCo = Refl
630

631
mkAxInstCo :: CoAxiom br -> BranchIndex -> [Type] -> Coercion
632
633
-- mkAxInstCo can legitimately be called over-staturated; 
-- i.e. with more type arguments than the coercion requires
634
635
mkAxInstCo ax index tys
  | arity == n_tys = AxiomInstCo ax_br index rtys
636
  | otherwise      = ASSERT( arity < n_tys )
637
                     foldl AppCo (AxiomInstCo ax_br index (take arity rtys))
638
639
640
                                 (drop arity rtys)
  where
    n_tys = length tys
641
    arity = coAxiomArity ax index
642
    rtys  = map Refl tys
643
644
645
646
647
648
    ax_br = toBranchedAxiom ax

-- to be used only with unbranched axioms
mkUnbranchedAxInstCo :: CoAxiom Unbranched -> [Type] -> Coercion
mkUnbranchedAxInstCo ax tys
  = mkAxInstCo ax 0 tys
649

650
mkAxInstLHS, mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
651
652
653
-- Instantiate the axiom with specified types,
-- returning the instantiated RHS
-- A companion to mkAxInstCo: 
654
--    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
655
656
657
mkAxInstLHS ax index tys
  | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs } <- coAxiomNthBranch ax index
  , (tys1, tys2) <- splitAtList tvs tys
658
  = ASSERT( tvs `equalLength` tys1 ) 
659
660
661
662
663
664
665
    mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)

mkAxInstRHS ax index tys
  | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
  , (tys1, tys2) <- splitAtList tvs tys
  = ASSERT( tvs `equalLength` tys1 ) 
    mkAppTys (substTyWith tvs tys1 rhs) tys2
666
667
668

mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
669

670
671
672
673
674
675
676
677
678
-- | 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
679
680

-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
681
682
683
-- See also 'mkAppCo'
mkAppCos :: Coercion -> [Coercion] -> Coercion
mkAppCos co1 tys = foldl mkAppCo co1 tys
684
685

-- | Apply a type constructor to a list of coercions.
686
687
688
689
mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
mkTyConAppCo tc cos
	       -- Expand type synonyms
  | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos
690
  = mkAppCos (liftCoSubst tv_co_prs rhs_ty) leftover_cos
691
692
693
694
695

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

  | otherwise = TyConAppCo tc cos
696
697

-- | Make a function 'Coercion' between two other 'Coercion's
698
699
mkFunCo :: Coercion -> Coercion -> Coercion
mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2]
batterseapower's avatar
batterseapower committed
700
701

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

707
-------------------------------
batterseapower's avatar
batterseapower committed
708

709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
-- | 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
728
729
730
731
732
733
734
mkNthCo n (Refl ty) = ASSERT( ok_tc_app ty n ) 
                      Refl (tyConAppArgN n ty)
mkNthCo n co        = ASSERT( ok_tc_app _ty1 n && ok_tc_app _ty2 n )
                      NthCo n co
                    where
                      Pair _ty1 _ty2 = coercionKind co

735
736
737
738
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo lr (Refl ty) = Refl (pickLR lr (splitAppTy ty))
mkLRCo lr co        = LRCo lr co

739
740
741
742
ok_tc_app :: Type -> Int -> Bool
ok_tc_app ty n = case splitTyConApp_maybe ty of
                   Just (_, tys) -> tys `lengthExceeds` n
                   Nothing       -> False
743

744
-- | Instantiates a 'Coercion' with a 'Type' argument. 
745
mkInstCo :: Coercion -> Type -> Coercion
746
mkInstCo co ty = InstCo co ty
747
748
749
750
751
752
753
754
755

-- | 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)
756
  | tc1 == tc2
757
  = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2)
758

759
760
mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2)
  = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2)
761

762
mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
763

764
-- See note [Newtype coercions] in TyCon
batterseapower's avatar
batterseapower committed
765

766
767
768
769
770
-- | 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.
771
mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom Unbranched
772
mkNewTypeCo name tycon tvs rhs_ty
773
774
775
  = CoAxiom { co_ax_unique   = nameUnique name
            , co_ax_name     = name
            , co_ax_implicit = True  -- See Note [Implicit axioms] in TyCon
776
777
            , co_ax_tc       = tycon
            , co_ax_branches = FirstBranch branch }
778
779
  where branch = CoAxBranch { cab_loc = getSrcSpan name
                            , cab_tvs = tvs
780
                            , cab_lhs = mkTyVarTys tvs
781
782
                            , cab_rhs = rhs_ty
                            , cab_incomps = [] }
783
784
785
786
787
788
789

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
790
791
792
793
794
795
796
797
798
799
800
801

mkCoCast :: Coercion -> Coercion -> Coercion
-- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2)
mkCoCast c g
  = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
  where
       -- g  :: (s1 ~# s2) ~# (t1 ~#  t2)
       -- g1 :: s1 ~# t1
       -- g2 :: s2 ~# t2
    [_reflk, g1, g2] = decomposeCo 3 g
            -- Remember, (~#) :: forall k. k -> k -> *
            -- so it takes *three* arguments, not two
802
\end{code}
803

804
805
806
807
808
%************************************************************************
%*									*
            Newtypes
%*									*
%************************************************************************
809

810
\begin{code}
811
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
batterseapower's avatar
batterseapower committed
812
813
814
-- ^ If @co :: T ts ~ rep_ty@ then:
--
-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
815
-- Checks for a newtype, and for being saturated
816
instNewTyCon_maybe tc tys
817
818
819
  | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc  -- Check for newtype
  , tys `lengthIs` tyConArity tc                      -- Check saturated
  = Just (substTyWith tvs tys ty, mkUnbranchedAxInstCo co_tc tys)
820
821
822
  | otherwise
  = Nothing

823
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
batterseapower's avatar
batterseapower committed
824
825
-- ^ 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
826
-- itself recursively. If
batterseapower's avatar
batterseapower committed
827
828
829
--
-- > splitNewTypeRepCo_maybe ty = Just (ty', co)
--
830
831
-- then  @co : ty ~ ty'@.  The function returns @Nothing@ for non-@newtypes@, 
-- or unsaturated applications
832
splitNewTypeRepCo_maybe ty 
833
834
  | Just ty' <- coreView ty 
  = splitNewTypeRepCo_maybe ty'
835
splitNewTypeRepCo_maybe (TyConApp tc tys)
836
  = instNewTyCon_maybe tc tys
837
splitNewTypeRepCo_maybe _
838
  = Nothing
839

840
841
topNormaliseNewType :: Type -> Maybe (Type, Coercion)
topNormaliseNewType ty
842
  = case topNormaliseNewTypeX initRecTc ty of
843
844
845
      Just (_, co, ty) -> Just (ty, co)
      Nothing          -> Nothing

846
topNormaliseNewTypeX :: RecTcChecker -> Type -> Maybe (RecTcChecker, Coercion, Type)
847
848
849
850
851
topNormaliseNewTypeX rec_nts ty
  | Just ty' <- coreView ty         -- Expand predicates and synonyms
  = topNormaliseNewTypeX rec_nts ty'

topNormaliseNewTypeX rec_nts (TyConApp tc tys)
852
853
  | Just rec_nts'     <- checkRecTc rec_nts tc  -- See Note [Expanding newtypes] in TyCon
  , Just (rep_ty, co) <- instNewTyCon_maybe tc tys
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
  = case topNormaliseNewTypeX rec_nts' rep_ty of
       Nothing                       -> Just (rec_nts', co,                 rep_ty)
       Just (rec_nts', co', rep_ty') -> Just (rec_nts', co `mkTransCo` co', rep_ty')

topNormaliseNewTypeX _ _ = Nothing
\end{code}


%************************************************************************
%*									*
                   Equality of coercions
%*                                                                      *
%************************************************************************

\begin{code}
batterseapower's avatar
batterseapower committed
869
-- | Determines syntactic equality of coercions
870
coreEqCoercion :: Coercion -> Coercion -> Bool
871
872
coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2
  where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2))
873
874

coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
875
876
877
878
879
880
881
882
883
884
885
886
887
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

888
coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
889
  = con1 == con2
890
    && ind1 == ind2
891
892
893
894
    && 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
895

896
897
898
899
900
901
902
903
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
904
905
coreEqCoercion2 env (LRCo d1 co1) (LRCo d2 co2)
  = d1 == d2 && coreEqCoercion2 env co1 co2
906
907
908
909
910
911

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
912

913
914
%************************************************************************
%*									*
915
916
                   Substitution of coercions
%*                                                                      *
917
918
%************************************************************************

919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
\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

961
962
963
964
965
966
967
extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
-- Also extends the in-scope set
extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co
  = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
            tenv
            (extendVarEnv cenv cv co)

968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
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,
985
		  -- because they can have free type variables
986
987
988
989
990
991

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)

992
993
994
mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst
mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs)

995
996
997
998
999
1000
1001
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)

1002
1003
substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
1004

1005
1006
substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithTys in_scope tvs tys co
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
  | 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
1042
    go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
1043
1044
1045
1046
    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)
1047
    go (LRCo lr co)          = mkLRCo lr (go co)
1048
1049
1050
1051
1052
1053
    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
1054
  | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
                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
1073

1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
Note [Lifting coercions over types: liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The KPUSH rule deals with this situation
   data T a = MkK (a -> Maybe a)
   g :: T t1 ~ K t2
   x :: t1 -> Maybe t1

   case (K @t1 x) |> g of
     K (y:t2 -> Maybe t2) -> rhs

We want to push the coercion inside the constructor application.  
So we do this

   g' :: t1~t2  =  Nth 0 g

   case K @t2 (x |> g' -> Maybe g') of
     K (y:t2 -> Maybe t2) -> rhs

The crucial operation is that we 
  * take the type of K's argument: a -> Maybe a
  * and substitute g' for a
thus giving *coercion*.  This is what liftCoSubst does.

Note [Substituting kinds in liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to take care with kind polymorphism.  Suppose
  K :: forall k (a:k). (forall b:k. a -> b) -> T k a

Now given  (K @kk1 @ty1 v) |> g) where
  g :: T kk1 ty1 ~ T kk2 ty2
we want to compute
   (forall b:k a->b) [ Nth 0 g/k, Nth 1 g/a ]
Notice that we MUST substitute for 'k'; this happens in
liftCoSubstTyVarBndr.  But what should we substitute?
We need to take b's kind 'k' and return a Kind, not a Coercion!

Happily we can do this because we know that all kind coercions
((Nth 0 g) in this case) are Refl.  So we need a special purpose
   subst_kind: LiftCoSubst -> Kind -> Kind
that expects a Refl coercion (or something equivalent to Refl)
when it looks up a kind variable.

TomSchrijvers's avatar
TomSchrijvers committed
1116
\begin{code}
1117
1118
1119
1120
-- ----------------------------------------------------
-- See Note [Lifting coercions over types: liftCoSubst]
-- ----------------------------------------------------

1121
1122
1123
1124
1125
1126
data LiftCoSubst = LCS InScopeSet LiftCoEnv

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

1127
liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
1128
1129
1130
1131
1132
1133
1134
1135
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
1136
1137
1138

-- | The \"lifting\" operation which substitutes coercions for type
--   variables in a type to produce a coercion.
batterseapower's avatar
batterseapower committed
1139
--
1140
--   For the inverse operation, see 'liftCoMatch' 
1141
ty_co_subst :: LiftCoSubst -> Type -> Coercion
1142
1143
1144
1145
ty_co_subst subst ty
  = go ty
  where
    go (TyVarTy tv)      = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
1146
1147
       			     -- A type variable from a non-cloned forall
			     -- won't be in the substitution
1148
1149
    go (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2)
    go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
dreixel's avatar
dreixel committed
1150
1151
1152
                           -- IA0_NOTE: Do we need to do anything
                           -- about kind instantiations? I don't think
                           -- so.  see Note [Kind coercions]
1153
1154
1155
1156
    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
1157
    go ty@(LitTy {})     = mkReflCo ty
1158

1159
1160
1161
1162
liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv 

liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
1163
liftCoSubstTyVarBndr subst@(LCS in_scope cenv) old_var
1164
  = (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)		
1165
  where
1166
1167
    new_cenv | no_change = delVarEnv cenv old_var
	     | otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
1168

1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
    no_change = no_kind_change && (new_var == old_var)

    new_var1 = uniqAway in_scope old_var

    old_ki = tyVarKind old_var
    no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
    new_var | no_kind_change = new_var1
            | otherwise      = setTyVarKind new_var1 (subst_kind subst old_ki)

subst_kind :: LiftCoSubst -> Kind -> Kind
-- See Note [Substituting kinds in liftCoSubst]
subst_kind subst@(LCS _ cenv) kind
  = go kind
  where
    go (LitTy n)         = n `seq` LitTy n
    go (TyVarTy kv)      = subst_kv kv
    go (TyConApp tc tys) = let args = map go tys
                           in  args `seqList` TyConApp tc args

    go (FunTy arg res)   = (FunTy $! (go arg)) $! (go res)
    go (AppTy fun arg)   = mkAppTy (go fun) $! (go arg)
    go (ForAllTy tv ty)  = case liftCoSubstTyVarBndr subst tv of
                              (subst', tv') ->
                                 ForAllTy tv' $! (subst_kind subst' ty)

    subst_kv kv
      | Just co <- lookupVarEnv cenv kv
      , let co_kind = coercionKind co
      = ASSERT2( pFst co_kind `eqKind` pSnd co_kind, ppr kv $$ ppr co )
        pFst co_kind
      | otherwise
      = TyVarTy kv
1201
1202
1203
1204
1205
1206
1207
1208
\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.
1209
liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
1210
liftCoMatch tmpls ty co 
1211
1212
1213
  = case ty_co_match menv emptyVarEnv ty co of
      Just cenv -> Just (LCS in_scope cenv)
      Nothing   -> Nothing
1214
1215
1216
1217
1218
1219
1220
  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'.
1221
1222
1223
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
1224
1225

  -- Match a type variable against a non-refl coercion
1226
ty_co_match menv cenv (TyVarTy tv1) co
1227
1228
  | Just co1' <- lookupVarEnv cenv tv1'      -- tv1' is already bound to co1
  = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
1229
    then Just cenv
1230
1231
1232
1233
1234
    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
1235
    else return (extendVarEnv cenv tv1' co)
1236
1237
1238
1239
1240
1241
1242
        -- 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
1243
1244

  where
1245
1246
1247
    rn_env = me_env menv
    tv1' = rnOccL rn_env tv1

1248
1249
ty_co_match menv subst (AppTy ty1 ty2) co
  | Just (co1, co2) <- splitAppCo_maybe co	-- c.f. Unify.match on AppTy
1250
1251
  = do { subst' <- ty_co_match menv subst ty1 co1 
       ; ty_co_match menv subst' ty2 co2 }
TomSchrijvers's avatar
TomSchrijvers committed
1252

1253
1254
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
1255

1256
1257
ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
  | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
1258

1259
1260
1261
1262
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 }
1263

1264
1265
1266
ty_co_match menv subst ty co
  | Just co' <- pushRefl co = ty_co_match menv subst ty co'
  | otherwise               = Nothing
1267

1268
ty_co_matches :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion] -> Maybe LiftCoEnv
1269
ty_co_matches menv = matchList (ty_co_match menv)
1270
1271
1272
1273
1274
1275
1276

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
1277
\end{code}
1278
1279

%************************************************************************
1280
%*									*
1281
            Sequencing on coercions
1282
%*									*
1283
1284
1285
%************************************************************************

\begin{code}
1286
1287
1288
1289
1290
1291
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` ()
1292
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
1293
1294
1295
1296
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
1297
seqCo (LRCo _ co)           = seqCo co
1298
1299
1300
1301
1302
1303
seqCo (InstCo co ty)        = seqCo co `seq` seqType ty

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

1305
1306
1307
1308
1309
1310
1311
1312
1313
1314

%************************************************************************
%*									*
	     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
1315
                    Pair ty1 ty2 -> mkCoercionType ty1 ty2
1316
1317
1318
1319
1320
1321

------------------
-- | If it is the case that
--
-- > c :: (t1 ~ t2)
--
1322
-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
1323
1324

coercionKind :: Coercion -> Pair Type 
1325
coercionKind co = go co
1326
1327
1328
1329
1330
  where 
    go (Refl ty)            = Pair ty ty
    go (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)
    go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
    go (ForAllCo tv co)     = mkForAllTy tv <$> go co
1331
    go (CoVarCo cv)         = toPair $ coVarKind cv
1332
    go (AxiomInstCo ax ind cos)
1333
      | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
1334
1335
1336
1337
1338
      , Pair tys1 tys2 <- sequenceA (map go cos)
      = ASSERT( cos `equalLength` tvs )  -- Invariant of AxiomInstCo: cos should 
                                         -- exactly saturate the axiom branch
        Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
             (substTyWith tvs tys2 rhs)
1339
1340
1341
    go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
    go (SymCo co)           = swap $ go co
    go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
1342
    go (NthCo d co)         = tyConAppArgN d <$> go co
1343
    go (LRCo lr co)         = (pickLR lr . splitAppTy) <$> go co
1344
1345
1346
1347
1348
1349
1350
    go (InstCo aco ty)      = go_app aco [ty]

    go_app :: Coercion -> [Type] -> Pair Type
    -- Collect up all the arguments and apply all at once
    -- See Note [Nested InstCos]
    go_app (InstCo co ty) tys = go_app co (ty:tys)
    go_app co             tys = (`applyTys` tys) <$> go co
1351
1352

-- | Apply 'coercionKind' to multiple 'Coercion's
1353
1354
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds tys = sequenceA $ map coercionKind tys
1355
\end{code}
1356

1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
Note [Nested InstCos]
~~~~~~~~~~~~~~~~~~~~~
In Trac #5631 we found that 70% of the entire compilation time was
being spent in coercionKind!  The reason was that we had
   (g @ ty1 @ ty2 .. @ ty100)    -- The "@s" are InstCos
where 
   g :: forall a1 a2 .. a100. phi
If we deal with the InstCos one at a time, we'll do this:
   1.  Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
   2.  Substitute phi'[ ty100/a100 ], a single tyvar->type subst
But this is a *quadratic* algorithm, and the blew up Trac #5631.
So it's very important to do the substitution simultaneously.

cf Type.applyTys (which in fact we call here)


1373
1374
1375
1376
1377
1378
\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
1379
\end{code}
dreixel's avatar
dreixel committed
1380
1381
1382
1383
1384
1385

Note [Kind coercions]
~~~~~~~~~~~~~~~~~~~~~
Kind coercions are only of the form: Refl kind. They are only used to
instantiate kind polymorphic type constructors in TyConAppCo. Remember
that kind instantiation only happens with TyConApp, not AppTy.