Commit 4be195e7 authored by David Feuer's avatar David Feuer Committed by Ben Gamari
Browse files

Simplify Data.Type.Equality.==

Contrary to previous comments, we can calculate `==` for types
in an extremely general fashion. The approach used here is actually
the one mistakenly rejected as impossible. There will be some cases
when the previous version was able to reduce and this one is not,
particularly for types in `*` that are unknown, but known equal.
However, the new behavior is much more uniform. Within the
established framework of equality testing by pattern matching,
it does a better job than the previous version.

Reviewers: goldfire, austin, hvr, bgamari, RyanGlScott

Reviewed By: RyanGlScott

Subscribers: RyanGlScott, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3835
parent f9bf621c
......@@ -191,6 +191,14 @@ Template Haskell
- Blank strings can now be used as values for environment variables using the
System.Environment.Blank module. See :ghc-ticket:`12494`
- ``Data.Type.Equality.==`` is now a closed type family. It works for all kinds
out of the box. Any modules that previously declared instances of this family
will need to remove them. Whereas the previous definition was somewhat ad
hoc, the behavior is now completely uniform. As a result, some applications
that used to reduce no longer do, and conversely. Most notably, ``(==)`` no
longer treats the ``*``, ``j -> k``, or ``()`` kinds specially; equality is
tested structurally in all cases.
Build system
~~~~~~~~~~~~
......
......@@ -34,8 +34,6 @@ import GHC.Base
import GHC.Show
import GHC.Read
import Data.Type.Equality
-- $setup
-- Allow the use of some Prelude functions in doctests.
-- >>> import Prelude ( (+), (*), length, putStrLn )
......@@ -330,13 +328,6 @@ fromRight :: b -> Either a b -> b
fromRight _ (Right b) = b
fromRight b _ = b
-- instance for the == Boolean type-level equality operator
type family EqEither a b where
EqEither ('Left x) ('Left y) = x == y
EqEither ('Right x) ('Right y) = x == y
EqEither a b = 'False
type instance a == b = EqEither a b
{-
{--------------------------------------------------------------------
Testing
......
......@@ -179,164 +179,47 @@ instance TestEquality ((:~:) a) where
instance TestEquality ((:~~:) a) where
testEquality HRefl HRefl = Just Refl
-- | A type family to compute Boolean equality. Instances are provided
-- only for /open/ kinds, such as @*@ and function kinds. Instances are
-- also provided for datatypes exported from base. A poly-kinded instance
-- is /not/ provided, as a recursive definition for algebraic kinds is
-- generally more useful.
type family (a :: k) == (b :: k) :: Bool
infix 4 ==
{-
This comment explains more about why a poly-kinded instance for (==) is
not provided. To be concrete, here would be the poly-kinded instance:
type family EqPoly (a :: k) (b :: k) where
EqPoly a a = True
EqPoly a b = False
type instance (a :: k) == (b :: k) = EqPoly a b
Note that this overlaps with every other instance -- if this were defined,
it would be the only instance for (==).
Now, consider
data Nat = Zero | Succ Nat
Suppose I want
foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
foo = Refl
This would not type-check with the poly-kinded instance. `Succ n == Succ m`
quickly becomes `EqPoly (Succ n) (Succ m)` but then is stuck. We don't know
enough about `n` and `m` to reduce further.
On the other hand, consider this:
type family EqNat (a :: Nat) (b :: Nat) where
EqNat Zero Zero = True
EqNat (Succ n) (Succ m) = EqNat n m
EqNat n m = False
type instance (a :: Nat) == (b :: Nat) = EqNat a b
With this instance, `foo` type-checks fine. `Succ n == Succ m` becomes `EqNat
(Succ n) (Succ m)` which becomes `EqNat n m`. Thus, we can conclude `(n == m)
~ True` as desired.
So, the Nat-specific instance allows strictly more reductions, and is thus
preferable to the poly-kinded instance. But, if we introduce the poly-kinded
instance, we are barred from writing the Nat-specific instance, due to
overlap.
Even better than the current instance for * would be one that does this sort
of recursion for all datatypes, something like this:
type family EqStar (a :: *) (b :: *) where
EqStar Bool Bool = True
EqStar (a,b) (c,d) = a == c && b == d
EqStar (Maybe a) (Maybe b) = a == b
...
EqStar a b = False
The problem is the (...) is extensible -- we would want to add new cases for
all datatypes in scope. This is not currently possible for closed type
families.
-}
-- all of the following closed type families are local to this module
type family EqStar (a :: *) (b :: *) where
EqStar a a = 'True
EqStar a b = 'False
-- This looks dangerous, but it isn't. This allows == to be defined
-- over arbitrary type constructors.
type family EqArrow (a :: k1 -> k2) (b :: k1 -> k2) where
EqArrow a a = 'True
EqArrow a b = 'False
type family EqBool a b where
EqBool 'True 'True = 'True
EqBool 'False 'False = 'True
EqBool a b = 'False
type family EqOrdering a b where
EqOrdering 'LT 'LT = 'True
EqOrdering 'EQ 'EQ = 'True
EqOrdering 'GT 'GT = 'True
EqOrdering a b = 'False
type EqUnit (a :: ()) (b :: ()) = 'True
type family EqList a b where
EqList '[] '[] = 'True
EqList (h1 ': t1) (h2 ': t2) = (h1 == h2) && (t1 == t2)
EqList a b = 'False
type family EqMaybe a b where
EqMaybe 'Nothing 'Nothing = 'True
EqMaybe ('Just x) ('Just y) = x == y
EqMaybe a b = 'False
type family Eq2 a b where
Eq2 '(a1, b1) '(a2, b2) = a1 == a2 && b1 == b2
type family Eq3 a b where
Eq3 '(a1, b1, c1) '(a2, b2, c2) = a1 == a2 && b1 == b2 && c1 == c2
type family Eq4 a b where
Eq4 '(a1, b1, c1, d1) '(a2, b2, c2, d2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2
type family Eq5 a b where
Eq5 '(a1, b1, c1, d1, e1) '(a2, b2, c2, d2, e2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2
type family Eq6 a b where
Eq6 '(a1, b1, c1, d1, e1, f1) '(a2, b2, c2, d2, e2, f2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2
type family Eq7 a b where
Eq7 '(a1, b1, c1, d1, e1, f1, g1) '(a2, b2, c2, d2, e2, f2, g2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2
type family Eq8 a b where
Eq8 '(a1, b1, c1, d1, e1, f1, g1, h1) '(a2, b2, c2, d2, e2, f2, g2, h2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2
type family Eq9 a b where
Eq9 '(a1, b1, c1, d1, e1, f1, g1, h1, i1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2
type family Eq10 a b where
Eq10 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2
type family Eq11 a b where
Eq11 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2
type family Eq12 a b where
Eq12 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2
type family Eq13 a b where
Eq13 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2
type family Eq14 a b where
Eq14 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2
type family Eq15 a b where
Eq15 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2 && o1 == o2
-- these all look to be overlapping, but they are differentiated by their kinds
type instance a == b = EqStar a b
type instance a == b = EqArrow a b
type instance a == b = EqBool a b
type instance a == b = EqOrdering a b
type instance a == b = EqUnit a b
type instance a == b = EqList a b
type instance a == b = EqMaybe a b
type instance a == b = Eq2 a b
type instance a == b = Eq3 a b
type instance a == b = Eq4 a b
type instance a == b = Eq5 a b
type instance a == b = Eq6 a b
type instance a == b = Eq7 a b
type instance a == b = Eq8 a b
type instance a == b = Eq9 a b
type instance a == b = Eq10 a b
type instance a == b = Eq11 a b
type instance a == b = Eq12 a b
type instance a == b = Eq13 a b
type instance a == b = Eq14 a b
type instance a == b = Eq15 a b
-- | A type family to compute Boolean equality.
type family (a :: k) == (b :: k) :: Bool where
f a == g b = f == g && a == b
a == a = 'True
_ == _ = 'False
-- The idea here is to recognize equality of *applications* using
-- the first case, and of *constructors* using the second and third
-- ones. It would be wonderful if GHC recognized that the
-- first and second cases are compatible, which would allow us to
-- prove
--
-- a ~ b => a == b
--
-- but it (understandably) does not.
--
-- It is absolutely critical that the three cases occur in precisely
-- this order. In particular, if
--
-- a == a = 'True
--
-- came first, then the type application case would only be reached
-- (uselessly) when GHC discovered that the types were not equal.
--
-- One might reasonably ask what's wrong with a simpler version:
--
-- type family (a :: k) == (b :: k) where
-- a == a = True
-- a == b = False
--
-- Consider
-- data Nat = Zero | Succ Nat
--
-- Suppose I want
-- foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
-- foo = Refl
--
-- This would not type-check with the simple version. `Succ n == Succ m`
-- is stuck. We don't know enough about `n` and `m` to reduce the family.
-- With the recursive version, `Succ n == Succ m` reduces to
-- `Succ == Succ && n == m`, which can reduce to `'True && n == m` and
-- finally to `n == m`.
......@@ -9,7 +9,6 @@
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-} -- for compiling instances of (==)
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
......@@ -44,7 +43,7 @@ module GHC.TypeLits
) where
import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
import GHC.Base(Eq(..), Ord(..), Ordering(..), otherwise)
import GHC.Types( Nat, Symbol )
import GHC.Num(Integer, fromInteger)
import GHC.Base(String)
......@@ -54,7 +53,7 @@ import GHC.Real(toInteger)
import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality(type (==), (:~:)(Refl))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)
import GHC.TypeNats (KnownNat)
......@@ -122,11 +121,6 @@ instance Show SomeSymbol where
instance Read SomeSymbol where
readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
type family EqSymbol (a :: Symbol) (b :: Symbol) where
EqSymbol a a = 'True
EqSymbol a b = 'False
type instance a == b = EqSymbol a b
--------------------------------------------------------------------------------
-- | Comparison of type-level symbols, as a function.
......
......@@ -9,7 +9,6 @@
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-} -- for compiling instances of (==)
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
......@@ -37,7 +36,7 @@ module GHC.TypeNats
) where
import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
import GHC.Types( Nat )
import GHC.Natural(Natural)
import GHC.Show(Show(..))
......@@ -45,7 +44,7 @@ import GHC.Read(Read(..))
import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality(type (==), (:~:)(Refl))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)
--------------------------------------------------------------------------------
......@@ -95,11 +94,6 @@ instance Read SomeNat where
readsPrec p xs = do (a,ys) <- readsPrec p xs
[(someNatVal a, ys)]
type family EqNat (a :: Nat) (b :: Nat) where
EqNat a a = 'True
EqNat a b = 'False
type instance a == b = EqNat a b
--------------------------------------------------------------------------------
infix 4 <=?, <=
......
......@@ -20,6 +20,14 @@
* Remove the deprecated `Typeable{1..7}` type synonyms (#14047)
* Make `Data.Type.Equality.==` a closed type family. It now works for all
kinds out of the box. Any modules that previously declared instances of this
family will need to remove them. Whereas the previous definition was somewhat
ad hoc, the behavior is now completely uniform. As a result, some applications
that used to reduce no longer do, and conversely. Most notably, `(==)` no
longer treats the `*`, `j -> k`, or `()` kinds specially; equality is
tested structurally in all cases.
* Add instances `Semigroup` and `Monoid` for `Control.Monad.ST` (#14107).
* The `Read` instances for `Proxy`, `Coercion`, `(:~:)`, `(:~~:)`, and `U1`
......
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