PmCheck - Comments only: Replace /~ by ≁

3 files changed, 33 insertions, 33 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index 9b9ce9d700..831509d351 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -221,7 +221,7 @@ safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
 exception into divergence (@f x = f x@).
 
 Semantically, unlike every other case expression, -XEmptyCase is strict in its
-match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the
+match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
 initial Nabla and check if there are any values left to match on.
 -}
 
@@ -786,7 +786,7 @@ Note [Strict fields and fields of unlifted type]
 How do strict fields play into Note [Field match order for RecCon]? Answer:
 They don't. Desugaring is entirely unconcerned by strict fields; the forcing
 happens *before* pattern matching. But for each strict (or more generally,
-unlifted) field @s@ we have to add @s /~ ⊥@ constraints when we check the PmCon
+unlifted) field @s@ we have to add @s ≁ ⊥@ constraints when we check the PmCon
 guard in 'checkGrd'. Strict fields are devoid of ⊥ by construction, there's
 nothing that a bang pattern would act on. Example from #18341:
 
@@ -798,7 +798,7 @@ nothing that a bang pattern would act on. Example from #18341:
 
 The second clause desugars to @MkT n <- x, !n@. When coverage checked, the
 'PmCon' @MkT n <- x@ refines the set of values that reach the bang pattern with
-the constraints @x ~ MkT n, n /~ ⊥@ (this list is computed by 'pmConCts').
+the constraints @x ~ MkT n, n ≁ ⊥@ (this list is computed by 'pmConCts').
 Checking the 'PmBang' @!n@ will then try to add the constraint @n ~ ⊥@ to this
 set to get the diverging set, which is found to be empty. Hence the whole
 clause is detected as redundant, as expected.
@@ -942,7 +942,7 @@ throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
 -- These include
 --
 --   * @gammas@: Constraints arising from the bound evidence vars
---   * @y /~ ⊥@ constraints for each unlifted field (including strict fields)
+--   * @y ≁ ⊥@ constraints for each unlifted field (including strict fields)
 --     @y@ in @ys@
 --   * The constructor constraint itself: @x ~ T as ys@.
 --
@@ -974,7 +974,7 @@ checkGrd grd = CA $ \inc -> case grd of
     pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
                      , cr_uncov = mempty
                      , cr_approx = Precise }
-  -- Bang x _: Diverge on x ~ ⊥, refine with x /~ ⊥
+  -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
   PmBang x mb_info -> do
     div <- addPmCtNablas inc (PmBotCt x)
     matched <- addPmCtNablas inc (PmNotBotCt x)
@@ -986,7 +986,7 @@ checkGrd grd = CA $ \inc -> case grd of
     pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
                      , cr_uncov = mempty
                      , cr_approx = Precise }
-  -- Con: Fall through on x /~ K and refine with x ~ K ys and type info
+  -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
   PmCon x con tvs dicts args -> do
     !div <- if isPmAltConMatchStrict con
       then addPmCtNablas inc (PmBotCt x)
@@ -1048,7 +1048,7 @@ How do we do that? Consider
 
 And imagine we set our limit to 1 for the sake of the example. The first clause
 will be checked against the initial Nabla, {}. Doing so will produce an
-Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}.
+Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
 Also we find the first clause to cover the model {x~True,y~True}.
 
 But the Uncovered set we get out of the match is too huge! We somehow have to
@@ -1056,8 +1056,8 @@ ensure not to make things worse as they are already, so we continue checking
 with a singleton Uncovered set of the initial Nabla {}. Why is this
 sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
 to forgetting that we matched against the first clause. The values represented
-by {} are a superset of those represented by its two refinements {x/~True} and
-{x~True,y/~True}.
+by {} are a superset of those represented by its two refinements {x≁True} and
+{x~True,y≁True}.
 
 This forgetfulness becomes very apparent in the example above: By continuing
 with {} we don't detect the second clause as redundant, as it again covers the
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index e3f4cec57b..492e993f19 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -628,10 +628,10 @@ Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos',
 any entry in 'vi_neg' must be incomparable to C (return Nothing) according to
 'eqPmAltCons'. Those entries that are comparable either lead to a refutation
 or are redundant. Examples:
-* @x ~ Just y@, @x /~ [Just]@. 'eqPmAltCon' returns @Equal@, so refute.
-* @x ~ Nothing@, @x /~ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative
+* @x ~ Just y@, @x ≁ [Just]@. 'eqPmAltCon' returns @Equal@, so refute.
+* @x ~ Nothing@, @x ≁ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative
   info is redundant and should be discarded.
-* @x ~ I# y@, @x /~ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal.
+* @x ~ I# y@, @x ≁ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal.
   We keep this info in order to be able to refute a redundant match on i.e. 4
   later on.
 
@@ -676,19 +676,19 @@ oracle) contradictory. This implies a few invariants:
 Maintaining these invariants in 'addVarCt' (the core of the term oracle) and
 'addNotConCt' is subtle.
 * Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate').
-  - (COMPLETE) If we had @x /~ True@ and @y /~ False@, then we get
-    @x /~ [True,False]@. This is vacuous by matter of comparing to the built-in
+  - (COMPLETE) If we had @x ≁ True@ and @y ≁ False@, then we get
+    @x ≁ [True,False]@. This is vacuous by matter of comparing to the built-in
     COMPLETE set, so should refute.
-  - (Pos/Neg) If we had @x /~ True@ and @y ~ True@, we have to refute.
+  - (Pos/Neg) If we had @x ≁ True@ and @y ~ True@, we have to refute.
 * Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt')
-  - (Neg) If we had @x /~ K@, refute.
+  - (Neg) If we had @x ≁ K@, refute.
   - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to
     'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute.
-  - (Refine) If we had @x /~ K zs@, unify each y with each z in turn.
-* Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addNotConCt')
+  - (Refine) If we had @x ≁ K zs@, unify each y with each z in turn.
+* Adding negative information. Example: Add the fact @x ≁ Nothing@ (see 'addNotConCt')
   - (Refut) If we have @x ~ K ys@, refute.
-  - (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get
-    @x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in
+  - (COMPLETE) If K=Nothing and we had @x ≁ Just@, then we get
+    @x ≁ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in
     COMPLETE set, so should refute.
 
 Note that merging VarInfo in equate can be done by calling out to 'addConCt' and
@@ -783,10 +783,10 @@ clause as redundant, which clearly is unsound. The solution:
 1. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a
    newtype match is lazy.
 2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@)
-   to @y@, similar to what 'equate' does, and don't add a @x /~ ⊥@ constraint.
+   to @y@, similar to what 'equate' does, and don't add a @x ≁ ⊥@ constraint.
    This way, the third clause will still be marked as inaccessible RHS instead
    of redundant. This is ensured by calling 'lookupVarInfoNT'.
-3. Immediately reject when we find @x /~ T2@.
+3. Immediately reject when we find @x ≁ T2@.
 Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper,
 where you can find the solution in a perhaps more digestible format.
 -}
@@ -826,13 +826,13 @@ data TmCt
   -- ^ @TmConCt x K tvs ys@ encodes "x ~ K @tvs ys", equating @x@ with the 'PmAltCon'
   -- application @K @tvs ys@.
   | TmNotConCt  !Id !PmAltCon
-  -- ^ @TmNotConCt x K@ encodes "x /~ K", asserting that @x@ can't be headed
+  -- ^ @TmNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed
   -- by @K@.
   | TmBotCt     !Id
   -- ^ @TmBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
   -- by @K@.
   | TmNotBotCt !Id
-  -- ^ @TmNotBotCt x y@ encodes "x /~ ⊥", asserting that @x@ can't be ⊥.
+  -- ^ @TmNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥.
 
 instance Outputable TmCt where
   ppr (TmVarCt x y)            = ppr x <+> char '~' <+> ppr y
@@ -841,9 +841,9 @@ instance Outputable TmCt where
     where
       pp_tvs  = map ((<> char '@') . ppr) tvs
       pp_args = map ppr args
-  ppr (TmNotConCt x con)       = ppr x <+> text "/~" <+> ppr con
+  ppr (TmNotConCt x con)       = ppr x <+> text "≁" <+> ppr con
   ppr (TmBotCt x)              = ppr x <+> text "~ ⊥"
-  ppr (TmNotBotCt x)           = ppr x <+> text "/~ ⊥"
+  ppr (TmNotBotCt x)           = ppr x <+> text "≁ ⊥"
 
 type TyCt = PredType
 
@@ -908,7 +908,7 @@ addBotCt :: Nabla -> Id -> MaybeT DsM Nabla
 addBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do
   let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
   case bot of
-    IsNotBot -> mzero      -- There was x /~ ⊥. Contradiction!
+    IsNotBot -> mzero      -- There was x ≁ ⊥. Contradiction!
     IsBot    -> pure nabla -- There already is x ~ ⊥. Nothing left to do
     MaybeBot -> do         -- We add x ~ ⊥
       let vi' = vi{ vi_bot = IsBot }
@@ -1015,8 +1015,8 @@ addNotBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do
   let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
   case bot of
     IsBot    -> mzero      -- There was x ~ ⊥. Contradiction!
-    IsNotBot -> pure nabla -- There already is x /~ ⊥. Nothing left to do
-    MaybeBot -> do         -- We add x /~ ⊥ and test if x is still inhabited
+    IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do
+    MaybeBot -> do         -- We add x ≁ ⊥ and test if x is still inhabited
       vi <- ensureInhabited nabla vi{ vi_bot = IsNotBot }
       pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi) reps}
 
@@ -1776,7 +1776,7 @@ addCoreCt nabla x e = do
 
     -- | Look at @let x = K taus theta es@ and generate the following
     -- constraints (assuming universals were dropped from @taus@ before):
-    --   1. @x /~ ⊥@ if 'K' is not a Newtype constructor.
+    --   1. @x ≁ ⊥@ if 'K' is not a Newtype constructor.
     --   2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@
     --   3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
     --   4. @x ~ K as ys@
@@ -1791,7 +1791,7 @@ addCoreCt nabla x e = do
       uniq_supply <- lift $ lift $ getUniqueSupplyM
       let (_, ex_tvs) = cloneTyVarBndrs (mkEmptyTCvSubst in_scope) dc_ex_tvs uniq_supply
           ty_cts      = equateTys (map mkTyVarTy ex_tvs) ex_tys
-      -- 1. @x /~ ⊥@ if 'K' is not a Newtype constructor (#18341)
+      -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor (#18341)
       when (not (isNewDataCon dc)) $
         modifyT $ \nabla -> addNotBotCt nabla x
       -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index 12bd5f32fb..4602b89611 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -416,7 +416,7 @@ instance Outputable PmEquality where
 
 -- | A data type that caches for the 'VarInfo' of @x@ the results of querying
 -- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
--- which we already know @x /~ K@ from these sets.
+-- which we already know @x ≁ K@ from these sets.
 --
 -- For motivation, see Section 5.3 in Lower Your Guards.
 -- See also Note [Implementation of COMPLETE pragmas]
@@ -552,7 +552,7 @@ data VarInfo
   --     data T = Leaf Int | Branch T T | Node Int T
   -- @
   --
-  -- then @x /~ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
+  -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
   -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
   -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
   -- between 'vi_pos' and 'vi_neg'.