X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=faab46304421562cc7ab117447019d7bf650a5b7;hb=c9d713bca9ce31fed25d7201464bad48f0dbc647;hp=dcd10fc910ff196e89b9eba35493a134e2e487a9;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516;p=ghc-hetmet.git diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index dcd10fc..faab463 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -44,8 +44,9 @@ module Coercion ( mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion, mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, - - mkCoVarCoercion, + + mkClassPPredCo, mkIParamPredCo, mkEqPredCo, + mkCoVarCoercion, mkCoPredCo, unsafeCoercionTyCon, symCoercionTyCon, @@ -68,7 +69,7 @@ module Coercion ( mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, mkForAllTyCoI, fromCoI, - mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI + mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI ) where @@ -80,6 +81,7 @@ import TyCon import Class import Var import VarEnv +import VarSet import Name import PrelNames import Util @@ -276,7 +278,15 @@ mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2) -- | (mkCoPredTy s t r) produces the type: (s~t) => r mkCoPredTy :: Type -> Type -> Type -> Type -mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r +mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) ) + ForAllTy co_var r + where + co_var = mkWildCoVar (mkCoKind s t) + +mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion +-- Creates a coercion between (s1~t1) => r1 and (s2~t2) => r2 +mkCoPredCo = mkCoPredTy + splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type) splitCoPredTy_maybe ty @@ -343,7 +353,7 @@ mkTyConCoercion con cos = mkTyConApp con cos -- | Make a function 'Coercion' between two other 'Coercion's mkFunCoercion :: Coercion -> Coercion -> Coercion -mkFunCoercion co1 co2 = mkFunTy co1 co2 +mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds! -- | Make a 'Coercion' which binds a variable within an inner 'Coercion' mkForAllCoercion :: Var -> Coercion -> Coercion @@ -440,6 +450,18 @@ mkFamInstCoercion name tvs family inst_tys rep_tycon desc = CoAxiom { co_ax_tvs = tvs , co_ax_lhs = mkTyConApp family inst_tys , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) } + + +mkClassPPredCo :: Class -> [Coercion] -> Coercion +mkClassPPredCo cls = (PredTy . ClassP cls) + +mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion +mkIParamPredCo ipn = (PredTy . IParam ipn) + +mkEqPredCo :: Coercion -> Coercion -> Coercion +mkEqPredCo co1 co2 = PredTy (EqPred co1 co2) + + \end{code} @@ -676,6 +698,11 @@ mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn) -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2)) + +mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI +mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3 + + \end{code} %************************************************************************ @@ -720,7 +747,8 @@ predKind (IParam {}) = liftedTypeKind -- always represented by lifted types -- -- > c :: (t1 ~ t2) -- --- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@. +-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, +-- then @coercionKind c = (t1, t2)@. coercionKind :: Coercion -> (Type, Type) coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a | otherwise = (ty, ty) @@ -822,5 +850,8 @@ coTyConAppKind (CoAxiom { co_ax_tvs = tvs = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty) where (tys1, tys2) = coercionKinds cos -coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos) +coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat + [ ppr co <+> dcolon <+> pprEqPred (coercionKind co) + | co <- cos ])) $ + coercionKind (head cos) \end{code}