Commit bcadca67 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Tidy up coercions, and implement csel1, csel2, cselR

In preparation for implementing the PushC rule for coercion-swizzling
in the Simplifier, I had to inmplement the three new decomposition
operators for coercions, which I've called csel1, csel2, and cselR.

     co :: ((s1~t1) => r1) ~ ((s2~t2) => r2)
     ---------------------------------------
              csel1 co :: s1~s2

and similarly csel2, cselR.

On the way I fixed the coercionKind function for types of form
          (s1~t2) => r2
which currently are expressed as a forall type.  

And I refactored quite a bit to help myself understand what is
going on.
parent d7bc4e06
......@@ -37,6 +37,7 @@ import DynFlags
import Outputable
import FastString
import Util
import Control.Monad
import Data.Maybe
\end{code}
......@@ -99,11 +100,22 @@ lintCoreBindings dflags _whoDunnit _binds
= return ()
lintCoreBindings dflags whoDunnit binds
= case (initL (lint_binds binds)) of
Nothing -> showPass dflags ("Core Linted result of " ++ whoDunnit)
Just bad_news -> printDump (display bad_news) >>
ghcExit dflags 1
| isEmptyBag errs
= do { showPass dflags ("Core Linted result of " ++ whoDunnit)
; unless (isEmptyBag warns) $ printDump $
(banner "warnings" $$ displayMessageBag warns)
; return () }
| otherwise
= do { printDump (vcat [ banner "errors", displayMessageBag errs
, ptext (sLit "*** Offending Program ***")
, pprCoreBindings binds
, ptext (sLit "*** End of Offense ***") ])
; ghcExit dflags 1 }
where
(warns, errs) = initL (lint_binds binds)
-- Put all the top-level binders in scope at the start
-- This is because transformation rules can bring something
-- into use 'unexpectedly'
......@@ -114,13 +126,12 @@ lintCoreBindings dflags whoDunnit binds
lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
display bad_news
= vcat [ text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
bad_news,
ptext (sLit "*** Offending Program ***"),
pprCoreBindings binds,
ptext (sLit "*** End of Offense ***")
]
banner string = ptext (sLit "*** Core Lint") <+> text string
<+> ptext (sLit ": in result of") <+> text whoDunnit
<+> ptext (sLit "***")
displayMessageBag :: Bag Message -> SDoc
displayMessageBag msgs = vcat (punctuate blankLine (bagToList msgs))
\end{code}
%************************************************************************
......@@ -139,9 +150,12 @@ lintUnfolding :: SrcLoc
-> Maybe Message -- Nothing => OK
lintUnfolding locn vars expr
= initL (addLoc (ImportedUnfolding locn) $
addInScopeVars vars $
lintCoreExpr expr)
| isEmptyBag errs = Nothing
| otherwise = Just (displayMessageBag errs)
where
(_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
addInScopeVars vars $
lintCoreExpr expr)
\end{code}
%************************************************************************
......@@ -172,6 +186,9 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
-- Check whether binder's specialisations contain any out-of-scope variables
; mapM_ (checkBndrIdInScope binder) bndr_vars
; when (isLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
(addWarnL (ptext (sLit "INLINE binder is loop breaker:") <+> ppr binder))
-- Check whether arity and demand type are consistent (only if demand analysis
-- already happened)
; checkL (case maybeDmdTy of
......@@ -351,7 +368,7 @@ lintCoreArg fun_ty arg =
Just (arg,res) ->
do { checkTys arg arg_ty err1
; return res }
_ -> addErrL err2 }
_ -> failWithL err2 }
\end{code}
\begin{code}
......@@ -359,7 +376,7 @@ lintCoreArg fun_ty arg =
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp ty arg_ty
= case splitForAllTy_maybe ty of
Nothing -> addErrL (mkTyAppMsg ty arg_ty)
Nothing -> failWithL (mkTyAppMsg ty arg_ty)
Just (tyvar,body)
-> do { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
......@@ -372,12 +389,15 @@ checkKinds tyvar arg_ty
-- tyvar; notably this is used so that we can give
-- error :: forall a:*. String -> a
-- and then apply it to both boxed and unboxed types.
= checkL (arg_kind `isSubKind` tyvar_kind)
(mkKindErrMsg tyvar arg_ty)
| isCoVar tyvar = unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
(addErrL (mkCoAppErrMsg tyvar arg_ty))
| otherwise = unless (arg_kind `isSubKind` tyvar_kind)
(addErrL (mkKindErrMsg tyvar arg_ty))
where
tyvar_kind = tyVarKind tyvar
arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
| otherwise = typeKind arg_ty
arg_kind = typeKind arg_ty
(s1,t1) = coVarKind tyvar
(s2,t2) = coercionKind arg_ty
checkDeadIdOcc :: Id -> LintM ()
-- Occurrences of an Id should never be dead....
......@@ -561,8 +581,10 @@ newtype LintM a =
TvSubst -> -- Current type substitution; we also use this
-- to keep track of all the variables in scope,
-- both Ids and TyVars
Bag Message -> -- Error messages so far
(Maybe a, Bag Message) } -- Result and error messages (if any)
WarnsAndErrs -> -- Error and warning messages so far
(Maybe a, WarnsAndErrs) } -- Result and messages (if any)
type WarnsAndErrs = (Bag Message, Bag Message)
{- Note [Type substitution]
~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -581,7 +603,7 @@ Here we substitute 'ty' for 'a' in 'body', on the fly.
instance Monad LintM where
return x = LintM (\ _ _ errs -> (Just x, errs))
fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
fail err = failWithL (text err)
m >>= k = LintM (\ loc subst errs ->
let (res, errs') = unLintM m loc subst errs in
case res of
......@@ -601,25 +623,33 @@ data LintLocInfo
\begin{code}
initL :: LintM a -> Maybe Message {- errors -}
initL :: LintM a -> WarnsAndErrs -- Errors and warnings
initL m
= case unLintM m [] emptyTvSubst emptyBag of
(_, errs) | isEmptyBag errs -> Nothing
| otherwise -> Just (vcat (punctuate blankLine (bagToList errs)))
= case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
(_, errs) -> errs
\end{code}
\begin{code}
checkL :: Bool -> Message -> LintM ()
checkL True _ = return ()
checkL False msg = addErrL msg
checkL False msg = failWithL msg
failWithL :: Message -> LintM a
failWithL msg = LintM $ \ loc subst (warns,errs) ->
(Nothing, (warns, addMsg subst errs msg loc))
addErrL :: Message -> LintM a
addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
addErrL :: Message -> LintM ()
addErrL msg = LintM $ \ loc subst (warns,errs) ->
(Just (), (warns, addMsg subst errs msg loc))
addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
addErr subst errs_so_far msg locs
addWarnL :: Message -> LintM ()
addWarnL msg = LintM $ \ loc subst (warns,errs) ->
(Just (), (addMsg subst warns msg loc, errs))
addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
addMsg subst msgs msg locs
= ASSERT( notNull locs )
errs_so_far `snocBag` mk_msg msg
msgs `snocBag` mk_msg msg
where
(loc, cxt1) = dumpLoc (head locs)
cxts = [snd (dumpLoc loc) | loc <- locs]
......@@ -644,7 +674,7 @@ addInScopeVars vars m
| null dups
= LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
| otherwise
= addErrL (dupVars dups)
= failWithL (dupVars dups)
where
(_, dups) = removeDups compare vars
......@@ -672,7 +702,7 @@ lookupIdInScope id
= do { subst <- getTvSubst
; case lookupInScope (getTvInScope subst) id of
Just v -> return v
Nothing -> do { _ <- addErrL out_of_scope
Nothing -> do { addErrL out_of_scope
; return id } }
where
out_of_scope = ppr id <+> ptext (sLit "is out of scope")
......@@ -837,6 +867,14 @@ mkKindErrMsg tyvar arg_ty
hang (ptext (sLit "Arg type:"))
4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
mkCoAppErrMsg :: TyVar -> Type -> Message
mkCoAppErrMsg tyvar arg_ty
= vcat [ptext (sLit "Kinds don't match in coercion application:"),
hang (ptext (sLit "Coercion variable:"))
4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
hang (ptext (sLit "Arg coercion:"))
4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
mkTyAppMsg :: Type -> Type -> Message
mkTyAppMsg ty arg_ty
= vcat [text "Illegal type application:",
......
......@@ -210,7 +210,7 @@ mkCoerce co expr
-- if to_ty `coreEqType` from_ty
-- then expr
-- else
ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ ppr (coercionKindPredTy co))
ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ pprEqPred (coercionKind co))
(Cast expr co)
\end{code}
......
......@@ -123,7 +123,7 @@ ppr_expr add_par (Cast expr co)
where
pprCo co | opt_SuppressCoercions = ptext (sLit "...")
| otherwise = parens
$ sep [ppr co, dcolon <+> ppr (coercionKindPredTy co)]
$ sep [ppr co, dcolon <+> pprEqPred (coercionKind co)]
ppr_expr add_par expr@(Lam _ _)
......@@ -407,18 +407,20 @@ instance Outputable Unfolding where
, uf_expandable=exp, uf_guidance=g, uf_arity=arity})
= ptext (sLit "Unf") <> braces (pp_info $$ pp_rhs)
where
pp_info = hsep [ ptext (sLit "TopLvl=") <> ppr top
, ptext (sLit "Arity=") <> int arity
, ptext (sLit "Value=") <> ppr hnf
, ptext (sLit "ConLike=") <> ppr conlike
, ptext (sLit "Cheap=") <> ppr cheap
, ptext (sLit "Expandable=") <> ppr exp
, ppr g ]
pp_info = fsep $ punctuate comma
[ ptext (sLit "TopLvl=") <> ppr top
, ptext (sLit "Arity=") <> int arity
, ptext (sLit "Value=") <> ppr hnf
, ptext (sLit "ConLike=") <> ppr conlike
, ptext (sLit "Cheap=") <> ppr cheap
, ptext (sLit "Expandable=") <> ppr exp
, ptext (sLit "Guidance=") <> ppr g ]
pp_tmpl = ptext (sLit "Tmpl=") <+> ppr rhs
pp_rhs = case g of
UnfoldNever -> usually_empty
UnfoldIfGoodArgs {} -> usually_empty
_other -> ppr rhs
usually_empty = ifPprDebug (ppr rhs)
_other -> pp_tmpl
usually_empty = ifPprDebug pp_tmpl
-- In this case show 'rhs' only in debug mode
\end{code}
......
......@@ -1026,7 +1026,8 @@ argTypeKindTyConKey = mkPreludeTyConUnique 91
-- Coercion constructors
symCoercionTyConKey, transCoercionTyConKey, leftCoercionTyConKey,
rightCoercionTyConKey, instCoercionTyConKey, unsafeCoercionTyConKey
rightCoercionTyConKey, instCoercionTyConKey, unsafeCoercionTyConKey,
csel1CoercionTyConKey, csel2CoercionTyConKey, cselRCoercionTyConKey
:: Unique
symCoercionTyConKey = mkPreludeTyConUnique 93
transCoercionTyConKey = mkPreludeTyConUnique 94
......@@ -1034,10 +1035,13 @@ leftCoercionTyConKey = mkPreludeTyConUnique 95
rightCoercionTyConKey = mkPreludeTyConUnique 96
instCoercionTyConKey = mkPreludeTyConUnique 97
unsafeCoercionTyConKey = mkPreludeTyConUnique 98
csel1CoercionTyConKey = mkPreludeTyConUnique 99
csel2CoercionTyConKey = mkPreludeTyConUnique 100
cselRCoercionTyConKey = mkPreludeTyConUnique 101
unknownTyConKey, unknown1TyConKey, unknown2TyConKey, unknown3TyConKey,
opaqueTyConKey :: Unique
unknownTyConKey = mkPreludeTyConUnique 99
unknownTyConKey = mkPreludeTyConUnique 129
unknown1TyConKey = mkPreludeTyConUnique 130
unknown2TyConKey = mkPreludeTyConUnique 131
unknown3TyConKey = mkPreludeTyConUnique 132
......
%
T%
% (c) The University of Glasgow 2006
%
......@@ -21,8 +21,8 @@ module Coercion (
-- * Main data type
Coercion,
mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion,
mkCoKind, mkReflCoKind, coVarKind,
coercionKind, coercionKinds, isIdentityCoercion,
-- ** Equality predicates
isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
......@@ -34,12 +34,14 @@ module Coercion (
mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
unsafeCoercionTyCon, symCoercionTyCon,
transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
-- ** Optimisation
optCoercion,
......@@ -98,6 +100,24 @@ decomposeCo n co
-------------------------------------------------------
-- and some coercion kind stuff
coVarKind :: CoVar -> (Type,Type)
-- c :: t1 ~ t2
coVarKind cv = splitCoVarKind (tyVarKind cv)
-- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
-- Panics if the argument is not a valid 'CoercionKind'
splitCoVarKind :: Kind -> (Type, Type)
splitCoVarKind co | Just co' <- kindView co = splitCoVarKind co'
splitCoVarKind (PredTy (EqPred ty1 ty2)) = (ty1, ty2)
-- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
-- | (mkCoPredTy s t r) produces the type: (s~t) => r
mkCoPredTy :: Type -> Type -> Type -> Type
mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
-- | Tests whether a type is just a type equality predicate
isEqPredTy :: Type -> Bool
isEqPredTy (PredTy pred) = isEqPred pred
......@@ -113,34 +133,17 @@ getEqPredTys :: PredType -> (Type,Type)
getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
getEqPredTys other = pprPanic "getEqPredTys" (ppr other)
-- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
mkCoKind :: Type -> Type -> CoercionKind
mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
-- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
mkReflCoKind :: Type -> CoercionKind
mkReflCoKind ty = mkCoKind ty ty
-- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
-- Panics if the argument is not a valid 'CoercionKind'
splitCoercionKind :: CoercionKind -> (Type, Type)
splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
splitCoercionKind (PredTy (EqPred ty1 ty2)) = (ty1, ty2)
-- | Take a 'CoercionKind' apart into the two types it relates, if possible. See also 'splitCoercionKind'
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 _ = Nothing
-- | If it is the case that
--
-- > c :: (t1 ~ t2)
--
-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
-- See also 'coercionKindPredTy'
coercionKind :: Coercion -> (Type, Type)
coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
| otherwise = (ty, ty)
coercionKind (AppTy ty1 ty2)
= let (t1, t2) = coercionKind ty1
......@@ -161,13 +164,40 @@ coercionKind (FunTy ty1 ty2)
= let (t1, t2) = coercionKind ty1
(s1, s2) = coercionKind ty2 in
(mkFunTy t1 s1, mkFunTy t2 s2)
coercionKind (ForAllTy tv ty)
coercionKind (ForAllTy tv ty)
| isCoVar tv
-- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
-- ----------------------------------------------
-- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2
-- or
-- forall (_:c1~c2)
= let (c1,c2) = coVarKind tv
(s1,s2) = coercionKind c1
(t1,t2) = coercionKind c2
(r1,r2) = coercionKind ty
in
(mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
| otherwise
-- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2
-- ----------------------------------------------
-- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
= let (ty1, ty2) = coercionKind ty in
(ForAllTy tv ty1, ForAllTy tv ty2)
coercionKind (PredTy (EqPred c1 c2))
= let k1 = coercionKindPredTy c1
= pprTrace "coercionKind" (pprEqPred (c1,c2)) $
let k1 = coercionKindPredTy c1
k2 = coercionKindPredTy c2 in
(k1,k2)
-- These should not show up in coercions at all
-- becuase they are in the form of for-alls
where
coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
coercionKind (PredTy (ClassP cl args))
= let (lArgs, rArgs) = coercionKinds args in
(PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
......@@ -175,11 +205,6 @@ coercionKind (PredTy (IParam name ty))
= let (ty1, ty2) = coercionKind ty in
(PredTy (IParam name ty1), PredTy (IParam name ty2))
-- | Recover the 'CoercionKind' corresponding to a particular 'Coerceion'. See also 'coercionKind'
-- and 'mkCoKind'
coercionKindPredTy :: Coercion -> CoercionKind
coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
-- | Apply 'coercionKind' to multiple 'Coercion's
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys
......@@ -189,11 +214,17 @@ isIdentityCoercion :: Coercion -> Bool
isIdentityCoercion co
= case coercionKind co of
(t1,t2) -> t1 `coreEqType` t2
\end{code}
-------------------------------------
-- Coercion kind and type mk's
-- (make saturated TyConApp CoercionTyCon{...} args)
%************************************************************************
%* *
Building coercions
%* *
%************************************************************************
Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
\begin{code}
-- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
-- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
-- if possible
......@@ -323,6 +354,12 @@ mkRightCoercions n co
= acc
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
-------------------------------
mkInstCoercion :: Coercion -> Type -> Coercion
-- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
-- the resulting beta-reduction, otherwise it creates a suspended instantiation.
......@@ -432,24 +469,34 @@ mkFamInstCoercion name tvs family instTys rep_tycon
rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs],
TyConApp family instTys, -- sigma (F ts)
TyConApp rep_tycon args) -- ~ R tys
\end{code}
--------------------------------------
-- 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)
-- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family
-- of functions if possible.
symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
%************************************************************************
%* *
Coercion Type Constructors
%* *
%************************************************************************
Example. The coercion ((sym c) (sym d) (sym e))
will be represented by (TyConApp sym [c, sym d, sym e])
If sym c :: p1=q1
sym d :: p2=q2
sym e :: p3=q3
then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
\begin{code}
-- | Coercion type constructors: avoid using these directly and instead use
-- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
--
-- Each coercion TyCon is built with the special CoercionTyCon record and
-- carries its own kinding rule. Such CoercionTyCons must be fully applied
-- 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, transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
symCoercionTyCon =
mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
where
......@@ -462,43 +509,42 @@ transCoercionTyCon =
where
composeCoercionKindsOf (co1:co2:rest)
= ASSERT( null rest )
WARN( not (r1 `coreEqType` a2),
WARN( not (r1 `coreEqType` a2),
text "Strange! Type mismatch in trans coercion, probably a bug"
$$
ppr r1 <+> text "=/=" <+> ppr a2)
_err_stuff )
(a1, r2)
where
(a1, r1) = coercionKind co1
(a2, r2) = coercionKind co2
leftCoercionTyCon =
mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
where
leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
where
(ty1,ty2) = fst (splitCoercionKindOf co)
_err_stuff = vcat [ text "co1:" <+> ppr co1
, text "co1 kind left:" <+> ppr a1
, text "co1 kind right:" <+> ppr r1
, text "co2:" <+> ppr co2
, text "co2 kind left:" <+> ppr a2
, text "co2 kind right:" <+> ppr r2 ]
rightCoercionTyCon =
mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
where
rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
where
(ty1,ty2) = snd (splitCoercionKindOf co)
---------------------------------------------------
leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 (fst . decompLR)
rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR)
splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
decompLR :: [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)
decompLR (co : rest)
| (ty1, ty2) <- coercionKind 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))
splitCoercionKindOf co
= pprPanic "Coercion.splitCoercionKindOf"
(ppr co $$ ppr (coercionKindPredTy co))
= ASSERT( null rest)
((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
decompLR cos
= pprPanic "Coercion.decompLR"
(ppr cos $$ vcat (map (pprEqPred .coercionKind) cos))
---------------------------------------------------
instCoercionTyCon
= mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
where
......@@ -510,29 +556,71 @@ instCoercionTyCon
(instantiateCo t1 ty, instantiateCo t2 ty)
where (t1, t2) = coercionKind co1
---------------------------------------------------
unsafeCoercionTyCon
= mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
where
unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2)
---------------------------------------------------
-- The csel* family
-- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
-- Then csel1 co :: s1 ~ s2
-- csel2 co :: t1 ~ t2
-- cselR co :: r1 ~ r2
csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (fstOf3 . decompCsel)
csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (sndOf3 . decompCsel)
cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (thirdOf3 . decompCsel)
decompCsel :: [Coercion] -> ((Type,Type), (Type,Type), (Type,Type))
decompCsel (co : rest)
| (ty1,ty2) <- coercionKind co
, Just (cv1, r1) <- splitForAllTy_maybe ty1
, Just (cv2, r2) <- splitForAllTy_maybe ty2
, (s1,t1) <- ASSERT( isCoVar cv1) coVarKind cv1
, (s2,t2) <- ASSERT( isCoVar cv1) coVarKind cv2
= ASSERT( null rest )
((s1,s2), (t1,t2), (r1,r2))
decompCsel other = pprPanic "decompCsel" (ppr other)
fstOf3 :: (a,b,c) -> a
sndOf3 :: (a,b,c) -> b
thirdOf3 :: (a,b,c) -> c
fstOf3 (a,_,_) = a
sndOf3 (_,b,_) = b
thirdOf3 (_,_,c) = c
--------------------------------------
-- ...and their names
-- Their Names
transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName,
rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
mkCoConName :: FastString -> Unique -> TyCon -> Name
mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
key (ATyCon coCon) BuiltInSyntax
transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name
transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
\end{code}
%************************************************************************
%* *
Newtypes
%* *
%************************************************************************