diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-04-09 15:03:05 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-04-09 17:37:02 +0100 |
commit | 702fc77e20073941be26ccdaa7e75fed6655dbc3 (patch) | |
tree | 06d4070042a7c4308717a2e3a1e904ab7107f0fc | |
parent | d9b0be3cb888a6342af7e4737dd034b68fe77543 (diff) | |
download | haskell-702fc77e20073941be26ccdaa7e75fed6655dbc3.tar.gz |
Comments only
-rw-r--r-- | compiler/types/Coercion.hs | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 4be4e92e06..ef70884ec6 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 |