Movatterモバイル変換

{-# LANGUAGE Trustworthy #-}{-# LANGUAGE DataKinds #-}{-# LANGUAGE KindSignatures #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeOperators #-}{-# LANGUAGE FlexibleInstances #-}{-# LANGUAGE FlexibleContexts #-}{-# LANGUAGE ScopedTypeVariables #-}{-# LANGUAGE ConstraintKinds #-}{-# LANGUAGE ExistentialQuantification #-}{-# LANGUAGE RankNTypes #-}{-# LANGUAGE NoImplicitPrelude #-}{-# LANGUAGE MagicHash #-}{-# LANGUAGE PolyKinds #-}{-| This module is an internal GHC module.  It declares the constants usedin the implementation of type-level natural numbers.  The programmer interfacefor working with type-level naturals should be defined in a separate library.@since 4.6.0.0-}moduleGHC.TypeLits(-- * KindsNat,Symbol-- Both declared in GHC.Types in package ghc-prim-- * Linking type and value level,N.KnownNat,natVal,natVal',KnownSymbol,symbolVal,symbolVal',N.SomeNat(..),SomeSymbol(..),someNatVal,someSymbolVal,N.sameNat,sameSymbol-- * Functions on type literals,type(N.<=),type(N.<=?),type(N.+),type(N.*),type(N.^),type(N.-),typeN.Div,typeN.Mod,typeN.Log2,AppendSymbol,N.CmpNat,CmpSymbol-- * User-defined type errors,TypeError,ErrorMessage(..))whereimportGHC.Base(Eq(..),Ord(..),Ordering(..),otherwise)importGHC.Types(Nat,Symbol)importGHC.Num(Integer,fromInteger)importGHC.Base(String)importGHC.Show(Show(..))importGHC.Read(Read(..))importGHC.Real(toInteger)importGHC.Prim(magicDict,Proxy#)importData.Maybe(Maybe(..))importData.Proxy(Proxy(..))importData.Type.Equality((:~:)(Refl))importUnsafe.Coerce(unsafeCoerce)importGHC.TypeNats(KnownNat)importqualifiedGHC.TypeNatsasN---------------------------------------------------------------------------------- | This class gives the string associated with a type-level symbol.-- There are instances of the class for every concrete literal: "hello", etc.---- @since 4.7.0.0classKnownSymbol(n::Symbol)wheresymbolSing::SSymboln-- | @since 4.7.0.0natVal::forallnproxy.KnownNatn=>proxyn->IntegernatValp=toInteger(N.natValp)-- | @since 4.7.0.0symbolVal::forallnproxy.KnownSymboln=>proxyn->StringsymbolVal_=casesymbolSing::SSymbolnofSSymbolx->x-- | @since 4.8.0.0natVal'::foralln.KnownNatn=>Proxy#n->IntegernatVal'p=toInteger(N.natVal'p)-- | @since 4.8.0.0symbolVal'::foralln.KnownSymboln=>Proxy#n->StringsymbolVal'_=casesymbolSing::SSymbolnofSSymbolx->x-- | This type represents unknown type-level symbols.dataSomeSymbol=foralln.KnownSymboln=>SomeSymbol(Proxyn)-- ^ @since 4.7.0.0-- | Convert an integer into an unknown type-level natural.---- @since 4.7.0.0someNatVal::Integer->MaybeN.SomeNatsomeNatValn|n>=0=Just(N.someNatVal(fromIntegern))|otherwise=Nothing-- | Convert a string into an unknown type-level symbol.---- @since 4.7.0.0someSymbolVal::String->SomeSymbolsomeSymbolValn=withSSymbolSomeSymbol(SSymboln)Proxy-- | @since 4.7.0.0instanceEqSomeSymbolwhereSomeSymbolx==SomeSymboly=symbolValx==symbolValy-- | @since 4.7.0.0instanceOrdSomeSymbolwherecompare(SomeSymbolx)(SomeSymboly)=compare(symbolValx)(symbolValy)-- | @since 4.7.0.0instanceShowSomeSymbolwhereshowsPrecp(SomeSymbolx)=showsPrecp(symbolValx)-- | @since 4.7.0.0instanceReadSomeSymbolwherereadsPrecpxs=[(someSymbolVala,ys)|(a,ys)<-readsPrecpxs]---------------------------------------------------------------------------------- | Comparison of type-level symbols, as a function.---- @since 4.7.0.0typefamilyCmpSymbol(m::Symbol)(n::Symbol)::Ordering-- | Concatenation of type-level symbols.---- @since 4.10.0.0typefamilyAppendSymbol(m::Symbol)(n::Symbol)::Symbol-- | A description of a custom type error.data{-kind-}ErrorMessage=TextSymbol-- ^ Show the text as is.|forallt.ShowTypet-- ^ Pretty print the type.-- @ShowType :: k -> ErrorMessage@|ErrorMessage:<>:ErrorMessage-- ^ Put two pieces of error message next-- to each other.|ErrorMessage:$$:ErrorMessage-- ^ Stack two pieces of error message on top-- of each other.infixl5:$$:infixl6:<>:-- | The type-level equivalent of 'error'.---- The polymorphic kind of this type allows it to be used in several settings.-- For instance, it can be used as a constraint, e.g. to provide a better error-- message for a non-existent instance,---- @-- -- in a context-- instance TypeError (Text "Cannot 'Show' functions." :$$:--                     Text "Perhaps there is a missing argument?")--       => Show (a -> b) where--     showsPrec = error "unreachable"-- @---- It can also be placed on the right-hand side of a type-level function-- to provide an error for an invalid case,---- @-- type family ByteSize x where--    ByteSize Word16   = 2--    ByteSize Word8    = 1--    ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:--                                   Text " is not exportable.")-- @---- @since 4.9.0.0typefamilyTypeError(a::ErrorMessage)::bwhere---------------------------------------------------------------------------------- | We either get evidence that this function was instantiated with the-- same type-level symbols, or 'Nothing'.---- @since 4.7.0.0sameSymbol::(KnownSymbola,KnownSymbolb)=>Proxya->Proxyb->Maybe(a:~:b)sameSymbolxy|symbolValx==symbolValy=Just(unsafeCoerceRefl)|otherwise=Nothing---------------------------------------------------------------------------------- PRIVATE:newtypeSSymbol(s::Symbol)=SSymbolStringdataWrapSab=WrapS(KnownSymbola=>Proxya->b)-- See Note [magicDictId magic] in "basicType/MkId.hs"withSSymbol::(KnownSymbola=>Proxya->b)->SSymbola->Proxya->bwithSSymbolfxy=magicDict(WrapSf)xy