Comments only: replace ":=:" by "~" (notation for equality predicates)

diff --git a/compiler/basicTypes/DataCon.lhs b/compiler/basicTypes/DataCon.lhs
index 5a67ffe..1b354c6 100644 (file)
--- a/compiler/basicTypes/DataCon.lhs
+++ b/compiler/basicTypes/DataCon.lhs
@@ -164,7 +164,7 @@ Why might the wrapper have anything to do?  Two reasons:
        \$wMkT :: a -> T [a]
        \$wMkT a x = MkT [a] a [a] x
   The third argument is a coerion
        \$wMkT :: a -> T [a]
        \$wMkT a x = MkT [a] a [a] x
   The third argument is a coerion

-       [a] :: [a]:=:[a]
+       [a] :: [a]~[a]

 
 INVARIANT: the dictionary constructor for a class
           never has a wrapper.
 
 INVARIANT: the dictionary constructor for a class
           never has a wrapper.

@@ -246,14 +246,14 @@ data DataCon
 
        --      *** As represented internally
        --  data T a where
 
        --      *** As represented internally
        --  data T a where

-       --    MkT :: forall a. forall x y. (a:=:(x,y),x~y,Ord x) => x -> y -> T a
+       --    MkT :: forall a. forall x y. (a~(x,y),x~y,Ord x) => x -> y -> T a

        -- 
        -- The next six fields express the type of the constructor, in pieces
        -- e.g.
        --
        --      dcUnivTyVars  = [a]
        --      dcExTyVars    = [x,y]
        -- 
        -- The next six fields express the type of the constructor, in pieces
        -- e.g.
        --
        --      dcUnivTyVars  = [a]
        --      dcExTyVars    = [x,y]

-       --      dcEqSpec      = [a:=:(x,y)]
+       --      dcEqSpec      = [a~(x,y)]

        --      dcEqTheta     = [x~y]   
        --      dcDictTheta   = [Ord x]
        --      dcOrigArgTys  = [a,List b]
        --      dcEqTheta     = [x~y]   
        --      dcDictTheta   = [Ord x]
        --      dcOrigArgTys  = [a,List b]

@@ -286,9 +286,9 @@ data DataCon
                                        -- _as written by the programmer_
                -- This field allows us to move conveniently between the two ways
                -- of representing a GADT constructor's type:
                                        -- _as written by the programmer_
                -- This field allows us to move conveniently between the two ways
                -- of representing a GADT constructor's type:

-               --      MkT :: forall a b. (a :=: [b]) => b -> T a
+               --      MkT :: forall a b. (a ~ [b]) => b -> T a

                --      MkT :: forall b. b -> T [b]
                --      MkT :: forall b. b -> T [b]

-               -- Each equality is of the form (a :=: ty), where 'a' is one of 
+               -- Each equality is of the form (a ~ ty), where 'a' is one of 

                -- the universally quantified type variables
                                        
                -- The next two fields give the type context of the data constructor
                -- the universally quantified type variables
                                        
                -- The next two fields give the type context of the data constructor

@@ -346,7 +346,7 @@ data DataCon
        dcRepTyCon  :: TyCon,           -- Result tycon, T
 
        dcRepType   :: Type,    -- Type of the constructor
        dcRepTyCon  :: TyCon,           -- Result tycon, T
 
        dcRepType   :: Type,    -- Type of the constructor

-                               --      forall a x y. (a:=:(x,y), x~y, Ord x) =>
+                               --      forall a x y. (a~(x,y), x~y, Ord x) =>

                                 --        x -> y -> T a
                                -- (this is *not* of the constructor wrapper Id:
                                --  see Note [Data con representation] below)
                                 --        x -> y -> T a
                                -- (this is *not* of the constructor wrapper Id:
                                --  see Note [Data con representation] below)

@@ -355,7 +355,7 @@ data DataCon
        --      case (e :: T t) of
         --        MkT x y co1 co2 (d:Ord x) (v:r) (w:F s) -> ...
        -- It's convenient to apply the rep-type of MkT to 't', to get
        --      case (e :: T t) of
         --        MkT x y co1 co2 (d:Ord x) (v:r) (w:F s) -> ...
        -- It's convenient to apply the rep-type of MkT to 't', to get

-       --      forall x y. (t:=:(x,y), x~y, Ord x) => x -> y -> T t
+       --      forall x y. (t~(x,y), x~y, Ord x) => x -> y -> T t

        -- and use that to check the pattern.  Mind you, this is really only
        -- used in CoreLint.
 
        -- and use that to check the pattern.  Mind you, this is really only
        -- used in CoreLint.
 

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index f9eae93..ae2d837 100644 (file)
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -188,7 +188,7 @@ tyConFamInst_maybe). A coercion allows you to move between
 representation and family type.  It is accessible from :R123Map via
 tyConFamilyCoercion_maybe and has kind
 
 representation and family type.  It is accessible from :R123Map via
 tyConFamilyCoercion_maybe and has kind
 

-  Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}

 
 The wrapper and worker of MapPair get the types
 
 
 The wrapper and worker of MapPair get the types
 

diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs
index ee09c3e..4f1ed2e 100644 (file)
--- a/compiler/basicTypes/Var.lhs
+++ b/compiler/basicTypes/Var.lhs
@@ -289,7 +289,7 @@ mkTcTyVar name kind details
 
 \begin{code}
 type CoVar = TyVar -- A coercion variable is simply a type 
 
 \begin{code}
 type CoVar = TyVar -- A coercion variable is simply a type 

-                       -- variable of kind @ty1 :=: ty2@. Hence its
+                       -- variable of kind @ty1 ~ ty2@. Hence its

                        -- 'varType' is always @PredTy (EqPred t1 t2)@
 
 coVarName :: CoVar -> Name
                        -- 'varType' is always @PredTy (EqPred t1 t2)@
 
 coVarName :: CoVar -> Name

diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index eb9ea41..f44967e 100644 (file)
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -740,12 +740,12 @@ dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
 --    ...
 --
 --  has representation type 
 --    ...
 --
 --  has representation type 

---   forall a. forall a1. forall b. (a :=: (a1,b)) => 
+--   forall a. forall a1. forall b. (a ~ (a1,b)) => 

 --     Int -> b -> T a
 --
 --  dataConInstPat fss us T1 (a1',b') will return
 --
 --     Int -> b -> T a
 --
 --  dataConInstPat fss us T1 (a1',b') will return
 --

---  ([a1'', b''], [c :: (a1', b'):=:(a1'', b'')], [x :: Int, y :: b''])
+--  ([a1'', b''], [c :: (a1', b')~(a1'', b'')], [x :: Int, y :: b''])

 --
 --  where the double-primed variables are created with the FastStrings and
 --  Uniques given as fss and us
 --
 --  where the double-primed variables are created with the FastStrings and
 --  Uniques given as fss and us

@@ -801,7 +801,7 @@ exprIsConApp_maybe (Cast expr co)
 
        -- The transformation applies iff we have
        --      (C e1 ... en) `cast` co
 
        -- The transformation applies iff we have
        --      (C e1 ... en) `cast` co

-       -- where co :: (T t1 .. tn) :=: (T s1 ..sn)
+       -- where co :: (T t1 .. tn) ~ (T s1 ..sn)

        -- That is, with a T at the top of both sides
        -- The left-hand one must be a T, because exprIsConApp returned True
        -- but the right-hand one might not be.  (Though it usually will.)
        -- That is, with a T at the top of both sides
        -- The left-hand one must be a T, because exprIsConApp returned True
        -- but the right-hand one might not be.  (Though it usually will.)

diff --git a/compiler/hsSyn/HsExpr.lhs b/compiler/hsSyn/HsExpr.lhs
index 17a8c3f..bcc5084 100644 (file)
--- a/compiler/hsSyn/HsExpr.lhs
+++ b/compiler/hsSyn/HsExpr.lhs
@@ -164,6 +164,8 @@ data HsExpr id
   -- Record update
   | RecordUpd   (LHsExpr id)
                 (HsRecordBinds id)
   -- Record update
   | RecordUpd   (LHsExpr id)
                 (HsRecordBinds id)

+--             (HsMatchGroup Id)  -- Filled in by the type checker to be 
+--                                -- a match that does the job

                 [DataCon]          -- Filled in by the type checker to the
                                    -- _non-empty_ list of DataCons that have
                                    -- all the upd'd fields
                 [DataCon]          -- Filled in by the type checker to the
                                    -- _non-empty_ list of DataCons that have
                                    -- all the upd'd fields

diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index 296b430..12668ab 100644 (file)
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -93,7 +93,7 @@ buildAlgTyCon tc_name tvs stupid_theta rhs is_rec want_generics gadt_syn
 --
 -- (1) create a coercion that identifies the family instance type and the
 --     representation type from Step (1); ie, it is of the form 
 --
 -- (1) create a coercion that identifies the family instance type and the
 --     representation type from Step (1); ie, it is of the form 

---        `Co tvs :: F ts :=: R tvs', where `Co' is the name of the coercion,
+--        `Co tvs :: F ts ~ R tvs', where `Co' is the name of the coercion,

 --        `F' the family tycon and `R' the (derived) representation tycon,
 --        and
 -- (2) produce a `TyConParent' value containing the parent and coercion
 --        `F' the family tycon and `R' the (derived) representation tycon,
 --        and
 -- (2) produce a `TyConParent' value containing the parent and coercion

diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs
index 59fb3e9..1688344 100644 (file)
--- a/compiler/iface/IfaceType.lhs
+++ b/compiler/iface/IfaceType.lhs
@@ -238,7 +238,7 @@ ppr_tc tc              = ppr tc
 -------------------
 instance Outputable IfacePredType where
        -- Print without parens
 -------------------
 instance Outputable IfacePredType where
        -- Print without parens

-  ppr (IfaceEqPred ty1 ty2)= hsep [ppr ty1, ptext (sLit ":=:"), ppr ty2]
+  ppr (IfaceEqPred ty1 ty2)= hsep [ppr ty1, ptext (sLit "~"), ppr ty2]

   ppr (IfaceIParam ip ty)  = hsep [ppr ip, dcolon, ppr ty]
   ppr (IfaceClassP cls ts) = parenSymOcc (getOccName cls) (ppr cls)
                             <+> sep (map pprParendIfaceType ts)
   ppr (IfaceIParam ip ty)  = hsep [ppr ip, dcolon, ppr ty]
   ppr (IfaceClassP cls ts) = parenSymOcc (getOccName cls) (ppr cls)
                             <+> sep (map pprParendIfaceType ts)

diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index f3d37e7..e7c472b 100644 (file)
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -571,7 +571,7 @@ tcInstDecl2 :: InstInfo Name -> TcM (LHsBinds Id)
 --      newtype N a = MkN (Tree [a]) deriving( Foo Int )
 --
 -- The newtype gives an FC axiom looking like
 --      newtype N a = MkN (Tree [a]) deriving( Foo Int )
 --
 -- The newtype gives an FC axiom looking like

---      axiom CoN a ::  N a :=: Tree [a]
+--      axiom CoN a ::  N a ~ Tree [a]

 --   (see Note [Newtype coercions] in TyCon for this unusual form of axiom)
 --
 -- So all need is to generate a binding looking like:
 --   (see Note [Newtype coercions] in TyCon for this unusual form of axiom)
 --
 -- So all need is to generate a binding looking like:

@@ -637,7 +637,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived })
       --        make_coercion
       -- The inst_head looks like (C s1 .. sm (T a1 .. ak))
       -- But we want the coercion (C s1 .. sm (sym (CoT a1 .. ak)))
       --        make_coercion
       -- The inst_head looks like (C s1 .. sm (T a1 .. ak))
       -- But we want the coercion (C s1 .. sm (sym (CoT a1 .. ak)))

-      --        with kind (C s1 .. sm (T a1 .. ak)  :=:  C s1 .. sm <rep_ty>)
+      --        with kind (C s1 .. sm (T a1 .. ak)  ~  C s1 .. sm <rep_ty>)

       --        where rep_ty is the (eta-reduced) type rep of T
       -- So we just replace T with CoT, and insert a 'sym'
       -- NB: we know that k will be >= arity of CoT, because the latter fully eta-reduced
       --        where rep_ty is the (eta-reduced) type rep of T
       -- So we just replace T with CoT, and insert a 'sym'
       -- NB: we know that k will be >= arity of CoT, because the latter fully eta-reduced

diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index 9511619..984b2e5 100644 (file)
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -568,7 +568,7 @@ the split arguments for the representation tycon :R123Map as {Int, c, w}
 
 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion 
 
 
 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion 
 

-  Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}

 
 moving between representation and family type into account.  To produce type
 correct Core, this coercion needs to be used to case the type of the scrutinee
 
 moving between representation and family type into account.  To produce type
 correct Core, this coercion needs to be used to case the type of the scrutinee

@@ -594,7 +594,7 @@ to express the local scope of GADT refinements.
 
 \begin{code}
 --     Running example:
 
 \begin{code}
 --     Running example:

--- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
+-- MkT :: forall a b c. (a~[b]) => b -> c -> T a

 --      with scrutinee of type (T ty)
 
 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
 --      with scrutinee of type (T ty)
 
 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index cb6021c..1e51ee0 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -861,7 +861,7 @@ Note [NO TYVARS]
 
 The excitement comes when simplifying the bindings for h.  Initially
 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
 
 The excitement comes when simplifying the bindings for h.  Initially
 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.

-From this we get t1:=:t2, but also various bindings.  We can't forget
+From this we get t1~t2, but also various bindings.  We can't forget

 the bindings (because of [LOOP]), but in fact t1 is what g is
 polymorphic in.  
 
 the bindings (because of [LOOP]), but in fact t1 is what g is
 polymorphic in.  
 

diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 5a2f773..2400838 100644 (file)
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -878,7 +878,7 @@ tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
        -- E.g.  data T a b c where
        --         MkT :: forall x y z. T (x,y) z z
        -- Then we generate
        -- E.g.  data T a b c where
        --         MkT :: forall x y z. T (x,y) z z
        -- Then we generate

-       --      ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
+       --      ([a,z,c], [x,y], [a~(x,y), c~z], T)

 
   = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
 
 
   = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
 

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 9f5daeb..72df161 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1294,8 +1294,8 @@ Note [TyCon app]
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two

-AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
+AppTys (f1 a1)~(f2 a2).  In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app).  If we unify f1~f2 first,

 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 
 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 

@@ -1870,7 +1870,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *

--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *

 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where
 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index d6b92fa..59a1a15 100644 (file)
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -74,14 +74,14 @@ import FastString
 -- | A 'Coercion' represents a 'Type' something should be coerced to.
 type Coercion     = Type
 
 -- | A 'Coercion' represents a 'Type' something should be coerced to.
 type Coercion     = Type
 

--- | A 'CoercionKind' is always of form @ty1 :=: ty2@ and indicates the
+-- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the

 -- types that a 'Coercion' will work on.
 type CoercionKind = Kind
 
 ------------------------------
 
 -- types that a 'Coercion' will work on.
 type CoercionKind = Kind
 
 ------------------------------
 

--- | This breaks a 'Coercion' with 'CoercionKind' @T A B C :=: T D E F@ into
--- a list of 'Coercion's of kinds @A :=: D@, @B :=: E@ and @E :=: F@. Hence:
+-- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
+-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:

 --
 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
 decomposeCo :: Arity -> Coercion -> [Coercion]
 --
 -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
 decomposeCo :: Arity -> Coercion -> [Coercion]

@@ -134,7 +134,7 @@ splitCoercionKind_maybe _ = Nothing
 
 -- | If it is the case that
 --
 
 -- | If it is the case that
 --

--- > c :: (t1 :=: t2)
+-- > c :: (t1 ~ t2)

 --
 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
 -- See also 'coercionKindPredTy'
 --
 -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
 -- See also 'coercionKindPredTy'

@@ -218,8 +218,8 @@ mkFunCoercion    co1 co2 = mkFunTy co1 co2
 
 mkSymCoercion :: Coercion -> Coercion
 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
 
 mkSymCoercion :: Coercion -> Coercion
 -- ^ Create a symmetric version of the given 'Coercion' that asserts equality between

--- the same types but in the other "direction", so a kind of @t1 :=: t2@ becomes the
--- kind @t2 :=: t1@.
+-- the same types but in the other "direction", so a kind of @t1 ~ t2@ becomes the
+-- kind @t2 ~ t1@.

 --
 -- This function attempts to simplify the generated 'Coercion' by removing redundant applications
 -- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that 
 --
 -- This function attempts to simplify the generated 'Coercion' by removing redundant applications
 -- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that 

@@ -405,7 +405,7 @@ mkNewTypeCoercion name tycon tvs rhs_ty
                (TyConApp tycon args, substTyWith tvs args rhs_ty)
 
 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
                (TyConApp tycon args, substTyWith tvs args rhs_ty)
 
 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type

--- and its family instance.  It has the form @Co tvs :: F ts :=: R tvs@, where @Co@ is 
+-- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 

 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 -- representation tycon.
 mkFamInstCoercion :: Name      -- ^ Unique name for the coercion tycon
 -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
 -- representation tycon.
 mkFamInstCoercion :: Name      -- ^ Unique name for the coercion tycon

@@ -420,7 +420,7 @@ mkFamInstCoercion name tvs family instTys rep_tycon
     coArity = length tvs
     rule args = (substTyWith tvs args $                     -- with sigma = [tys/tvs],
                   TyConApp family instTys,          --       sigma (F ts)
     coArity = length tvs
     rule args = (substTyWith tvs args $                     -- with sigma = [tys/tvs],
                   TyConApp family instTys,          --       sigma (F ts)

-                TyConApp rep_tycon args)            --   :=: R tys
+                TyConApp rep_tycon args)            --   ~ R tys

 
 --------------------------------------
 -- Coercion Type Constructors...
 
 --------------------------------------
 -- Coercion Type Constructors...

@@ -478,7 +478,7 @@ splitCoercionKindOf :: 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...
 --
 -- 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))
+-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))

 splitCoercionKindOf co
   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
 splitCoercionKindOf co
   | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1

diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs
index 7f9f050..170304c 100644 (file)
--- a/compiler/types/FunDeps.lhs
+++ b/compiler/types/FunDeps.lhs
@@ -203,7 +203,7 @@ type Equation = (TyVarSet, [(Type, Type)])
 pprEquation :: Equation -> SDoc
 pprEquation (qtvs, pairs) 
   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
 pprEquation :: Equation -> SDoc
 pprEquation (qtvs, pairs) 
   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),

-         nest 2 (vcat [ ppr t1 <+> ptext (sLit ":=:") <+> ppr t2 | (t1,t2) <- pairs])]
+         nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])]

 \end{code}
 
 Given a bunch of predicates that must hold, such as
 \end{code}
 
 Given a bunch of predicates that must hold, such as

@@ -320,7 +320,7 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
 --                 tys2 = [Maybe t1, t2]
 --
 -- We can instantiate x to t1, and then we want to force
 --                 tys2 = [Maybe t1, t2]
 --
 -- We can instantiate x to t1, and then we want to force

---     (Tree x) [t1/x]  :=:   t2
+--     (Tree x) [t1/x]  ~   t2

 --
 -- This function is also used when matching two Insts (rather than an Inst
 -- against an instance decl. In that case, qtvs is empty, and we are doing
 --
 -- This function is also used when matching two Insts (rather than an Inst
 -- against an instance decl. In that case, qtvs is empty, and we are doing

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 09caf8e..256b141 100644 (file)
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -112,7 +112,7 @@ import Constants
 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
 --
 -- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where
 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
 --
 -- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where

---    that type has kind @t1 :=: t2@. See "Coercion" for more on this
+--    that type has kind @t1 ~ t2@. See "Coercion" for more on this

 --
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.
 --
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.

@@ -211,7 +211,7 @@ data TyCon
        tyConExtName :: Maybe FastString        -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing
     }
 
        tyConExtName :: Maybe FastString        -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing
     }
 

-  -- | Type coercions, such as @(:=:)@, @sym@, @trans@, @left@ and @right@.
+  -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@.

   -- INVARIANT: coercions are always fully applied
   | CoercionTyCon {    
        tyConUnique :: Unique,
   -- INVARIANT: coercions are always fully applied
   | CoercionTyCon {    
        tyConUnique :: Unique,

@@ -393,7 +393,7 @@ newtype, to the newtype itself. For example,
 
    newtype T a = MkT (a -> a)
 
 
    newtype T a = MkT (a -> a)
 

-the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t ->
+the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t ->

 t.  This TyCon is a CoercionTyCon, so it does not have a kind on its
 own; it basically has its own typing rule for the fully-applied
 version.  If the newtype T has k type variables then CoT has arity at
 t.  This TyCon is a CoercionTyCon, so it does not have a kind on its
 own; it basically has its own typing rule for the fully-applied
 version.  If the newtype T has k type variables then CoT has arity at

@@ -403,11 +403,11 @@ ending with the same type variables as the left hand side, we
 
    newtype S a = MkT [a]
 
 
    newtype S a = MkT [a]
 

-then we would generate the arity 0 coercion CoS : S :=: [].  The
+then we would generate the arity 0 coercion CoS : S ~ [].  The

 primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write
 primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write

-       axiom CoT : (forall t. T t) :=: (forall t. [t])
+       axiom CoT : (forall t. T t) ~ (forall t. [t])

 and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
 and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])

@@ -418,7 +418,7 @@ be saturated, but which encodes as
        TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like
        TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like

-       axiom CoT t :  T t :=: [t]
+       axiom CoT t :  T t ~ [t]

 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 3e35ac6..07c927c 100644 (file)
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -384,7 +384,7 @@ dataConCannotMatch tys con
 data Refinement = Reft InScopeSet InternalReft 
 
 type InternalReft = TyVarEnv (Coercion, Type)
 data Refinement = Reft InScopeSet InternalReft 
 
 type InternalReft = TyVarEnv (Coercion, Type)

--- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
+-- INVARIANT:   a->(co,ty)   then   co :: (a~ty)

 -- Not necessarily idemopotent
 
 instance Outputable Refinement where
 -- Not necessarily idemopotent
 
 instance Outputable Refinement where

@@ -401,7 +401,7 @@ isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Apply the refinement to the type.
 -- If (refineType r ty) = (co, ty')
 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Apply the refinement to the type.
 -- If (refineType r ty) = (co, ty')

--- Then co :: ty:=:ty'
+-- Then co :: ty~ty'

 -- Nothing => the refinement does nothing to this type
 refineType (Reft in_scope env) ty
   | not (isEmptyVarEnv env),           -- Common case
 -- Nothing => the refinement does nothing to this type
 refineType (Reft in_scope env) ty
   | not (isEmptyVarEnv env),           -- Common case

@@ -427,7 +427,7 @@ refinePred (Reft in_scope env) pred
 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Like refineType, but returns the 'sym' coercion
 -- If (refineResType r ty) = (co, ty')
 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Like refineType, but returns the 'sym' coercion
 -- If (refineResType r ty) = (co, ty')

--- Then co :: ty':=:ty
+-- Then co :: ty'~ty

 refineResType reft ty
   = case refineType reft ty of
       Just (co, ty1) -> Just (mkSymCoercion co, ty1)
 refineResType reft ty
   = case refineType reft ty of
       Just (co, ty1) -> Just (mkSymCoercion co, ty1)

@@ -617,8 +617,8 @@ uVar :: TvSubstEnv  -- An existing substitution to extend
      -> UM TvSubstEnv
 
 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
      -> UM TvSubstEnv
 
 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that

---     if swap=False   (tv1:=:ty)
---     if swap=True    (ty:=:tv1)
+--     if swap=False   (tv1~ty)
+--     if swap=True    (ty~tv1)

 
 uVar subst tv1 ty
  = -- Check to see whether tv1 is refined by the substitution
 
 uVar subst tv1 ty
  = -- Check to see whether tv1 is refined by the substitution

@@ -640,7 +640,7 @@ uUnrefined subst tv1 ty2 ty2'
   = uUnrefined subst tv1 ty2 ty2''     -- Unwrap synonyms
                -- This is essential, in case we have
                --      type Foo a = a
   = uUnrefined subst tv1 ty2 ty2''     -- Unwrap synonyms
                -- This is essential, in case we have
                --      type Foo a = a

-               -- and then unify a :=: Foo a
+               -- and then unify a ~ Foo a

 
 uUnrefined subst tv1 ty2 (TyVarTy tv2)
   | tv1 == tv2         -- Same type variable
 
 uUnrefined subst tv1 ty2 (TyVarTy tv2)
   | tv1 == tv2         -- Same type variable