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

5
Module for type coercions, as in System FC.
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27

Coercions are represented as types, and their kinds tell what types the 
coercion works on. 

The coercion kind constructor is a special TyCon that must always be saturated

  typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]

\begin{code}
module Coercion (
        Coercion,
 
        mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
        coercionKind, coercionKinds, coercionKindPredTy,

	-- Equality predicates
	isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  

	-- Coercion transformations
        mkSymCoercion, mkTransCoercion,
        mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
        mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
28
        mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
29

30
        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
31 32 33

        unsafeCoercionTyCon, symCoercionTyCon,
        transCoercionTyCon, leftCoercionTyCon, 
TomSchrijvers's avatar
TomSchrijvers committed
34 35 36 37 38 39 40 41 42 43 44
        rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn

	-- CoercionI
	CoercionI(..),
	isIdentityCoercion,
	mkSymCoI, mkTransCoI, 
	mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
	mkNoteTyCoI, mkForAllTyCoI,
	fromCoI,
	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI,

45 46 47 48 49
       ) where 

#include "HsVersions.h"

import TypeRep
50 51
import Type
import TyCon
TomSchrijvers's avatar
TomSchrijvers committed
52
import Class
53
import Var
54 55 56 57 58 59
import Name
import OccName
import PrelNames
import Util
import Unique
import BasicTypes
60 61 62 63 64 65
import Outputable


------------------------------
decomposeCo :: Arity -> Coercion -> [Coercion]
-- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
66 67
-- So this breaks a coercion with kind T A B C :=: T D E F into
-- a list of coercions of kinds A :=: D, B :=: E and E :=: F
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
decomposeCo n co
  = go n co []
  where
    go 0 co cos = cos
    go n co cos = go (n-1) (mkLeftCoercion co)
			   (mkRightCoercion co : cos)

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

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

isEqPredTy (PredTy pred) = isEqPred pred
isEqPredTy other         = False

mkEqPred :: (Type, Type) -> PredType
mkEqPred (ty1, ty2) = EqPred ty1 ty2

getEqPredTys :: PredType -> (Type,Type)
getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
getEqPredTys other	      = pprPanic "getEqPredTys" (ppr other)

mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)

mkReflCoKind :: Type -> CoercionKind
mkReflCoKind ty = mkCoKind ty ty

splitCoercionKind :: CoercionKind -> (Type, Type)
splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)

splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
splitCoercionKind_maybe other = Nothing

type Coercion     = Type
type CoercionKind = Kind	-- A CoercionKind is always of form (ty1 :=: ty2)

coercionKind :: Coercion -> (Type, Type)
-- 	c :: (t1 :=: t2)
-- Then (coercionKind c) = (t1,t2)
111 112
coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
                            | otherwise = (ty, ty)
113 114 115 116 117 118
coercionKind (AppTy ty1 ty2) 
  = let (t1, t2) = coercionKind ty1
        (s1, s2) = coercionKind ty2 in
    (mkAppTy t1 s1, mkAppTy t2 s2)
coercionKind (TyConApp tc args)
  | Just (ar, rule) <- isCoercionTyCon_maybe tc 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
119
    -- CoercionTyCons carry their kinding rule, so we use it here
120 121 122 123 124
  = ASSERT( length args >= ar )	-- Always saturated
    let (ty1,ty2)    = rule (take ar args)	-- Apply the rule to the right number of args
	(tys1, tys2) = coercionKinds (drop ar args)
    in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)

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 155 156 157 158 159 160 161 162 163 164 165 166 167 168
  | otherwise
  = let (lArgs, rArgs) = coercionKinds args in
    (TyConApp tc lArgs, TyConApp tc rArgs)
coercionKind (FunTy ty1 ty2) 
  = let (t1, t2) = coercionKind ty1
        (s1, s2) = coercionKind ty2 in
    (mkFunTy t1 s1, mkFunTy t2 s2)
coercionKind (ForAllTy tv ty) 
  = let (ty1, ty2) = coercionKind ty in
    (ForAllTy tv ty1, ForAllTy tv ty2)
coercionKind (NoteTy _ ty) = coercionKind ty
coercionKind (PredTy (EqPred c1 c2)) 
  = let k1 = coercionKindPredTy c1
        k2 = coercionKindPredTy c2 in
    (k1,k2)
coercionKind (PredTy (ClassP cl args)) 
  = let (lArgs, rArgs) = coercionKinds args in
    (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
coercionKind (PredTy (IParam name ty))
  = let (ty1, ty2) = coercionKind ty in
    (PredTy (IParam name ty1), PredTy (IParam name ty2))

coercionKindPredTy :: Coercion -> CoercionKind
coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2

coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys

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

mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) 
                        TyConApp coCon args

mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion

mkAppCoercion    co1 co2 = mkAppTy co1 co2
mkAppsCoercion   co1 tys = foldl mkAppTy co1 tys
-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
mkForAllCoercion tv  co  = ASSERT ( isTyVar tv ) mkForAllTy tv co
mkFunCoercion    co1 co2 = mkFunTy co1 co2

169

170
-------------------------------
171 172 173 174
-- This smart constructor creates a sym'ed version its argument,
-- but tries to push the sym's down to the leaves.  If we come to
-- sym tv or sym tycon then we can drop the sym because tv and tycon
-- are reflexive coercions
175
mkSymCoercion co      
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
  | Just co' <- coreView co = mkSymCoercion co'

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

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

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

mkSymCoercion (TyConApp tc [co1,co2]) 
  | tc `hasKey` transCoercionTyConKey
192
     -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2)
193
     -- Note reversal of arguments!
194
  = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1)
195 196

  | tc `hasKey` instCoercionTyConKey
197
     -- sym (co @ ty) --> (sym co) @ ty
198 199 200 201 202 203
     -- Note: sym is not applied to 'ty'
  = mkInstCoercion (mkSymCoercion co1) co2

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

204 205
mkSymCoercion (TyVarTy tv) 
  | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv]
206 207 208 209 210 211 212 213 214 215 216 217
  | otherwise  = TyVarTy tv	-- Reflexive

-------------------------------
-- ToDo: we should be cleverer about transitivity
mkTransCoercion g1 g2	-- sym g `trans` g = id
  | (t1,_) <- coercionKind g1
  , (_,t2) <- coercionKind g2
  , t1 `coreEqType` t2 
  = t1	

  | otherwise
  = mkCoercion transCoercionTyCon [g1, g2]
218

219 220

-------------------------------
221 222 223
-- Smart constructors for left and right
mkLeftCoercion co 
  | Just (co', _) <- splitAppCoercion_maybe co = co'
224
  | otherwise = mkCoercion leftCoercionTyCon [co]
225 226 227 228 229

mkRightCoercion  co      
  | Just (co1, co2) <- splitAppCoercion_maybe co = co2
  | otherwise = mkCoercion rightCoercionTyCon [co]

230 231 232 233 234
mkInstCoercion co ty
  | Just (tv,co') <- splitForAllTy_maybe co
  = substTyWith [tv] [ty] co'	-- (forall a.co) @ ty  -->  co[ty/a]
  | otherwise
  = mkCoercion instCoercionTyCon  [co, ty]
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290

mkInstsCoercion co tys = foldl mkInstCoercion co tys

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

splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- Splits a coercion application, being careful *not* to split (left c), etc
-- which are really sytactic constructs, not applications
splitAppCoercion_maybe co  | Just co' <- coreView co = splitAppCoercion_maybe co'
splitAppCoercion_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
splitAppCoercion_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
splitAppCoercion_maybe (TyConApp tc tys) 
   | not (isCoercionTyCon tc)
   = case snocView tys of
       Just (tys', ty') -> Just (TyConApp tc tys', ty')
       Nothing          -> Nothing
splitAppCoercion_maybe co = Nothing

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

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

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

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

-- Unsafe coercion is not safe, it is used when we know we are dealing with
291
-- bottom, which is one case in which it is safe.  It is also used to 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
292
-- implement the unsafeCoerce# primitive.
293 294 295 296 297
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion ty1 ty2 
  = mkCoercion unsafeCoercionTyCon [ty1, ty2]


298
-- See note [Newtype coercions] in TyCon
299 300
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
mkNewTypeCoercion name tycon tvs rhs_ty
301
  = mkCoercionTyCon name co_con_arity rule
302
  where
303 304
    co_con_arity = length tvs

305 306
    rule args = ASSERT( co_con_arity == length args )
		(TyConApp tycon args, substTyWith tvs args rhs_ty)
307

308 309 310
-- Coercion identifying a data/newtype/synonym representation type and its 
-- family instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is 
-- the coercion tycon built here, `F' the family tycon and `R' the (derived)
311 312
-- representation tycon.
--
313 314 315 316 317 318 319
mkFamInstCoercion :: Name	-- unique name for the coercion tycon
		  -> [TyVar]	-- type parameters of the coercion (`tvs')
		  -> TyCon	-- family tycon (`F')
		  -> [Type]	-- type instance (`ts')
		  -> TyCon	-- representation tycon (`R')
		  -> TyCon	-- => coercion tycon (`Co')
mkFamInstCoercion name tvs family instTys rep_tycon
320
  = mkCoercionTyCon name coArity rule
321 322
  where
    coArity = length tvs
323
    rule args = (substTyWith tvs args $		     -- with sigma = [tys/tvs],
324
		   TyConApp family instTys,	     --       sigma (F ts)
325
		 TyConApp rep_tycon args)	     --   :=: R tys
326

327 328 329 330 331 332 333 334 335 336 337 338
--------------------------------------
-- Coercion Type Constructors...

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

symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
-- Each coercion TyCon is built with the special CoercionTyCon record and
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
339
-- carries its own kinding rule.  Such CoercionTyCons must be fully applied
340 341 342
-- by any TyConApp in which they are applied, however they may also be over
-- applied (see example above) and the kinding function must deal with this.
symCoercionTyCon = 
343
  mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
344
  where
345
    flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)
346 347 348 349
	where
	  (ty1, ty2) = coercionKind co

transCoercionTyCon = 
350
  mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf
351
  where
352 353
    composeCoercionKindsOf (co1:co2:rest)
      = ASSERT( null rest )
354
        WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
355
        (a1, r2)
356 357 358 359 360
      where
        (a1, r1) = coercionKind co1
        (a2, r2) = coercionKind co2 

leftCoercionTyCon =
361
  mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
362
  where
363
    leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
364 365 366 367
      where
        (ty1,ty2) = fst (splitCoercionKindOf co)

rightCoercionTyCon =
368
  mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
369
  where
370
    rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
      where
        (ty1,ty2) = snd (splitCoercionKindOf co)

splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
-- Helper for left and right.  Finds coercion kind of its input and
-- returns the left and right projections of the coercion...
--
-- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
splitCoercionKindOf co
  | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
  , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
  , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
  = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))

instCoercionTyCon 
386
  =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
387 388 389 390 391
  where
    instantiateCo t s =
      let Just (tv, ty) = splitForAllTy_maybe t in
      substTyWith [tv] [s] ty

392 393
    instCoercionKind (co1:ty:rest) = ASSERT( null rest )
				     (instantiateCo t1 ty, instantiateCo t2 ty)
394 395 396
      where (t1, t2) = coercionKind co1

unsafeCoercionTyCon 
397
  = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
398
  where
399
   unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 
400 401 402 403 404
        
--------------------------------------
-- ...and their names

mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
405
                            key (ATyCon coCon) BuiltInSyntax
406 407 408 409 410 411 412 413 414 415

transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
leftCoercionTyConName  = mkCoConName FSLIT("left") leftCoercionTyConKey leftCoercionTyCon
rightCoercionTyConName = mkCoConName FSLIT("right") rightCoercionTyConKey rightCoercionTyCon
instCoercionTyConName  = mkCoConName FSLIT("inst") instCoercionTyConKey instCoercionTyCon
unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon



416 417 418 419 420 421 422 423 424 425 426 427 428
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
-- instNewTyCon_maybe T ts
--	= Just (rep_ty, co)	if   co : T ts ~ rep_ty
instNewTyCon_maybe tc tys
  | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc
  = ASSERT( tys `lengthIs` tyConArity tc )
    Just (substTyWith tvs tys ty, 
	  case mb_co_tc of
	   Nothing    -> IdCo
	   Just co_tc -> ACo (mkTyConApp co_tc tys))
  | otherwise
  = Nothing

429 430
-- this is here to avoid module loops
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)  
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
431
-- Sometimes we want to look through a newtype and get its associated coercion
432 433
-- It only strips *one layer* off, so the caller will usually call itself recursively
-- Only applied to types of kind *, hence the newtype is always saturated
434 435 436
--    splitNewTypeRepCo_maybe ty
--	= Just (ty', co)  if   co : ty ~ ty'
-- Returns Nothing for non-newtypes or fully-transparent newtypes
437 438 439
splitNewTypeRepCo_maybe ty 
  | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
splitNewTypeRepCo_maybe (TyConApp tc tys)
440 441 442 443 444 445 446
  | Just (ty', coi) <- instNewTyCon_maybe tc tys
  = case coi of
	ACo co -> Just (ty', co)
	IdCo   -> panic "splitNewTypeRepCo_maybe"
			-- This case handled by coreView
splitNewTypeRepCo_maybe other 
  = Nothing
447
\end{code}
TomSchrijvers's avatar
TomSchrijvers committed
448 449 450 451 452 453 454 455 456 457 458


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


\begin{code}
	-- CoercionI is either 
	--	(a) proper coercion
	--	(b) the identity coercion
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
459
data CoercionI = IdCo | ACo Coercion
TomSchrijvers's avatar
TomSchrijvers committed
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535

isIdentityCoercion :: CoercionI -> Bool
isIdentityCoercion IdCo = True
isIdentityCoercion _    = False

mkSymCoI :: CoercionI -> CoercionI
mkSymCoI IdCo = IdCo
mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] 
				-- the smart constructor
				-- is too smart with tyvars

mkTransCoI :: CoercionI -> CoercionI -> CoercionI
mkTransCoI IdCo aco = aco
mkTransCoI aco IdCo = aco
mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2

mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
mkTyConAppCoI tyCon tys cois =
	let (anyAcon,co_args) = f tys cois
	in if anyAcon
		then ACo (TyConApp tyCon co_args)
		else IdCo
	where
		f [] [] = (False,[])
		f (x:xs) (y:ys) = 
			let (b,cos) = f xs ys
			in case y of
				IdCo   -> (b,x:cos)
				ACo co -> (True,co:cos)

mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
mkAppTyCoI ty1 coi1 ty2 coi2 =
	ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)

mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo
mkFunTyCoI ty1 coi1 ty2 coi2 =
	ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)

mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
mkNoteTyCoI _ IdCo = IdCo
mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co

mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co

fromCoI IdCo ty     = ty
fromCoI (ACo co) ty = co

mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
mkClassPPredCoI cls tys cois =
	let (anyAcon,co_args) = f tys cois
	in if anyAcon
		then ACo $ PredTy $ ClassP cls co_args
		else IdCo
	where
		f [] [] = (False,[])
		f (x:xs) (y:ys) = 
			let (b,cos) = f xs ys
			in case y of
				IdCo   -> (b,x:cos)
				ACo co -> (True,co:cos)

mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
mkIParamPredCoI ipn IdCo     = IdCo
mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co

mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkEqPredCoI _    IdCo     _   IdCo      = IdCo
mkEqPredCoI ty1  IdCo     _   (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
mkEqPredCoI ty1 (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)

\end{code}