[Git][ghc/ghc][master] Make typechecker equality consider visibility in ForAllTys
Marge Bot
gitlab at gitlab.haskell.org
Sat Oct 31 06:54:04 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
57c3db96 by Ryan Scott at 2020-10-31T02:53:55-04:00
Make typechecker equality consider visibility in ForAllTys
Previously, `can_eq_nc'` would equate `ForAllTy`s regardless of their
`ArgFlag`, including `forall i -> i -> Type` and `forall i. i -> Type`! To fix
this, `can_eq_nc'` now uses the `sameVis` function to first check if the
`ArgFlag`s are equal modulo specificity. I have also updated `tcEqType`'s
implementation to match this behavior. For more explanation on the "modulo
specificity" part, see the new `Note [ForAllTy and typechecker equality]`
in `GHC.Tc.Solver.Canonical`.
While I was in town, I fixed some related documentation issues:
* I added `Note [Typechecker equality]` to `GHC.Tc.Utils.TcType` to describe
what exactly distinguishes `can_eq_nc'` and `tcEqType` (which implement
typechecker equality) from `eqType` (which implements definitional equality,
which does not care about the `ArgFlags` of `ForAllTy`s at all).
* The User's Guide had some outdated prose on the specified/inferred
distinction being different for types and kinds, a holdover from #15079. This
is no longer the case on today's GHC, so I removed this prose, added some new
prose to take its place, and added a regression test for the programs in
#15079.
* The User's Guide had some _more_ outdated prose on inferred type variables
not being allowed in `default` type signatures for class methods, which is no
longer true as of the resolution of #18432.
* The related `Note [Deferred Unification]` was being referenced as
`Note [Deferred unification]` elsewhere, which made it harder to `grep`
for. I decided to change the name of the Note to `Deferred unification`
for consistency with the capitalization style used for most other Notes.
Fixes #18863.
- - - - -
14 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- docs/users_guide/exts/poly_kinds.rst
- docs/users_guide/exts/type_applications.rst
- + testsuite/tests/saks/should_fail/T18863a.hs
- + testsuite/tests/saks/should_fail/T18863a.stderr
- + testsuite/tests/saks/should_fail/T18863b.hs
- + testsuite/tests/saks/should_fail/T18863b.stderr
- testsuite/tests/saks/should_fail/all.T
- + testsuite/tests/typecheck/should_compile/T15079.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -485,6 +485,12 @@ Another helpful principle with eqType is this:
This principle also tells us that eqType must relate only types with the
same kinds.
+Besides eqType, another equality relation that upholds the (EQ) property above
+is /typechecker equality/, which is implemented as
+GHC.Tc.Utils.TcType.tcEqType. See
+Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType for
+what the difference between eqType and tcEqType is.
+
Note [Respecting definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Non-trivial definitional equality] introduces the property (EQ).
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -2236,7 +2236,7 @@ eqVarBndrs _ _ _= Nothing
{-
Note [nonDetCmpType nondeterminism]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
@@ -2926,7 +2926,7 @@ splitVisVarsOfTypes = foldMap splitVisVarsOfType
************************************************************************
Note [Kind Constraint and kind Type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The kind Constraint is the kind of classes and other type constraints.
The special thing about types of kind Constraint is that
* They are displayed with double arrow:
@@ -2945,6 +2945,18 @@ generates an axiom witnessing
so on the left we have Constraint, and on the right we have Type.
See #7451.
+Because we treat Constraint/Type differently during and after type inference,
+GHC has two notions of equality that differ in whether they equate
+Constraint/Type or not:
+
+* GHC.Tc.Utils.TcType.tcEqType implements typechecker equality (see
+ Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType),
+ which treats Constraint and Type as distinct. This is used during type
+ inference. See #11715 for issues that arise from this.
+* GHC.Core.TyCo.Rep.eqType implements definitional equality (see
+ Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep), which treats
+ Constraint and Type as equal. This is used after type inference.
+
Bottom line: although 'Type' and 'Constraint' are distinct TyCons, with
distinct uniques, they are treated as equal at all times except
during type inference.
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1035,7 +1035,9 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
= canTyConApp ev eq_rel tc1 tys1 tc2 tys2
can_eq_nc' _flat _rdr_env _envs ev eq_rel
- s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
+ s1@(ForAllTy (Bndr _ vis1) _) _
+ s2@(ForAllTy (Bndr _ vis2) _) _
+ | vis1 `sameVis` vis2 -- Note [ForAllTy and typechecker equality]
= can_eq_nc_forall ev eq_rel s1 s2
-- See Note [Canonicalising type applications] about why we require flat types
@@ -1071,6 +1073,63 @@ If we have an unsolved equality like
that is not necessarily insoluble! Maybe 'a' will turn out to be a newtype.
So we want to make it a potentially-soluble Irred not an insoluble one.
Missing this point is what caused #15431
+
+Note [ForAllTy and typechecker equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should GHC type-check the following program (adapted from #15740)?
+
+ {-# LANGUAGE PolyKinds, ... #-}
+ data D a
+ type family F :: forall k. k -> Type
+ type instance F = D
+
+Due to the way F is declared, any instance of F must have a right-hand side
+whose kind is equal to `forall k. k -> Type`. The kind of D is
+`forall {k}. k -> Type`, which is very close, but technically uses distinct
+Core:
+
+ -----------------------------------------------------------
+ | Source Haskell | Core |
+ -----------------------------------------------------------
+ | forall k. <...> | ForAllTy (Bndr k Specified) (<...>) |
+ | forall {k}. <...> | ForAllTy (Bndr k Inferred) (<...>) |
+ -----------------------------------------------------------
+
+We could deem these kinds to be unequal, but that would imply rejecting
+programs like the one above. Whether a kind variable binder ends up being
+specified or inferred can be somewhat subtle, however, especially for kinds
+that aren't explicitly written out in the source code (like in D above).
+For now, we decide to not make the specified/inferred status of an invisible
+type variable binder affect GHC's notion of typechecker equality
+(see Note [Typechecker equality vs definitional equality] in
+GHC.Tc.Utils.TcType). That is, we have the following:
+
+ --------------------------------------------------
+ | Type 1 | Type 2 | Equal? |
+ --------------------|-----------------------------
+ | forall k. <...> | forall k. <...> | Yes |
+ | | forall {k}. <...> | Yes |
+ | | forall k -> <...> | No |
+ --------------------------------------------------
+ | forall {k}. <...> | forall k. <...> | Yes |
+ | | forall {k}. <...> | Yes |
+ | | forall k -> <...> | No |
+ --------------------------------------------------
+ | forall k -> <...> | forall k. <...> | No |
+ | | forall {k}. <...> | No |
+ | | forall k -> <...> | Yes |
+ --------------------------------------------------
+
+We implement this nuance by using the GHC.Types.Var.sameVis function in
+GHC.Tc.Solver.Canonical.canEqNC and GHC.Tc.Utils.TcType.tcEqType, which
+respect typechecker equality. sameVis puts both forms of invisible type
+variable binders into the same equivalence class.
+
+Note that we do /not/ use sameVis in GHC.Core.Type.eqType, which implements
+/definitional/ equality, a slighty more coarse-grained notion of equality
+(see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep) that does
+not consider the ArgFlag of ForAllTys at all. That is, eqType would equate all
+of forall k. <...>, forall {k}. <...>, and forall k -> <...>.
-}
---------------------------------
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1506,9 +1506,8 @@ tcEqKind :: HasDebugCallStack => TcKind -> TcKind -> Bool
tcEqKind = tcEqType
tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool
--- tcEqType is a proper implements the same Note [Non-trivial definitional
--- equality] (in GHC.Core.TyCo.Rep) as `eqType`, but Type.eqType believes (* ==
--- Constraint), and that is NOT what we want in the type checker!
+-- ^ tcEqType implements typechecker equality, as described in
+-- @Note [Typechecker equality vs definitional equality]@.
tcEqType ty1 ty2
= tc_eq_type False False ki1 ki2
&& tc_eq_type False False ty1 ty2
@@ -1557,7 +1556,9 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
go env (ForAllTy (Bndr tv1 vis1) ty1)
(ForAllTy (Bndr tv2 vis2) ty2)
- = vis1 == vis2
+ = vis1 `sameVis` vis2
+ -- See Note [ForAllTy and typechecker equality] in
+ -- GHC.Tc.Solver.Canonical for why we use `sameVis` here
&& (vis_only || go env (varType tv1) (varType tv2))
&& go (rnBndr2 env tv1 tv2) ty1 ty2
@@ -1622,6 +1623,29 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
get_args _ _ = False
eqFunTy _ _ _ _ _ = False
+{- Note [Typechecker equality vs definitional equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC has two notions of equality over Core types:
+
+* Definitional equality, as implemented by GHC.Core.Type.eqType.
+ See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep.
+* Typechecker equality, as implemented by tcEqType (in GHC.Tc.Utils.TcType).
+ GHC.Tc.Solver.Canonical.canEqNC also respects typechecker equality.
+
+Typechecker equality implies definitional equality: if two types are equal
+according to typechecker equality, then they are also equal according to
+definitional equality. The converse is not always true, as typechecker equality
+is more finer-grained than definitional equality in two places:
+
+* Unlike definitional equality, which equates Type and Constraint, typechecker
+ treats them as distinct types. See Note [Kind Constraint and kind Type] in
+ GHC.Core.Type.
+* Unlike definitional equality, which does not care about the ArgFlag of a
+ ForAllTy, typechecker equality treats Required type variable binders as
+ distinct from Invisible type variable binders.
+ See Note [ForAllTy and typechecker equality] in GHC.Tc.Solver.Canonical.
+-}
+
{- *********************************************************************
* *
Predicate types
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1321,7 +1321,7 @@ We expand synonyms during unification, but:
This is particularly helpful when checking (* ~ *), because * is
now a type synonym.
-Note [Deferred Unification]
+Note [Deferred unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
and yet its consistency is undetermined. Previously, there was no way to still
=====================================
docs/users_guide/exts/poly_kinds.rst
=====================================
@@ -769,24 +769,6 @@ In this redefinition, we give an explicit kind for ``(:~~:)``, deferring the cho
of ``k2`` until after the first argument (``a``) has been given. With this declaration
for ``(:~~:)``, the instance for ``HTestEquality`` is accepted.
-Another difference between higher-rank kinds and types can be found in their
-treatment of inferred and user-specified type variables. Consider the following
-program: ::
-
- newtype Foo (f :: forall k. k -> Type) = MkFoo (f Int)
- data Proxy a = Proxy
-
- foo :: Foo Proxy
- foo = MkFoo Proxy
-
-The kind of ``Foo``'s parameter is ``forall k. k -> Type``, but the kind of
-``Proxy`` is ``forall {k}. k -> Type``, where ``{k}`` denotes that the kind
-variable ``k`` is to be inferred, not specified by the user. (See
-:ref:`visible-type-application` for more discussion on the inferred-specified
-distinction). GHC does not consider ``forall k. k -> Type`` and
-``forall {k}. k -> Type`` to be equal at the kind level, and thus rejects
-``Foo Proxy`` as ill-kinded.
-
The kind ``Type``
-----------------
=====================================
docs/users_guide/exts/type_applications.rst
=====================================
@@ -246,8 +246,7 @@ The braces are *not* allowed in the following places:
explicitly applied. Making them inferred (and thus not appliable) would be
conflicting.
-- In default type signatures for class methods, in SPECIALISE pragmas or in
- instance declaration heads, e.g.::
+- In SPECIALISE pragmas or in instance declaration heads, e.g.::
instance forall {a}. Eq (Maybe a) where ...
@@ -256,3 +255,22 @@ The braces are *not* allowed in the following places:
could play a role.
- On the left-hand sides of type declarations, such as classes, data types, etc.
+
+Note that while specified and inferred type variables have different properties
+vis-à-vis visible type application, they do not otherwise affect GHC's notion
+of equality over types. For example, given the following definitions: ::
+
+ id1 :: forall a. a -> a
+ id1 x = x
+
+ id2 :: forall {a}. a -> a
+ id2 x = x
+
+ app1 :: (forall a. a -> a) -> b -> b
+ app1 g x = g x
+
+ app2 :: (forall {a}. a -> a) -> b -> b
+ app2 g x = g x
+
+GHC will deem all of ``app1 id1``, ``app1 id2``, ``app2 id1``, and ``app2 id2``
+to be well typed.
=====================================
testsuite/tests/saks/should_fail/T18863a.hs
=====================================
@@ -0,0 +1,9 @@
+{-# Language PolyKinds #-}
+{-# Language RankNTypes #-}
+{-# Language StandaloneKindSignatures #-}
+module T18863a where
+
+import Data.Kind
+
+type IDa :: forall i -> i -> Type
+data IDa :: forall i. i -> Type
=====================================
testsuite/tests/saks/should_fail/T18863a.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18863a.hs:9:1: error:
+ • Couldn't match expected kind: forall i. i -> *
+ with actual kind: forall i -> i -> *
+ • In the data type declaration for ‘IDa’
=====================================
testsuite/tests/saks/should_fail/T18863b.hs
=====================================
@@ -0,0 +1,9 @@
+{-# Language PolyKinds #-}
+{-# Language RankNTypes #-}
+{-# Language StandaloneKindSignatures #-}
+module T18863b where
+
+import Data.Kind
+
+type IDb :: forall i. i -> Type
+data IDb :: forall i -> i -> Type
=====================================
testsuite/tests/saks/should_fail/T18863b.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18863b.hs:9:1: error:
+ • Couldn't match expected kind: forall i -> i -> *
+ with actual kind: i -> *
+ • In the data type declaration for ‘IDb’
=====================================
testsuite/tests/saks/should_fail/all.T
=====================================
@@ -31,3 +31,5 @@ test('T16725', normal, compile_fail, [''])
test('T16826', normal, compile_fail, [''])
test('T16756b', normal, compile_fail, [''])
test('T16758', normal, compile_fail, [''])
+test('T18863a', normal, compile_fail, [''])
+test('T18863b', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_compile/T15079.hs
=====================================
@@ -0,0 +1,64 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T15079 where
+
+import Data.Kind
+import qualified Data.Type.Equality as Eq
+import Data.Void
+import GHC.Exts (Any)
+
+infixl 4 :==
+-- | Heterogeneous Leibnizian equality.
+newtype (a :: j) :== (b :: k)
+ = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
+
+-----
+
+newtype Coerce a = Coerce { uncoerce :: Starify a }
+type family Starify (a :: k) :: Type where
+ Starify (a :: Type) = a
+ Starify _ = Void
+
+coerce :: a :== b -> a -> b
+coerce f = uncoerce . hsubst f . Coerce
+
+-----
+
+newtype Flay :: (forall (i :: Type). i -> i -> Type)
+ -> forall (j :: Type). j -> forall (k :: Type). k -> Type where
+ Flay :: forall (p :: forall (i :: Type). i -> i -> Type)
+ (j :: Type) (k :: Type) (a :: j) (b :: k).
+ { unflay :: p a (MassageKind j b) } -> Flay p a b
+
+type family MassageKind (j :: Type) (a :: k) :: j where
+ MassageKind j (a :: j) = a
+ MassageKind _ _ = Any
+
+fromLeibniz :: forall a b. a :== b -> a Eq.:~: b
+fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl
+
+-----
+
+newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int)
+data InferredProxy a = MkInferredProxy
+
+foo :: Foo InferredProxy
+foo = MkFoo MkInferredProxy
+
+-----
+
+id1 :: forall a. a -> a
+id1 x = x
+
+id2 :: forall {a}. a -> a
+id2 x = x
+
+app1 :: (forall a. a -> a) -> b -> b
+app1 g x = g x
+
+app2 :: (forall {a}. a -> a) -> b -> b
+app2 g x = g x
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -627,6 +627,7 @@ test('SplitWD', normal, compile, [''])
# (2) Build the program twice: once with -dynamic, and then
# with -prof using -osuf to set a different object file suffix.
test('T14441', omit_ways(['profasm']), compile, [''])
+test('T15079', normal, compile, [''])
test('T15050', normal, compile, [''])
test('T14735', normal, compile, [''])
test('T15180', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57c3db9612463426e1724816fd3f98142fec0e31
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57c3db9612463426e1724816fd3f98142fec0e31
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/20201031/0d68ae6e/attachment-0001.html>
More information about the ghc-commits
mailing list