Commit 5e5310b3 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

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

parent fbbd2bfa
......@@ -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
[a] :: [a]:=:[a]
[a] :: [a]~[a]
INVARIANT: the dictionary constructor for a class
never has a wrapper.
......@@ -246,14 +246,14 @@ data DataCon
-- *** 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]
-- dcEqSpec = [a:=:(x,y)]
-- dcEqSpec = [a~(x,y)]
-- 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:
-- MkT :: forall a b. (a :=: [b]) => b -> T a
-- MkT :: forall a b. (a ~ [b]) => b -> T a
-- 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
......@@ -346,7 +346,7 @@ data DataCon
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)
......@@ -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
-- 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.
......
......@@ -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
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
......
......@@ -289,7 +289,7 @@ mkTcTyVar name kind details
\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
......
......@@ -740,12 +740,12 @@ dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
-- ...
--
-- 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
--
-- ([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
......@@ -801,7 +801,7 @@ exprIsConApp_maybe (Cast expr 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.)
......
......@@ -164,6 +164,8 @@ data HsExpr 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
......
......@@ -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
-- `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
......
......@@ -238,7 +238,7 @@ ppr_tc tc = ppr tc
-------------------
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)
......
......@@ -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
-- 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:
......@@ -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)))
-- 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
......
......@@ -568,7 +568,7 @@ the split arguments for the representation tycon :R123Map as {Int, c, w}
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
......@@ -594,7 +594,7 @@ to express the local scope of GADT refinements.
\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
......
......@@ -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}.
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.
......
......@@ -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
-- ([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
......
......@@ -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
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.
......@@ -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 ?? = *
-- What about (kv -> *) :=: ?? -> *
-- What about (kv -> *) ~ ?? -> *
kindSimpleKind orig_swapped orig_kind
= go orig_swapped orig_kind
where
......
......@@ -74,14 +74,14 @@ import FastString
-- | 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
------------------------------
-- | 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]
......@@ -134,7 +134,7 @@ splitCoercionKind_maybe _ = Nothing
-- | 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'
......@@ -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
-- 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
......@@ -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
-- 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
......@@ -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)
TyConApp rep_tycon args) -- :=: R tys
TyConApp rep_tycon args) -- ~ R tys
--------------------------------------
-- 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...
--
-- 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
......
......@@ -203,7 +203,7 @@ type Equation = (TyVarSet, [(Type, Type)])
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
......@@ -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
-- (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
......
......@@ -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
-- 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.
......@@ -211,7 +211,7 @@ data TyCon
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,
......@@ -393,7 +393,7 @@ newtype, to the newtype itself. For example,
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
......@@ -403,11 +403,11 @@ ending with the same type variables as the left hand side, we
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
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])
......@@ -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
axiom CoT t : T t :=: [t]
axiom CoT t : T t ~ [t]
Note [Newtype eta]
~~~~~~~~~~~~~~~~~~
......
......@@ -384,7 +384,7 @@ dataConCannotMatch tys con
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
......@@ -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')
-- 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
......@@ -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')
-- Then co :: ty':=:ty
-- Then co :: ty'~ty
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
-- 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
......@@ -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
-- and then unify a :=: Foo a
-- and then unify a ~ Foo a
uUnrefined subst tv1 ty2 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable
......
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