Commit 6f952f58 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Use CoercionN and friends in TyCoRep

parent 7d8031ba
...@@ -127,13 +127,6 @@ import Control.Monad (foldM) ...@@ -127,13 +127,6 @@ import Control.Monad (foldM)
import Control.Arrow ( first ) import Control.Arrow ( first )
import Data.Function ( on ) import Data.Function ( on )
-----------------------------------------------------------------
-- These synonyms are very useful as documentation
type CoercionN = Coercion -- nominal coercion
type CoercionR = Coercion -- representational coercion
type CoercionP = Coercion -- phantom coercion
{- {-
%************************************************************************ %************************************************************************
%* * %* *
......
...@@ -33,6 +33,7 @@ module TyCoRep ( ...@@ -33,6 +33,7 @@ module TyCoRep (
-- Coercions -- Coercions
Coercion(..), LeftOrRight(..), Coercion(..), LeftOrRight(..),
UnivCoProvenance(..), CoercionHole(..), UnivCoProvenance(..), CoercionHole(..),
CoercionN, CoercionR, CoercionP, KindCoercion,
-- Functions over types -- Functions over types
mkTyConTy, mkTyVarTy, mkTyVarTys, mkTyConTy, mkTyVarTy, mkTyVarTys,
...@@ -213,7 +214,7 @@ data Type ...@@ -213,7 +214,7 @@ data Type
| CastTy | CastTy
Type Type
Coercion -- ^ A kind cast. The coercion is always nominal. KindCoercion -- ^ A kind cast. The coercion is always nominal.
-- INVARIANT: The cast is never refl. -- INVARIANT: The cast is never refl.
-- INVARIANT: The cast is "pushed down" as far as it -- INVARIANT: The cast is "pushed down" as far as it
-- can go. See Note [Pushing down casts] -- can go. See Note [Pushing down casts]
...@@ -592,11 +593,11 @@ data Coercion ...@@ -592,11 +593,11 @@ data Coercion
-- we expand synonyms eagerly -- we expand synonyms eagerly
-- But it can be a type function -- But it can be a type function
| AppCo Coercion Coercion -- lift AppTy | AppCo Coercion CoercionN -- lift AppTy
-- AppCo :: e -> N -> e -- AppCo :: e -> N -> e
-- See Note [Forall coercions] -- See Note [Forall coercions]
| ForAllCo TyVar Coercion Coercion | ForAllCo TyVar KindCoercion Coercion
-- ForAllCo :: _ -> N -> e -> e -- ForAllCo :: _ -> N -> e -> e
-- These are special -- These are special
...@@ -626,15 +627,15 @@ data Coercion ...@@ -626,15 +627,15 @@ data Coercion
-- Using NthCo on a ForAllCo gives an N coercion always -- Using NthCo on a ForAllCo gives an N coercion always
-- See Note [NthCo and newtypes] -- See Note [NthCo and newtypes]
| LRCo LeftOrRight Coercion -- Decomposes (t_left t_right) | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
-- :: _ -> N -> N -- :: _ -> N -> N
| InstCo Coercion Coercion | InstCo Coercion CoercionN
-- :: e -> N -> e -- :: e -> N -> e
-- See Note [InstCo roles] -- See Note [InstCo roles]
-- Coherence applies a coercion to the left-hand type of another coercion -- Coherence applies a coercion to the left-hand type of another coercion
-- See Note [Coherence] -- See Note [Coherence]
| CoherenceCo Coercion Coercion | CoherenceCo Coercion KindCoercion
-- :: e -> N -> e -- :: e -> N -> e
-- Extract a kind coercion from a (heterogeneous) type coercion -- Extract a kind coercion from a (heterogeneous) type coercion
...@@ -642,11 +643,16 @@ data Coercion ...@@ -642,11 +643,16 @@ data Coercion
| KindCo Coercion | KindCo Coercion
-- :: e -> N -- :: e -> N
| SubCo Coercion -- Turns a ~N into a ~R | SubCo CoercionN -- Turns a ~N into a ~R
-- :: N -> R -- :: N -> R
deriving (Data.Data, Data.Typeable) deriving (Data.Data, Data.Typeable)
type CoercionN = Coercion -- always nominal
type CoercionR = Coercion -- always representational
type CoercionP = Coercion -- always phantom
type KindCoercion = CoercionN -- always nominal
-- If you edit this type, you may need to update the GHC formalism -- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data LeftOrRight = CLeft | CRight data LeftOrRight = CLeft | CRight
...@@ -1002,10 +1008,12 @@ role and kind, which is done in the UnivCo constructor. ...@@ -1002,10 +1008,12 @@ role and kind, which is done in the UnivCo constructor.
data UnivCoProvenance data UnivCoProvenance
= UnsafeCoerceProv -- ^ From @unsafeCoerce#@. These are unsound. = UnsafeCoerceProv -- ^ From @unsafeCoerce#@. These are unsound.
| PhantomProv Coercion -- ^ See Note [Phantom coercions] | PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
-- roled coercions
| ProofIrrelProv Coercion -- ^ From the fact that any two coercions are | ProofIrrelProv KindCoercion -- ^ From the fact that any two coercions are
-- considered equivalent. See Note [ProofIrrelProv] -- considered equivalent. See Note [ProofIrrelProv].
-- Can be used in Nominal or Representational coercions
| PluginProv String -- ^ From a plugin, which asserts that this coercion | PluginProv String -- ^ From a plugin, which asserts that this coercion
-- is sound. The string is for the use of the plugin. -- is sound. The string is for the use of the plugin.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment