[Git][ghc/ghc][wip/int-index/core-ignore-forall-vis] [skip ci] Editing

[Vladislav Zavialov (@int-index)]

Vladislav Zavialov pushed to branch wip/int-index/core-ignore-forall-vis at Glasgow Haskell Compiler / GHC


Commits:
25f0afa3 by Vladislav Zavialov at 2023-06-06T08:29:12+02:00
[skip ci] Editing

- - - - -


1 changed file:

- compiler/GHC/Core/TyCo/Compare.hs


Changes:

=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -257,7 +257,7 @@ We call those properties *visibility* and *specificity* respectively.
 Visibility and specificity are jointly represented by the `ForallTyFlag` data
 type. The interaction between this flag and type equality is tricky:
   * Definitional equality (eqType) completly ignores the flag
-  * Typechecker equality (tcEqType, can_eq_nc) respect visibility but ignore specificity
+  * Typechecker equality (tcEqType, can_eq_nc) respects visibility but ignores specificity
 
 This is not the only possible design, so we describe the design space below.
 Since visibility and specificity are different properties, we cover them
@@ -284,7 +284,7 @@ The Core terms for `idv` and `id` are identical, while the types are different.
 That's not possible because we should be able to determine the type from the term:
     exprType :: CoreExpr -> Type
 
-So the question becomes: which forall visibility should we `exprType` return
+So the question becomes: which forall visibility should `exprType` return
 when faced with (/\a -> e), is it (forall a. t) or (forall a -> t)?
 The term alone doesn't contain enough information to make this choice.
 
@@ -300,6 +300,7 @@ There are two ways we could address this:
   b) Declare `forall a -> t` and `forall a. t` nominally equal and
      ignore the visibility flag in `eqType`
         eqType :: Type -> Type -> Bool
+     This way `exprType` can always generate invisible foralls because it won't matter.
      This begs the question: why not remove visibilities from Core syntax
      altogether? The answer is that it's not possible because Core types are
      also used in parts of the compiler we the distinction does matter:
@@ -318,7 +319,6 @@ lint will accept the following:
 
 We are able to assign `idv = id` despite the difference in visibilities.
 There are no casts involved.
-`exprType` can always generate invisible foralls because it won't matter.
 
 At the same time, we want to reject such programs in surface Haskell,
 where users care about the distinction between visible and invisible forall.



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/25f0afa3b1db85c08f74b48a30411ac6f27e39aa

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/25f0afa3b1db85c08f74b48a30411ac6f27e39aa
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230606/4977151e/attachment-0001.html>