[commit: ghc] master: Comments only (702fc77)
git at git.haskell.org
git at git.haskell.org
Thu Apr 9 16:36:48 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/702fc77e20073941be26ccdaa7e75fed6655dbc3/ghc
>---------------------------------------------------------------
commit 702fc77e20073941be26ccdaa7e75fed6655dbc3
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Thu Apr 9 15:03:05 2015 +0100
Comments only
>---------------------------------------------------------------
702fc77e20073941be26ccdaa7e75fed6655dbc3
compiler/types/Coercion.hs | 40 ++++++++++++++++++++++++----------------
1 file changed, 24 insertions(+), 16 deletions(-)
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 4be4e92..ef70884 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -470,26 +470,31 @@ which the coercion proves equality. The choice of this parameter affects
the required roles of the arguments of the TyConAppCo. To help explain
it, assume the following definition:
-newtype Age = MkAge Int
-
-Nominal: All arguments must have role Nominal. Why? So that Foo Age ~N Foo Int
-does *not* hold.
-
-Representational: All arguments must have the roles corresponding to the
-result of tyConRoles on the TyCon. This is the whole point of having
-roles on the TyCon to begin with. So, we can have Foo Age ~R Foo Int,
-if Foo's parameter has role R.
+ type instance F Int = Bool -- Axiom axF : F Int ~N Bool
+ newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
+ data Foo a = MkFoo a -- Role on Foo's parameter is Represntational
-If a Representational TyConAppCo is over-saturated (which is otherwise fine),
-the spill-over arguments must all be at Nominal. This corresponds to the
-behavior for AppCo.
+TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
+ For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
+ So that Foo Age ~N Foo Int does *not* hold.
-Phantom: All arguments must have role Phantom. This one isn't strictly
-necessary for soundness, but this choice removes ambiguity.
+TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
+TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
+ For (TyConAppCo Representational), all arguments must have the roles
+ corresponding to the result of tyConRoles on the TyCon. This is the
+ whole point of having roles on the TyCon to begin with. So, we can
+ have Foo Age ~R Foo Int, if Foo's parameter has role R.
+ If a Representational TyConAppCo is over-saturated (which is otherwise fine),
+ the spill-over arguments must all be at Nominal. This corresponds to the
+ behavior for AppCo.
+TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
+ All arguments must have role Phantom. This one isn't strictly
+ necessary for soundness, but this choice removes ambiguity.
-The rules here also dictate what the parameters to mkTyConAppCo.
+The rules here dictate the roles of the parameters to mkTyConAppCo
+(should be checked by Lint).
************************************************************************
* *
@@ -1079,7 +1084,10 @@ mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole c
-- only *downgrades* a role. See Note [Role twiddling functions]
downgradeRole_maybe :: Role -- desired role
-> Role -- current role
- -> Coercion -> Maybe Coercion
+ -> Coercion
+ -> Maybe Coercion
+-- In (downgradeRole_maybe dr cr co) it's a precondition that
+-- cr = coercionRole co
downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
downgradeRole_maybe Nominal Representational _ = Nothing
downgradeRole_maybe Phantom Phantom co = Just co
More information about the ghc-commits
mailing list