diff options
author | Richard Eisenberg <eir@cis.upenn.edu> | 2015-12-11 18:19:53 -0500 |
---|---|---|
committer | Richard Eisenberg <eir@cis.upenn.edu> | 2015-12-11 18:23:12 -0500 |
commit | 6746549772c5cc0ac66c0fce562f297f4d4b80a2 (patch) | |
tree | 96869fcfb5757651462511d64d99a3712f09e7fb /libraries/base | |
parent | 6e56ac58a6905197412d58e32792a04a63b94d7e (diff) | |
download | haskell-6746549772c5cc0ac66c0fce562f297f4d4b80a2.tar.gz |
Add kind equalities to GHC.
This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).
There are several noteworthy changes with this patch:
* We now have casts in types. These change the kind
of a type. See new constructor `CastTy`.
* All types and all constructors can be promoted.
This includes GADT constructors. GADT pattern matches
take place in type family equations. In Core,
types can now be applied to coercions via the
`CoercionTy` constructor.
* Coercions can now be heterogeneous, relating types
of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
proves both that `t1` and `t2` are the same and also that
`k1` and `k2` are the same.
* The `Coercion` type has been significantly enhanced.
The documentation in `docs/core-spec/core-spec.pdf` reflects
the new reality.
* The type of `*` is now `*`. No more `BOX`.
* Users can write explicit kind variables in their code,
anywhere they can write type variables. For backward compatibility,
automatic inference of kind-variable binding is still permitted.
* The new extension `TypeInType` turns on the new user-facing
features.
* Type families and synonyms are now promoted to kinds. This causes
trouble with parsing `*`, leading to the somewhat awkward new
`HsAppsTy` constructor for `HsType`. This is dispatched with in
the renamer, where the kind `*` can be told apart from a
type-level multiplication operator. Without `-XTypeInType` the
old behavior persists. With `-XTypeInType`, you need to import
`Data.Kind` to get `*`, also known as `Type`.
* The kind-checking algorithms in TcHsType have been significantly
rewritten to allow for enhanced kinds.
* The new features are still quite experimental and may be in flux.
* TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.
* TODO: Update user manual.
Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.
Diffstat (limited to 'libraries/base')
-rw-r--r-- | libraries/base/Data/Coerce.hs | 3 | ||||
-rw-r--r-- | libraries/base/Data/Kind.hs | 19 | ||||
-rw-r--r-- | libraries/base/Data/Monoid.hs | 1 | ||||
-rw-r--r-- | libraries/base/Data/Type/Coercion.hs | 10 | ||||
-rw-r--r-- | libraries/base/Data/Type/Equality.hs | 42 | ||||
-rw-r--r-- | libraries/base/Data/Typeable/Internal.hs | 48 | ||||
-rw-r--r-- | libraries/base/GHC/Base.hs | 19 | ||||
-rwxr-xr-x | libraries/base/GHC/Exts.hs | 11 | ||||
-rw-r--r-- | libraries/base/GHC/TypeLits.hs | 2 | ||||
-rw-r--r-- | libraries/base/base.cabal | 1 | ||||
-rw-r--r-- | libraries/base/tests/CatEntail.hs | 2 |
11 files changed, 102 insertions, 56 deletions
diff --git a/libraries/base/Data/Coerce.hs b/libraries/base/Data/Coerce.hs index 23c37967df..bb98393210 100644 --- a/libraries/base/Data/Coerce.hs +++ b/libraries/base/Data/Coerce.hs @@ -26,5 +26,4 @@ module Data.Coerce import GHC.Prim (coerce) import GHC.Types (Coercible) -import GHC.Base () -- for build ordering - +import GHC.Base () -- for build ordering; see Notes in GHC.Base for more info diff --git a/libraries/base/Data/Kind.hs b/libraries/base/Data/Kind.hs new file mode 100644 index 0000000000..348301347c --- /dev/null +++ b/libraries/base/Data/Kind.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE Trustworthy, ExplicitNamespaces #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Kind +-- License : BSD-style (see the LICENSE file in the distribution) +-- +-- Maintainer : libraries@haskell.org +-- Stability : experimental +-- Portability : not portable +-- +-- Basic kinds +-- +-- @since 4.9.0.0 +----------------------------------------------------------------------------- + +module Data.Kind ( Type, Constraint, type (*), type (★) ) where + +import GHC.Types diff --git a/libraries/base/Data/Monoid.hs b/libraries/base/Data/Monoid.hs index f60a15fb58..0a33c27cac 100644 --- a/libraries/base/Data/Monoid.hs +++ b/libraries/base/Data/Monoid.hs @@ -235,4 +235,3 @@ prop_mconcatLast x = where listLastToMaybe [] = Nothing listLastToMaybe lst = Just (last lst) -- -} - diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs index f9f64c1439..c85af5b282 100644 --- a/libraries/base/Data/Type/Coercion.hs +++ b/libraries/base/Data/Type/Coercion.hs @@ -52,19 +52,17 @@ data Coercion a b where -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif -- for 'type-eq' -newtype Sym a b = Sym { unsym :: Coercion b a } - -- | Type-safe cast, using representational equality coerceWith :: Coercion a b -> a -> b coerceWith Coercion x = coerce x -- | Symmetry of representational equality -sym :: forall a b. Coercion a b -> Coercion b a -sym Coercion = unsym (coerce (Sym Coercion :: Sym a a)) +sym :: Coercion a b -> Coercion b a +sym Coercion = Coercion -- | Transitivity of representational equality trans :: Coercion a b -> Coercion b c -> Coercion a c -trans c Coercion = coerce c +trans Coercion Coercion = Coercion -- | Convert propositional (nominal) equality to representational equality repr :: (a Eq.:~: b) -> Coercion a b @@ -98,4 +96,4 @@ instance TestCoercion ((Eq.:~:) a) where testCoercion Eq.Refl Eq.Refl = Just Coercion instance TestCoercion (Coercion a) where - testCoercion c Coercion = Just $ coerce (sym c) + testCoercion Coercion Coercion = Just Coercion diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs index 59d4ea3455..a021fa7b9a 100644 --- a/libraries/base/Data/Type/Equality.hs +++ b/libraries/base/Data/Type/Equality.hs @@ -1,15 +1,17 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} ----------------------------------------------------------------------------- -- | @@ -29,9 +31,9 @@ module Data.Type.Equality ( - -- * The equality type - (:~:)(..), - + -- * The equality types + (:~:)(..), type (~~), + -- * Working with equality sym, trans, castWith, gcastWith, apply, inner, outer, @@ -49,6 +51,16 @@ import GHC.Read import GHC.Base import Data.Type.Bool +-- | Lifted, homogeneous equality. By lifted, we mean that it can be +-- bogus (deferred type error). By homogeneous, the two types @a@ +-- and @b@ must have the same kind. +class a ~~ b => (a :: k) ~ (b :: k) | a -> b, b -> a + -- NB: Not exported, as (~) is magical syntax. That's also why there's + -- no fixity. +instance {-# INCOHERENT #-} a ~~ b => a ~ b + -- incoherent because we want to use this instance eagerly, even when + -- the tyvars are partially unknown. + infix 4 :~: -- | Propositional equality. If @a :~: b@ is inhabited by some terminating diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs index 4379155c57..86ced96b12 100644 --- a/libraries/base/Data/Typeable/Internal.hs +++ b/libraries/base/Data/Typeable/Internal.hs @@ -44,9 +44,10 @@ module Data.Typeable.Internal ( tcBool, tc'True, tc'False, tcOrdering, tc'LT, tc'EQ, tc'GT, tcChar, tcInt, tcWord, tcFloat, tcDouble, tcFun, - tcIO, tcSPEC, tcTyCon, tcModule, - tcCoercible, tcList, tcEq, - tcLiftedKind, tcUnliftedKind, tcOpenKind, tcBOX, tcConstraint, tcAnyK, + tcIO, tcSPEC, tcTyCon, tcModule, tcTrName, + tcCoercible, tcList, tcHEq, + tcConstraint, + tcTYPE, tcLevity, tc'Lifted, tc'Unlifted, funTc, -- ToDo @@ -403,8 +404,8 @@ mkGhcTypesTyCon name = mkTyCon3# "ghc-prim"# "GHC.Types"# name tcBool, tc'True, tc'False, tcOrdering, tc'GT, tc'EQ, tc'LT, tcChar, tcInt, tcWord, tcFloat, tcDouble, tcFun, - tcIO, tcSPEC, tcTyCon, tcModule, - tcCoercible, tcEq, tcList :: TyCon + tcIO, tcSPEC, tcTyCon, tcModule, tcTrName, + tcCoercible, tcHEq, tcList :: TyCon tcBool = mkGhcTypesTyCon "Bool"# -- Bool is promotable tc'True = mkGhcTypesTyCon "'True"# @@ -415,28 +416,28 @@ tc'EQ = mkGhcTypesTyCon "'EQ"# tc'LT = mkGhcTypesTyCon "'LT"# -- None of the rest are promotable (see TysWiredIn) -tcChar = mkGhcTypesTyCon "Char"# -tcInt = mkGhcTypesTyCon "Int"# -tcWord = mkGhcTypesTyCon "Word"# -tcFloat = mkGhcTypesTyCon "Float"# -tcDouble = mkGhcTypesTyCon "Double"# -tcSPEC = mkGhcTypesTyCon "SPEC"# -tcIO = mkGhcTypesTyCon "IO"# -tcTyCon = mkGhcTypesTyCon "TyCon"# -tcModule = mkGhcTypesTyCon "Module"# -tcCoercible = mkGhcTypesTyCon "Coercible"# +tcChar = mkGhcTypesTyCon "Char"# +tcInt = mkGhcTypesTyCon "Int"# +tcWord = mkGhcTypesTyCon "Word"# +tcFloat = mkGhcTypesTyCon "Float"# +tcDouble = mkGhcTypesTyCon "Double"# +tcSPEC = mkGhcTypesTyCon "SPEC"# +tcIO = mkGhcTypesTyCon "IO"# +tcTyCon = mkGhcTypesTyCon "TyCon"# +tcModule = mkGhcTypesTyCon "Module"# +tcTrName = mkGhcTypesTyCon "TrName"# +tcCoercible = mkGhcTypesTyCon "Coercible"# tcFun = mkGhcTypesTyCon "->"# tcList = mkGhcTypesTyCon "[]"# -- Type rep for the list type constructor -tcEq = mkGhcTypesTyCon "~"# -- Type rep for the (~) type constructor - -tcLiftedKind, tcUnliftedKind, tcOpenKind, tcBOX, tcConstraint, tcAnyK :: TyCon -tcLiftedKind = mkGhcTypesTyCon "*"# -tcUnliftedKind = mkGhcTypesTyCon "#"# -tcOpenKind = mkGhcTypesTyCon "#"# -tcBOX = mkGhcTypesTyCon "BOX"# -tcAnyK = mkGhcTypesTyCon "AnyK"# +tcHEq = mkGhcTypesTyCon "~~"# -- Type rep for the (~~) type constructor + +tcConstraint, tcTYPE, tcLevity, tc'Lifted, tc'Unlifted :: TyCon tcConstraint = mkGhcTypesTyCon "Constraint"# +tcTYPE = mkGhcTypesTyCon "TYPE"# +tcLevity = mkGhcTypesTyCon "Levity"# +tc'Lifted = mkGhcTypesTyCon "'Lifted"# +tc'Unlifted = mkGhcTypesTyCon "'Unlifted"# funTc :: TyCon funTc = tcFun -- Legacy @@ -463,4 +464,3 @@ typeSymbolTypeRep p = typeLitTypeRep (show (symbolVal' p)) -- | An internal function, to make representations for type literals. typeLitTypeRep :: String -> TypeRep typeLitTypeRep nm = mkTyConApp (mkTypeLitTyCon nm) [] - diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs index 199664d9db..90eaaf0a1e 100644 --- a/libraries/base/GHC/Base.hs +++ b/libraries/base/GHC/Base.hs @@ -1,4 +1,17 @@ {- + +NOTA BENE: Do NOT use ($) anywhere in this module! The type of ($) is +slightly magical (it can return unlifted types), and it is wired in. +But, it is also *defined* in this module, with a non-magical type. +GHC gets terribly confused (and *hangs*) if you try to use ($) in this +module, because it has different types in different scenarios. + +This is not a problem in general, because the type ($), being wired in, is not +written out to the interface file, so importing files don't get confused. +The problem is only if ($) is used here. So don't! + +--------------------------------------------- + The overall structure of the GHC Prelude is a bit tricky. a) We want to avoid "orphan modules", i.e. ones with instance @@ -1086,13 +1099,13 @@ instance Alternative IO where instance MonadPlus IO returnIO :: a -> IO a -returnIO x = IO $ \ s -> (# s, x #) +returnIO x = IO (\ s -> (# s, x #)) bindIO :: IO a -> (a -> IO b) -> IO b -bindIO (IO m) k = IO $ \ s -> case m s of (# new_s, a #) -> unIO (k a) new_s +bindIO (IO m) k = IO (\ s -> case m s of (# new_s, a #) -> unIO (k a) new_s) thenIO :: IO a -> IO b -> IO b -thenIO (IO m) k = IO $ \ s -> case m s of (# new_s, _ #) -> unIO k new_s +thenIO (IO m) k = IO (\ s -> case m s of (# new_s, _ #) -> unIO k new_s) unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #)) unIO (IO a) = a diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs index ffc27d11eb..032e650c1e 100755 --- a/libraries/base/GHC/Exts.hs +++ b/libraries/base/GHC/Exts.hs @@ -53,6 +53,12 @@ module GHC.Exts -- @since 4.7.0.0 Data.Coerce.coerce, Data.Coerce.Coercible, + -- * Equality + type (~~), + + -- * Levity polymorphism + GHC.Prim.TYPE, Levity(..), + -- * Transform comprehensions Down(..), groupWith, sortWith, the, @@ -72,8 +78,9 @@ module GHC.Exts IsList(..) ) where -import GHC.Prim hiding (coerce, Constraint) -import GHC.Base hiding (coerce) -- implicitly comes from GHC.Prim +import GHC.Prim hiding ( coerce, TYPE ) +import qualified GHC.Prim +import GHC.Base hiding ( coerce ) import GHC.Word import GHC.Int import GHC.Ptr diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs index 0d9f4fe61f..a51ba910e0 100644 --- a/libraries/base/GHC/TypeLits.hs +++ b/libraries/base/GHC/TypeLits.hs @@ -284,5 +284,3 @@ withSNat f x y = magicDict (WrapN f) x y withSSymbol :: (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b withSSymbol f x y = magicDict (WrapS f) x y - - diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal index 684fabb14e..6261c446b8 100644 --- a/libraries/base/base.cabal +++ b/libraries/base/base.cabal @@ -148,6 +148,7 @@ Library Data.IORef Data.Int Data.Ix + Data.Kind Data.List Data.List.NonEmpty Data.Maybe diff --git a/libraries/base/tests/CatEntail.hs b/libraries/base/tests/CatEntail.hs index bc2d8d2f55..c980a2db73 100644 --- a/libraries/base/tests/CatEntail.hs +++ b/libraries/base/tests/CatEntail.hs @@ -2,7 +2,7 @@ {-# LANGUAGE TypeOperators, KindSignatures #-} module CatEntail where import Prelude hiding (id, (.)) -import GHC.Prim (Constraint) +import GHC.Exts (Constraint) import Control.Category -- One dictionary to rule them all. |