diff options
Diffstat (limited to 'compiler/GHC/Builtin/Types')
| -rw-r--r-- | compiler/GHC/Builtin/Types/Literals.hs | 993 | ||||
| -rw-r--r-- | compiler/GHC/Builtin/Types/Prim.hs | 1110 |
2 files changed, 2103 insertions, 0 deletions
diff --git a/compiler/GHC/Builtin/Types/Literals.hs b/compiler/GHC/Builtin/Types/Literals.hs new file mode 100644 index 0000000000..d5c1d209c6 --- /dev/null +++ b/compiler/GHC/Builtin/Types/Literals.hs @@ -0,0 +1,993 @@ +{-# LANGUAGE LambdaCase #-} + +module GHC.Builtin.Types.Literals + ( typeNatTyCons + , typeNatCoAxiomRules + , BuiltInSynFamily(..) + + -- If you define a new built-in type family, make sure to export its TyCon + -- from here as well. + -- See Note [Adding built-in type families] + , typeNatAddTyCon + , typeNatMulTyCon + , typeNatExpTyCon + , typeNatLeqTyCon + , typeNatSubTyCon + , typeNatDivTyCon + , typeNatModTyCon + , typeNatLogTyCon + , typeNatCmpTyCon + , typeSymbolCmpTyCon + , typeSymbolAppendTyCon + ) where + +import GhcPrelude + +import GHC.Core.Type +import Pair +import GHC.Tc.Utils.TcType ( TcType, tcEqType ) +import GHC.Core.TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon + , Injectivity(..) ) +import GHC.Core.Coercion ( Role(..) ) +import GHC.Tc.Types.Constraint ( Xi ) +import GHC.Core.Coercion.Axiom ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn ) +import GHC.Types.Name ( Name, BuiltInSyntax(..) ) +import GHC.Builtin.Types +import GHC.Builtin.Types.Prim ( mkTemplateAnonTyConBinders ) +import GHC.Builtin.Names + ( gHC_TYPELITS + , gHC_TYPENATS + , typeNatAddTyFamNameKey + , typeNatMulTyFamNameKey + , typeNatExpTyFamNameKey + , typeNatLeqTyFamNameKey + , typeNatSubTyFamNameKey + , typeNatDivTyFamNameKey + , typeNatModTyFamNameKey + , typeNatLogTyFamNameKey + , typeNatCmpTyFamNameKey + , typeSymbolCmpTyFamNameKey + , typeSymbolAppendFamNameKey + ) +import FastString ( FastString + , fsLit, nilFS, nullFS, unpackFS, mkFastString, appendFS + ) +import qualified Data.Map as Map +import Data.Maybe ( isJust ) +import Control.Monad ( guard ) +import Data.List ( isPrefixOf, isSuffixOf ) + +{- +Note [Type-level literals] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are currently two forms of type-level literals: natural numbers, and +symbols (even though this module is named GHC.Builtin.Types.Literals, it covers both). + +Type-level literals are supported by CoAxiomRules (conditional axioms), which +power the built-in type families (see Note [Adding built-in type families]). +Currently, all built-in type families are for the express purpose of supporting +type-level literals. + +See also the Wiki page: + + https://gitlab.haskell.org/ghc/ghc/wikis/type-nats + +Note [Adding built-in type families] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are a few steps to adding a built-in type family: + +* Adding a unique for the type family TyCon + + These go in GHC.Builtin.Names. It will likely be of the form + @myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that + has not been chosen before in GHC.Builtin.Names. There are several examples already + in GHC.Builtin.Names—see, for instance, typeNatAddTyFamNameKey. + +* Adding the type family TyCon itself + + This goes in GHC.Builtin.Types.Literals. There are plenty of examples of how to define + these—see, for instance, typeNatAddTyCon. + + Once your TyCon has been defined, be sure to: + + - Export it from GHC.Builtin.Types.Literals. (Not doing so caused #14632.) + - Include it in the typeNatTyCons list, defined in GHC.Builtin.Types.Literals. + +* Exposing associated type family axioms + + When defining the type family TyCon, you will need to define an axiom for + the type family in general (see, for instance, axAddDef), and perhaps other + auxiliary axioms for special cases of the type family (see, for instance, + axAdd0L and axAdd0R). + + After you have defined all of these axioms, be sure to include them in the + typeNatCoAxiomRules list, defined in GHC.Builtin.Types.Literals. + (Not doing so caused #14934.) + +* Define the type family somewhere + + Finally, you will need to define the type family somewhere, likely in @base@. + Currently, all of the built-in type families are defined in GHC.TypeLits or + GHC.TypeNats, so those are likely candidates. + + Since the behavior of your built-in type family is specified in GHC.Builtin.Types.Literals, + you should give an open type family definition with no instances, like so: + + type family MyTypeFam (m :: Nat) (n :: Nat) :: Nat + + Changing the argument and result kinds as appropriate. + +* Update the relevant test cases + + The GHC test suite will likely need to be updated after you add your built-in + type family. For instance: + + - The T9181 test prints the :browse contents of GHC.TypeLits, so if you added + a test there, the expected output of T9181 will need to change. + - The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit + tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have + runtime unit tests. Consider adding further unit tests to those if your + built-in type family deals with Nats or Symbols, respectively. +-} + +{------------------------------------------------------------------------------- +Built-in type constructors for functions on type-level nats +-} + +-- The list of built-in type family TyCons that GHC uses. +-- If you define a built-in type family, make sure to add it to this list. +-- See Note [Adding built-in type families] +typeNatTyCons :: [TyCon] +typeNatTyCons = + [ typeNatAddTyCon + , typeNatMulTyCon + , typeNatExpTyCon + , typeNatLeqTyCon + , typeNatSubTyCon + , typeNatDivTyCon + , typeNatModTyCon + , typeNatLogTyCon + , typeNatCmpTyCon + , typeSymbolCmpTyCon + , typeSymbolAppendTyCon + ] + +typeNatAddTyCon :: TyCon +typeNatAddTyCon = mkTypeNatFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamAdd + , sfInteractTop = interactTopAdd + , sfInteractInert = interactInertAdd + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "+") + typeNatAddTyFamNameKey typeNatAddTyCon + +typeNatSubTyCon :: TyCon +typeNatSubTyCon = mkTypeNatFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamSub + , sfInteractTop = interactTopSub + , sfInteractInert = interactInertSub + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "-") + typeNatSubTyFamNameKey typeNatSubTyCon + +typeNatMulTyCon :: TyCon +typeNatMulTyCon = mkTypeNatFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamMul + , sfInteractTop = interactTopMul + , sfInteractInert = interactInertMul + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "*") + typeNatMulTyFamNameKey typeNatMulTyCon + +typeNatDivTyCon :: TyCon +typeNatDivTyCon = mkTypeNatFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamDiv + , sfInteractTop = interactTopDiv + , sfInteractInert = interactInertDiv + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "Div") + typeNatDivTyFamNameKey typeNatDivTyCon + +typeNatModTyCon :: TyCon +typeNatModTyCon = mkTypeNatFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamMod + , sfInteractTop = interactTopMod + , sfInteractInert = interactInertMod + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "Mod") + typeNatModTyFamNameKey typeNatModTyCon + + + + + +typeNatExpTyCon :: TyCon +typeNatExpTyCon = mkTypeNatFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamExp + , sfInteractTop = interactTopExp + , sfInteractInert = interactInertExp + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "^") + typeNatExpTyFamNameKey typeNatExpTyCon + +typeNatLogTyCon :: TyCon +typeNatLogTyCon = mkTypeNatFunTyCon1 name + BuiltInSynFamily + { sfMatchFam = matchFamLog + , sfInteractTop = interactTopLog + , sfInteractInert = interactInertLog + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "Log2") + typeNatLogTyFamNameKey typeNatLogTyCon + + + +typeNatLeqTyCon :: TyCon +typeNatLeqTyCon = + mkFamilyTyCon name + (mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ]) + boolTy + Nothing + (BuiltInSynFamTyCon ops) + Nothing + NotInjective + + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "<=?") + typeNatLeqTyFamNameKey typeNatLeqTyCon + ops = BuiltInSynFamily + { sfMatchFam = matchFamLeq + , sfInteractTop = interactTopLeq + , sfInteractInert = interactInertLeq + } + +typeNatCmpTyCon :: TyCon +typeNatCmpTyCon = + mkFamilyTyCon name + (mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ]) + orderingKind + Nothing + (BuiltInSynFamTyCon ops) + Nothing + NotInjective + + where + name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "CmpNat") + typeNatCmpTyFamNameKey typeNatCmpTyCon + ops = BuiltInSynFamily + { sfMatchFam = matchFamCmpNat + , sfInteractTop = interactTopCmpNat + , sfInteractInert = \_ _ _ _ -> [] + } + +typeSymbolCmpTyCon :: TyCon +typeSymbolCmpTyCon = + mkFamilyTyCon name + (mkTemplateAnonTyConBinders [ typeSymbolKind, typeSymbolKind ]) + orderingKind + Nothing + (BuiltInSynFamTyCon ops) + Nothing + NotInjective + + where + name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol") + typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon + ops = BuiltInSynFamily + { sfMatchFam = matchFamCmpSymbol + , sfInteractTop = interactTopCmpSymbol + , sfInteractInert = \_ _ _ _ -> [] + } + +typeSymbolAppendTyCon :: TyCon +typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name + BuiltInSynFamily + { sfMatchFam = matchFamAppendSymbol + , sfInteractTop = interactTopAppendSymbol + , sfInteractInert = interactInertAppendSymbol + } + where + name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "AppendSymbol") + typeSymbolAppendFamNameKey typeSymbolAppendTyCon + + + +-- Make a unary built-in constructor of kind: Nat -> Nat +mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon +mkTypeNatFunTyCon1 op tcb = + mkFamilyTyCon op + (mkTemplateAnonTyConBinders [ typeNatKind ]) + typeNatKind + Nothing + (BuiltInSynFamTyCon tcb) + Nothing + NotInjective + + +-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat +mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon +mkTypeNatFunTyCon2 op tcb = + mkFamilyTyCon op + (mkTemplateAnonTyConBinders [ typeNatKind, typeNatKind ]) + typeNatKind + Nothing + (BuiltInSynFamTyCon tcb) + Nothing + NotInjective + +-- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol +mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon +mkTypeSymbolFunTyCon2 op tcb = + mkFamilyTyCon op + (mkTemplateAnonTyConBinders [ typeSymbolKind, typeSymbolKind ]) + typeSymbolKind + Nothing + (BuiltInSynFamTyCon tcb) + Nothing + NotInjective + + +{------------------------------------------------------------------------------- +Built-in rules axioms +-------------------------------------------------------------------------------} + +-- If you add additional rules, please remember to add them to +-- `typeNatCoAxiomRules` also. +-- See Note [Adding built-in type families] +axAddDef + , axMulDef + , axExpDef + , axLeqDef + , axCmpNatDef + , axCmpSymbolDef + , axAppendSymbolDef + , axAdd0L + , axAdd0R + , axMul0L + , axMul0R + , axMul1L + , axMul1R + , axExp1L + , axExp0R + , axExp1R + , axLeqRefl + , axCmpNatRefl + , axCmpSymbolRefl + , axLeq0L + , axSubDef + , axSub0R + , axAppendSymbol0R + , axAppendSymbol0L + , axDivDef + , axDiv1 + , axModDef + , axMod1 + , axLogDef + :: CoAxiomRule + +axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $ + \x y -> Just $ num (x + y) + +axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $ + \x y -> Just $ num (x * y) + +axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $ + \x y -> Just $ num (x ^ y) + +axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $ + \x y -> Just $ bool (x <= y) + +axCmpNatDef = mkBinAxiom "CmpNatDef" typeNatCmpTyCon + $ \x y -> Just $ ordering (compare x y) + +axCmpSymbolDef = + CoAxiomRule + { coaxrName = fsLit "CmpSymbolDef" + , coaxrAsmpRoles = [Nominal, Nominal] + , coaxrRole = Nominal + , coaxrProves = \cs -> + do [Pair s1 s2, Pair t1 t2] <- return cs + s2' <- isStrLitTy s2 + t2' <- isStrLitTy t2 + return (mkTyConApp typeSymbolCmpTyCon [s1,t1] === + ordering (compare s2' t2')) } + +axAppendSymbolDef = CoAxiomRule + { coaxrName = fsLit "AppendSymbolDef" + , coaxrAsmpRoles = [Nominal, Nominal] + , coaxrRole = Nominal + , coaxrProves = \cs -> + do [Pair s1 s2, Pair t1 t2] <- return cs + s2' <- isStrLitTy s2 + t2' <- isStrLitTy t2 + let z = mkStrLitTy (appendFS s2' t2') + return (mkTyConApp typeSymbolAppendTyCon [s1, t1] === z) + } + +axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $ + \x y -> fmap num (minus x y) + +axDivDef = mkBinAxiom "DivDef" typeNatDivTyCon $ + \x y -> do guard (y /= 0) + return (num (div x y)) + +axModDef = mkBinAxiom "ModDef" typeNatModTyCon $ + \x y -> do guard (y /= 0) + return (num (mod x y)) + +axLogDef = mkUnAxiom "LogDef" typeNatLogTyCon $ + \x -> do (a,_) <- genLog x 2 + return (num a) + +axAdd0L = mkAxiom1 "Add0L" $ \(Pair s t) -> (num 0 .+. s) === t +axAdd0R = mkAxiom1 "Add0R" $ \(Pair s t) -> (s .+. num 0) === t +axSub0R = mkAxiom1 "Sub0R" $ \(Pair s t) -> (s .-. num 0) === t +axMul0L = mkAxiom1 "Mul0L" $ \(Pair s _) -> (num 0 .*. s) === num 0 +axMul0R = mkAxiom1 "Mul0R" $ \(Pair s _) -> (s .*. num 0) === num 0 +axMul1L = mkAxiom1 "Mul1L" $ \(Pair s t) -> (num 1 .*. s) === t +axMul1R = mkAxiom1 "Mul1R" $ \(Pair s t) -> (s .*. num 1) === t +axDiv1 = mkAxiom1 "Div1" $ \(Pair s t) -> (tDiv s (num 1) === t) +axMod1 = mkAxiom1 "Mod1" $ \(Pair s _) -> (tMod s (num 1) === num 0) + -- XXX: Shouldn't we check that _ is 0? +axExp1L = mkAxiom1 "Exp1L" $ \(Pair s _) -> (num 1 .^. s) === num 1 +axExp0R = mkAxiom1 "Exp0R" $ \(Pair s _) -> (s .^. num 0) === num 1 +axExp1R = mkAxiom1 "Exp1R" $ \(Pair s t) -> (s .^. num 1) === t +axLeqRefl = mkAxiom1 "LeqRefl" $ \(Pair s _) -> (s <== s) === bool True +axCmpNatRefl = mkAxiom1 "CmpNatRefl" + $ \(Pair s _) -> (cmpNat s s) === ordering EQ +axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl" + $ \(Pair s _) -> (cmpSymbol s s) === ordering EQ +axLeq0L = mkAxiom1 "Leq0L" $ \(Pair s _) -> (num 0 <== s) === bool True +axAppendSymbol0R = mkAxiom1 "Concat0R" + $ \(Pair s t) -> (mkStrLitTy nilFS `appendSymbol` s) === t +axAppendSymbol0L = mkAxiom1 "Concat0L" + $ \(Pair s t) -> (s `appendSymbol` mkStrLitTy nilFS) === t + +-- The list of built-in type family axioms that GHC uses. +-- If you define new axioms, make sure to include them in this list. +-- See Note [Adding built-in type families] +typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule +typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x)) + [ axAddDef + , axMulDef + , axExpDef + , axLeqDef + , axCmpNatDef + , axCmpSymbolDef + , axAppendSymbolDef + , axAdd0L + , axAdd0R + , axMul0L + , axMul0R + , axMul1L + , axMul1R + , axExp1L + , axExp0R + , axExp1R + , axLeqRefl + , axCmpNatRefl + , axCmpSymbolRefl + , axLeq0L + , axSubDef + , axSub0R + , axAppendSymbol0R + , axAppendSymbol0L + , axDivDef + , axDiv1 + , axModDef + , axMod1 + , axLogDef + ] + + + +{------------------------------------------------------------------------------- +Various utilities for making axioms and types +-------------------------------------------------------------------------------} + +(.+.) :: Type -> Type -> Type +s .+. t = mkTyConApp typeNatAddTyCon [s,t] + +(.-.) :: Type -> Type -> Type +s .-. t = mkTyConApp typeNatSubTyCon [s,t] + +(.*.) :: Type -> Type -> Type +s .*. t = mkTyConApp typeNatMulTyCon [s,t] + +tDiv :: Type -> Type -> Type +tDiv s t = mkTyConApp typeNatDivTyCon [s,t] + +tMod :: Type -> Type -> Type +tMod s t = mkTyConApp typeNatModTyCon [s,t] + +(.^.) :: Type -> Type -> Type +s .^. t = mkTyConApp typeNatExpTyCon [s,t] + +(<==) :: Type -> Type -> Type +s <== t = mkTyConApp typeNatLeqTyCon [s,t] + +cmpNat :: Type -> Type -> Type +cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t] + +cmpSymbol :: Type -> Type -> Type +cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t] + +appendSymbol :: Type -> Type -> Type +appendSymbol s t = mkTyConApp typeSymbolAppendTyCon [s, t] + +(===) :: Type -> Type -> Pair Type +x === y = Pair x y + +num :: Integer -> Type +num = mkNumLitTy + +bool :: Bool -> Type +bool b = if b then mkTyConApp promotedTrueDataCon [] + else mkTyConApp promotedFalseDataCon [] + +isBoolLitTy :: Type -> Maybe Bool +isBoolLitTy tc = + do (tc,[]) <- splitTyConApp_maybe tc + case () of + _ | tc == promotedFalseDataCon -> return False + | tc == promotedTrueDataCon -> return True + | otherwise -> Nothing + +orderingKind :: Kind +orderingKind = mkTyConApp orderingTyCon [] + +ordering :: Ordering -> Type +ordering o = + case o of + LT -> mkTyConApp promotedLTDataCon [] + EQ -> mkTyConApp promotedEQDataCon [] + GT -> mkTyConApp promotedGTDataCon [] + +isOrderingLitTy :: Type -> Maybe Ordering +isOrderingLitTy tc = + do (tc1,[]) <- splitTyConApp_maybe tc + case () of + _ | tc1 == promotedLTDataCon -> return LT + | tc1 == promotedEQDataCon -> return EQ + | tc1 == promotedGTDataCon -> return GT + | otherwise -> Nothing + +known :: (Integer -> Bool) -> TcType -> Bool +known p x = case isNumLitTy x of + Just a -> p a + Nothing -> False + + +mkUnAxiom :: String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule +mkUnAxiom str tc f = + CoAxiomRule + { coaxrName = fsLit str + , coaxrAsmpRoles = [Nominal] + , coaxrRole = Nominal + , coaxrProves = \cs -> + do [Pair s1 s2] <- return cs + s2' <- isNumLitTy s2 + z <- f s2' + return (mkTyConApp tc [s1] === z) + } + + + +-- For the definitional axioms +mkBinAxiom :: String -> TyCon -> + (Integer -> Integer -> Maybe Type) -> CoAxiomRule +mkBinAxiom str tc f = + CoAxiomRule + { coaxrName = fsLit str + , coaxrAsmpRoles = [Nominal, Nominal] + , coaxrRole = Nominal + , coaxrProves = \cs -> + do [Pair s1 s2, Pair t1 t2] <- return cs + s2' <- isNumLitTy s2 + t2' <- isNumLitTy t2 + z <- f s2' t2' + return (mkTyConApp tc [s1,t1] === z) + } + + + +mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule +mkAxiom1 str f = + CoAxiomRule + { coaxrName = fsLit str + , coaxrAsmpRoles = [Nominal] + , coaxrRole = Nominal + , coaxrProves = \case [eqn] -> Just (f eqn) + _ -> Nothing + } + + +{------------------------------------------------------------------------------- +Evaluation +-------------------------------------------------------------------------------} + +matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamAdd [s,t] + | Just 0 <- mbX = Just (axAdd0L, [t], t) + | Just 0 <- mbY = Just (axAdd0R, [s], s) + | Just x <- mbX, Just y <- mbY = + Just (axAddDef, [s,t], num (x + y)) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamAdd _ = Nothing + +matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamSub [s,t] + | Just 0 <- mbY = Just (axSub0R, [s], s) + | Just x <- mbX, Just y <- mbY, Just z <- minus x y = + Just (axSubDef, [s,t], num z) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamSub _ = Nothing + +matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamMul [s,t] + | Just 0 <- mbX = Just (axMul0L, [t], num 0) + | Just 0 <- mbY = Just (axMul0R, [s], num 0) + | Just 1 <- mbX = Just (axMul1L, [t], t) + | Just 1 <- mbY = Just (axMul1R, [s], s) + | Just x <- mbX, Just y <- mbY = + Just (axMulDef, [s,t], num (x * y)) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamMul _ = Nothing + +matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamDiv [s,t] + | Just 1 <- mbY = Just (axDiv1, [s], s) + | Just x <- mbX, Just y <- mbY, y /= 0 = Just (axDivDef, [s,t], num (div x y)) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamDiv _ = Nothing + +matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamMod [s,t] + | Just 1 <- mbY = Just (axMod1, [s], num 0) + | Just x <- mbX, Just y <- mbY, y /= 0 = Just (axModDef, [s,t], num (mod x y)) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamMod _ = Nothing + + + +matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamExp [s,t] + | Just 0 <- mbY = Just (axExp0R, [s], num 1) + | Just 1 <- mbX = Just (axExp1L, [t], num 1) + | Just 1 <- mbY = Just (axExp1R, [s], s) + | Just x <- mbX, Just y <- mbY = + Just (axExpDef, [s,t], num (x ^ y)) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamExp _ = Nothing + +matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamLog [s] + | Just x <- mbX, Just (n,_) <- genLog x 2 = Just (axLogDef, [s], num n) + where mbX = isNumLitTy s +matchFamLog _ = Nothing + + +matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamLeq [s,t] + | Just 0 <- mbX = Just (axLeq0L, [t], bool True) + | Just x <- mbX, Just y <- mbY = + Just (axLeqDef, [s,t], bool (x <= y)) + | tcEqType s t = Just (axLeqRefl, [s], bool True) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamLeq _ = Nothing + +matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamCmpNat [s,t] + | Just x <- mbX, Just y <- mbY = + Just (axCmpNatDef, [s,t], ordering (compare x y)) + | tcEqType s t = Just (axCmpNatRefl, [s], ordering EQ) + where mbX = isNumLitTy s + mbY = isNumLitTy t +matchFamCmpNat _ = Nothing + +matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamCmpSymbol [s,t] + | Just x <- mbX, Just y <- mbY = + Just (axCmpSymbolDef, [s,t], ordering (compare x y)) + | tcEqType s t = Just (axCmpSymbolRefl, [s], ordering EQ) + where mbX = isStrLitTy s + mbY = isStrLitTy t +matchFamCmpSymbol _ = Nothing + +matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type) +matchFamAppendSymbol [s,t] + | Just x <- mbX, nullFS x = Just (axAppendSymbol0R, [t], t) + | Just y <- mbY, nullFS y = Just (axAppendSymbol0L, [s], s) + | Just x <- mbX, Just y <- mbY = + Just (axAppendSymbolDef, [s,t], mkStrLitTy (appendFS x y)) + where + mbX = isStrLitTy s + mbY = isStrLitTy t +matchFamAppendSymbol _ = Nothing + +{------------------------------------------------------------------------------- +Interact with axioms +-------------------------------------------------------------------------------} + +interactTopAdd :: [Xi] -> Xi -> [Pair Type] +interactTopAdd [s,t] r + | Just 0 <- mbZ = [ s === num 0, t === num 0 ] -- (s + t ~ 0) => (s ~ 0, t ~ 0) + | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y] -- (5 + t ~ 8) => (t ~ 3) + | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x] -- (s + 5 ~ 8) => (s ~ 3) + where + mbX = isNumLitTy s + mbY = isNumLitTy t + mbZ = isNumLitTy r +interactTopAdd _ _ = [] + +{- +Note [Weakened interaction rule for subtraction] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A simpler interaction here might be: + + `s - t ~ r` --> `t + r ~ s` + +This would enable us to reuse all the code for addition. +Unfortunately, this works a little too well at the moment. +Consider the following example: + + 0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0) + +This (correctly) spots that the constraint cannot be solved. + +However, this may be a problem if the constraint did not +need to be solved in the first place! Consider the following example: + +f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5 +f = id + +Currently, GHC is strict while evaluating functions, so this does not +work, because even though the `If` should evaluate to `5 - 0`, we +also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`, +which fails. + +So, for the time being, we only add an improvement when the RHS is a constant, +which happens to work OK for the moment, although clearly we need to do +something more general. +-} +interactTopSub :: [Xi] -> Xi -> [Pair Type] +interactTopSub [s,t] r + | Just z <- mbZ = [ s === (num z .+. t) ] -- (s - t ~ 5) => (5 + t ~ s) + where + mbZ = isNumLitTy r +interactTopSub _ _ = [] + + + + + +interactTopMul :: [Xi] -> Xi -> [Pair Type] +interactTopMul [s,t] r + | Just 1 <- mbZ = [ s === num 1, t === num 1 ] -- (s * t ~ 1) => (s ~ 1, t ~ 1) + | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y] -- (3 * t ~ 15) => (t ~ 5) + | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x] -- (s * 3 ~ 15) => (s ~ 5) + where + mbX = isNumLitTy s + mbY = isNumLitTy t + mbZ = isNumLitTy r +interactTopMul _ _ = [] + +interactTopDiv :: [Xi] -> Xi -> [Pair Type] +interactTopDiv _ _ = [] -- I can't think of anything... + +interactTopMod :: [Xi] -> Xi -> [Pair Type] +interactTopMod _ _ = [] -- I can't think of anything... + +interactTopExp :: [Xi] -> Xi -> [Pair Type] +interactTopExp [s,t] r + | Just 0 <- mbZ = [ s === num 0 ] -- (s ^ t ~ 0) => (s ~ 0) + | Just x <- mbX, Just z <- mbZ, Just y <- logExact z x = [t === num y] -- (2 ^ t ~ 8) => (t ~ 3) + | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x] -- (s ^ 2 ~ 9) => (s ~ 3) + where + mbX = isNumLitTy s + mbY = isNumLitTy t + mbZ = isNumLitTy r +interactTopExp _ _ = [] + +interactTopLog :: [Xi] -> Xi -> [Pair Type] +interactTopLog _ _ = [] -- I can't think of anything... + + + +interactTopLeq :: [Xi] -> Xi -> [Pair Type] +interactTopLeq [s,t] r + | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ] -- (s <= 0) => (s ~ 0) + where + mbY = isNumLitTy t + mbZ = isBoolLitTy r +interactTopLeq _ _ = [] + +interactTopCmpNat :: [Xi] -> Xi -> [Pair Type] +interactTopCmpNat [s,t] r + | Just EQ <- isOrderingLitTy r = [ s === t ] +interactTopCmpNat _ _ = [] + +interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type] +interactTopCmpSymbol [s,t] r + | Just EQ <- isOrderingLitTy r = [ s === t ] +interactTopCmpSymbol _ _ = [] + +interactTopAppendSymbol :: [Xi] -> Xi -> [Pair Type] +interactTopAppendSymbol [s,t] r + -- (AppendSymbol a b ~ "") => (a ~ "", b ~ "") + | Just z <- mbZ, nullFS z = + [s === mkStrLitTy nilFS, t === mkStrLitTy nilFS ] + + -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar") + | Just x <- fmap unpackFS mbX, Just z <- fmap unpackFS mbZ, x `isPrefixOf` z = + [ t === mkStrLitTy (mkFastString $ drop (length x) z) ] + + -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo") + | Just y <- fmap unpackFS mbY, Just z <- fmap unpackFS mbZ, y `isSuffixOf` z = + [ t === mkStrLitTy (mkFastString $ take (length z - length y) z) ] + + where + mbX = isStrLitTy s + mbY = isStrLitTy t + mbZ = isStrLitTy r + +interactTopAppendSymbol _ _ = [] + +{------------------------------------------------------------------------------- +Interaction with inerts +-------------------------------------------------------------------------------} + +interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertAdd [x1,y1] z1 [x2,y2] z2 + | sameZ && tcEqType x1 x2 = [ y1 === y2 ] + | sameZ && tcEqType y1 y2 = [ x1 === x2 ] + where sameZ = tcEqType z1 z2 +interactInertAdd _ _ _ _ = [] + +interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertSub [x1,y1] z1 [x2,y2] z2 + | sameZ && tcEqType x1 x2 = [ y1 === y2 ] + | sameZ && tcEqType y1 y2 = [ x1 === x2 ] + where sameZ = tcEqType z1 z2 +interactInertSub _ _ _ _ = [] + +interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertMul [x1,y1] z1 [x2,y2] z2 + | sameZ && known (/= 0) x1 && tcEqType x1 x2 = [ y1 === y2 ] + | sameZ && known (/= 0) y1 && tcEqType y1 y2 = [ x1 === x2 ] + where sameZ = tcEqType z1 z2 + +interactInertMul _ _ _ _ = [] + +interactInertDiv :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertDiv _ _ _ _ = [] + +interactInertMod :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertMod _ _ _ _ = [] + +interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertExp [x1,y1] z1 [x2,y2] z2 + | sameZ && known (> 1) x1 && tcEqType x1 x2 = [ y1 === y2 ] + | sameZ && known (> 0) y1 && tcEqType y1 y2 = [ x1 === x2 ] + where sameZ = tcEqType z1 z2 + +interactInertExp _ _ _ _ = [] + +interactInertLog :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertLog _ _ _ _ = [] + + +interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertLeq [x1,y1] z1 [x2,y2] z2 + | bothTrue && tcEqType x1 y2 && tcEqType y1 x2 = [ x1 === y1 ] + | bothTrue && tcEqType y1 x2 = [ (x1 <== y2) === bool True ] + | bothTrue && tcEqType y2 x1 = [ (x2 <== y1) === bool True ] + where bothTrue = isJust $ do True <- isBoolLitTy z1 + True <- isBoolLitTy z2 + return () + +interactInertLeq _ _ _ _ = [] + + +interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertAppendSymbol [x1,y1] z1 [x2,y2] z2 + | sameZ && tcEqType x1 x2 = [ y1 === y2 ] + | sameZ && tcEqType y1 y2 = [ x1 === x2 ] + where sameZ = tcEqType z1 z2 +interactInertAppendSymbol _ _ _ _ = [] + + + +{- ----------------------------------------------------------------------------- +These inverse functions are used for simplifying propositions using +concrete natural numbers. +----------------------------------------------------------------------------- -} + +-- | Subtract two natural numbers. +minus :: Integer -> Integer -> Maybe Integer +minus x y = if x >= y then Just (x - y) else Nothing + +-- | Compute the exact logarithm of a natural number. +-- The logarithm base is the second argument. +logExact :: Integer -> Integer -> Maybe Integer +logExact x y = do (z,True) <- genLog x y + return z + + +-- | Divide two natural numbers. +divide :: Integer -> Integer -> Maybe Integer +divide _ 0 = Nothing +divide x y = case divMod x y of + (a,0) -> Just a + _ -> Nothing + +-- | Compute the exact root of a natural number. +-- The second argument specifies which root we are computing. +rootExact :: Integer -> Integer -> Maybe Integer +rootExact x y = do (z,True) <- genRoot x y + return z + + + +{- | Compute the n-th root of a natural number, rounded down to +the closest natural number. The boolean indicates if the result +is exact (i.e., True means no rounding was done, False means rounded down). +The second argument specifies which root we are computing. -} +genRoot :: Integer -> Integer -> Maybe (Integer, Bool) +genRoot _ 0 = Nothing +genRoot x0 1 = Just (x0, True) +genRoot x0 root = Just (search 0 (x0+1)) + where + search from to = let x = from + div (to - from) 2 + a = x ^ root + in case compare a x0 of + EQ -> (x, True) + LT | x /= from -> search x to + | otherwise -> (from, False) + GT | x /= to -> search from x + | otherwise -> (from, False) + +{- | Compute the logarithm of a number in the given base, rounded down to the +closest integer. The boolean indicates if we the result is exact +(i.e., True means no rounding happened, False means we rounded down). +The logarithm base is the second argument. -} +genLog :: Integer -> Integer -> Maybe (Integer, Bool) +genLog x 0 = if x == 1 then Just (0, True) else Nothing +genLog _ 1 = Nothing +genLog 0 _ = Nothing +genLog x base = Just (exactLoop 0 x) + where + exactLoop s i + | i == 1 = (s,True) + | i < base = (s,False) + | otherwise = + let s1 = s + 1 + in s1 `seq` case divMod i base of + (j,r) + | r == 0 -> exactLoop s1 j + | otherwise -> (underLoop s1 j, False) + + underLoop s i + | i < base = s + | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base) diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs new file mode 100644 index 0000000000..4bee18b964 --- /dev/null +++ b/compiler/GHC/Builtin/Types/Prim.hs @@ -0,0 +1,1110 @@ +{- +(c) The AQUA Project, Glasgow University, 1994-1998 + + +Wired-in knowledge about primitive types +-} + +{-# LANGUAGE CPP #-} +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} + +-- | This module defines TyCons that can't be expressed in Haskell. +-- They are all, therefore, wired-in TyCons. C.f module GHC.Builtin.Types +module GHC.Builtin.Types.Prim( + mkPrimTyConName, -- For implicit parameters in GHC.Builtin.Types only + + mkTemplateKindVars, mkTemplateTyVars, mkTemplateTyVarsFrom, + mkTemplateKiTyVars, mkTemplateKiTyVar, + + mkTemplateTyConBinders, mkTemplateKindTyConBinders, + mkTemplateAnonTyConBinders, + + alphaTyVars, alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar, + alphaTys, alphaTy, betaTy, gammaTy, deltaTy, + alphaTyVarsUnliftedRep, alphaTyVarUnliftedRep, + alphaTysUnliftedRep, alphaTyUnliftedRep, + runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep1Ty, runtimeRep2Ty, + openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar, + + -- Kind constructors... + tYPETyCon, tYPETyConName, + + -- Kinds + tYPE, primRepToRuntimeRep, + + funTyCon, funTyConName, + unexposedPrimTyCons, exposedPrimTyCons, primTyCons, + + charPrimTyCon, charPrimTy, charPrimTyConName, + intPrimTyCon, intPrimTy, intPrimTyConName, + wordPrimTyCon, wordPrimTy, wordPrimTyConName, + addrPrimTyCon, addrPrimTy, addrPrimTyConName, + floatPrimTyCon, floatPrimTy, floatPrimTyConName, + doublePrimTyCon, doublePrimTy, doublePrimTyConName, + + voidPrimTyCon, voidPrimTy, + statePrimTyCon, mkStatePrimTy, + realWorldTyCon, realWorldTy, realWorldStatePrimTy, + + proxyPrimTyCon, mkProxyPrimTy, + + arrayPrimTyCon, mkArrayPrimTy, + byteArrayPrimTyCon, byteArrayPrimTy, + arrayArrayPrimTyCon, mkArrayArrayPrimTy, + smallArrayPrimTyCon, mkSmallArrayPrimTy, + mutableArrayPrimTyCon, mkMutableArrayPrimTy, + mutableByteArrayPrimTyCon, mkMutableByteArrayPrimTy, + mutableArrayArrayPrimTyCon, mkMutableArrayArrayPrimTy, + smallMutableArrayPrimTyCon, mkSmallMutableArrayPrimTy, + mutVarPrimTyCon, mkMutVarPrimTy, + + mVarPrimTyCon, mkMVarPrimTy, + tVarPrimTyCon, mkTVarPrimTy, + stablePtrPrimTyCon, mkStablePtrPrimTy, + stableNamePrimTyCon, mkStableNamePrimTy, + compactPrimTyCon, compactPrimTy, + bcoPrimTyCon, bcoPrimTy, + weakPrimTyCon, mkWeakPrimTy, + threadIdPrimTyCon, threadIdPrimTy, + + int8PrimTyCon, int8PrimTy, int8PrimTyConName, + word8PrimTyCon, word8PrimTy, word8PrimTyConName, + + int16PrimTyCon, int16PrimTy, int16PrimTyConName, + word16PrimTyCon, word16PrimTy, word16PrimTyConName, + + int32PrimTyCon, int32PrimTy, int32PrimTyConName, + word32PrimTyCon, word32PrimTy, word32PrimTyConName, + + int64PrimTyCon, int64PrimTy, int64PrimTyConName, + word64PrimTyCon, word64PrimTy, word64PrimTyConName, + + eqPrimTyCon, -- ty1 ~# ty2 + eqReprPrimTyCon, -- ty1 ~R# ty2 (at role Representational) + eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom) + equalityTyCon, + + -- * SIMD +#include "primop-vector-tys-exports.hs-incl" + ) where + +#include "HsVersions.h" + +import GhcPrelude + +import {-# SOURCE #-} GHC.Builtin.Types + ( runtimeRepTy, unboxedTupleKind, liftedTypeKind + , vecRepDataConTyCon, tupleRepDataConTyCon + , liftedRepDataConTy, unliftedRepDataConTy + , intRepDataConTy + , int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy + , wordRepDataConTy + , word16RepDataConTy, word8RepDataConTy, word32RepDataConTy, word64RepDataConTy + , addrRepDataConTy + , floatRepDataConTy, doubleRepDataConTy + , vec2DataConTy, vec4DataConTy, vec8DataConTy, vec16DataConTy, vec32DataConTy + , vec64DataConTy + , int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy + , int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy + , word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy + , doubleElemRepDataConTy + , mkPromotedListTy ) + +import GHC.Types.Var ( TyVar, mkTyVar ) +import GHC.Types.Name +import GHC.Core.TyCon +import GHC.Types.SrcLoc +import GHC.Types.Unique +import GHC.Builtin.Names +import FastString +import Outputable +import GHC.Core.TyCo.Rep -- Doesn't need special access, but this is easier to avoid + -- import loops which show up if you import Type instead + +import Data.Char + +{- +************************************************************************ +* * +\subsection{Primitive type constructors} +* * +************************************************************************ +-} + +primTyCons :: [TyCon] +primTyCons = unexposedPrimTyCons ++ exposedPrimTyCons + +-- | Primitive 'TyCon's that are defined in "GHC.Prim" but not exposed. +-- It's important to keep these separate as we don't want users to be able to +-- write them (see #15209) or see them in GHCi's @:browse@ output +-- (see #12023). +unexposedPrimTyCons :: [TyCon] +unexposedPrimTyCons + = [ eqPrimTyCon + , eqReprPrimTyCon + , eqPhantPrimTyCon + ] + +-- | Primitive 'TyCon's that are defined in, and exported from, "GHC.Prim". +exposedPrimTyCons :: [TyCon] +exposedPrimTyCons + = [ addrPrimTyCon + , arrayPrimTyCon + , byteArrayPrimTyCon + , arrayArrayPrimTyCon + , smallArrayPrimTyCon + , charPrimTyCon + , doublePrimTyCon + , floatPrimTyCon + , intPrimTyCon + , int8PrimTyCon + , int16PrimTyCon + , int32PrimTyCon + , int64PrimTyCon + , bcoPrimTyCon + , weakPrimTyCon + , mutableArrayPrimTyCon + , mutableByteArrayPrimTyCon + , mutableArrayArrayPrimTyCon + , smallMutableArrayPrimTyCon + , mVarPrimTyCon + , tVarPrimTyCon + , mutVarPrimTyCon + , realWorldTyCon + , stablePtrPrimTyCon + , stableNamePrimTyCon + , compactPrimTyCon + , statePrimTyCon + , voidPrimTyCon + , proxyPrimTyCon + , threadIdPrimTyCon + , wordPrimTyCon + , word8PrimTyCon + , word16PrimTyCon + , word32PrimTyCon + , word64PrimTyCon + + , tYPETyCon + +#include "primop-vector-tycons.hs-incl" + ] + +mkPrimTc :: FastString -> Unique -> TyCon -> Name +mkPrimTc fs unique tycon + = mkWiredInName gHC_PRIM (mkTcOccFS fs) + unique + (ATyCon tycon) -- Relevant TyCon + UserSyntax + +mkBuiltInPrimTc :: FastString -> Unique -> TyCon -> Name +mkBuiltInPrimTc fs unique tycon + = mkWiredInName gHC_PRIM (mkTcOccFS fs) + unique + (ATyCon tycon) -- Relevant TyCon + BuiltInSyntax + + +charPrimTyConName, intPrimTyConName, int8PrimTyConName, int16PrimTyConName, int32PrimTyConName, int64PrimTyConName, wordPrimTyConName, word32PrimTyConName, word8PrimTyConName, word16PrimTyConName, word64PrimTyConName, addrPrimTyConName, floatPrimTyConName, doublePrimTyConName, statePrimTyConName, proxyPrimTyConName, realWorldTyConName, arrayPrimTyConName, arrayArrayPrimTyConName, smallArrayPrimTyConName, byteArrayPrimTyConName, mutableArrayPrimTyConName, mutableByteArrayPrimTyConName, mutableArrayArrayPrimTyConName, smallMutableArrayPrimTyConName, mutVarPrimTyConName, mVarPrimTyConName, tVarPrimTyConName, stablePtrPrimTyConName, stableNamePrimTyConName, compactPrimTyConName, bcoPrimTyConName, weakPrimTyConName, threadIdPrimTyConName, eqPrimTyConName, eqReprPrimTyConName, eqPhantPrimTyConName, voidPrimTyConName :: Name +charPrimTyConName = mkPrimTc (fsLit "Char#") charPrimTyConKey charPrimTyCon +intPrimTyConName = mkPrimTc (fsLit "Int#") intPrimTyConKey intPrimTyCon +int8PrimTyConName = mkPrimTc (fsLit "Int8#") int8PrimTyConKey int8PrimTyCon +int16PrimTyConName = mkPrimTc (fsLit "Int16#") int16PrimTyConKey int16PrimTyCon +int32PrimTyConName = mkPrimTc (fsLit "Int32#") int32PrimTyConKey int32PrimTyCon +int64PrimTyConName = mkPrimTc (fsLit "Int64#") int64PrimTyConKey int64PrimTyCon +wordPrimTyConName = mkPrimTc (fsLit "Word#") wordPrimTyConKey wordPrimTyCon +word8PrimTyConName = mkPrimTc (fsLit "Word8#") word8PrimTyConKey word8PrimTyCon +word16PrimTyConName = mkPrimTc (fsLit "Word16#") word16PrimTyConKey word16PrimTyCon +word32PrimTyConName = mkPrimTc (fsLit "Word32#") word32PrimTyConKey word32PrimTyCon +word64PrimTyConName = mkPrimTc (fsLit "Word64#") word64PrimTyConKey word64PrimTyCon +addrPrimTyConName = mkPrimTc (fsLit "Addr#") addrPrimTyConKey addrPrimTyCon +floatPrimTyConName = mkPrimTc (fsLit "Float#") floatPrimTyConKey floatPrimTyCon +doublePrimTyConName = mkPrimTc (fsLit "Double#") doublePrimTyConKey doublePrimTyCon +statePrimTyConName = mkPrimTc (fsLit "State#") statePrimTyConKey statePrimTyCon +voidPrimTyConName = mkPrimTc (fsLit "Void#") voidPrimTyConKey voidPrimTyCon +proxyPrimTyConName = mkPrimTc (fsLit "Proxy#") proxyPrimTyConKey proxyPrimTyCon +eqPrimTyConName = mkPrimTc (fsLit "~#") eqPrimTyConKey eqPrimTyCon +eqReprPrimTyConName = mkBuiltInPrimTc (fsLit "~R#") eqReprPrimTyConKey eqReprPrimTyCon +eqPhantPrimTyConName = mkBuiltInPrimTc (fsLit "~P#") eqPhantPrimTyConKey eqPhantPrimTyCon +realWorldTyConName = mkPrimTc (fsLit "RealWorld") realWorldTyConKey realWorldTyCon +arrayPrimTyConName = mkPrimTc (fsLit "Array#") arrayPrimTyConKey arrayPrimTyCon +byteArrayPrimTyConName = mkPrimTc (fsLit "ByteArray#") byteArrayPrimTyConKey byteArrayPrimTyCon +arrayArrayPrimTyConName = mkPrimTc (fsLit "ArrayArray#") arrayArrayPrimTyConKey arrayArrayPrimTyCon +smallArrayPrimTyConName = mkPrimTc (fsLit "SmallArray#") smallArrayPrimTyConKey smallArrayPrimTyCon +mutableArrayPrimTyConName = mkPrimTc (fsLit "MutableArray#") mutableArrayPrimTyConKey mutableArrayPrimTyCon +mutableByteArrayPrimTyConName = mkPrimTc (fsLit "MutableByteArray#") mutableByteArrayPrimTyConKey mutableByteArrayPrimTyCon +mutableArrayArrayPrimTyConName= mkPrimTc (fsLit "MutableArrayArray#") mutableArrayArrayPrimTyConKey mutableArrayArrayPrimTyCon +smallMutableArrayPrimTyConName= mkPrimTc (fsLit "SmallMutableArray#") smallMutableArrayPrimTyConKey smallMutableArrayPrimTyCon +mutVarPrimTyConName = mkPrimTc (fsLit "MutVar#") mutVarPrimTyConKey mutVarPrimTyCon +mVarPrimTyConName = mkPrimTc (fsLit "MVar#") mVarPrimTyConKey mVarPrimTyCon +tVarPrimTyConName = mkPrimTc (fsLit "TVar#") tVarPrimTyConKey tVarPrimTyCon +stablePtrPrimTyConName = mkPrimTc (fsLit "StablePtr#") stablePtrPrimTyConKey stablePtrPrimTyCon +stableNamePrimTyConName = mkPrimTc (fsLit "StableName#") stableNamePrimTyConKey stableNamePrimTyCon +compactPrimTyConName = mkPrimTc (fsLit "Compact#") compactPrimTyConKey compactPrimTyCon +bcoPrimTyConName = mkPrimTc (fsLit "BCO") bcoPrimTyConKey bcoPrimTyCon +weakPrimTyConName = mkPrimTc (fsLit "Weak#") weakPrimTyConKey weakPrimTyCon +threadIdPrimTyConName = mkPrimTc (fsLit "ThreadId#") threadIdPrimTyConKey threadIdPrimTyCon + +{- +************************************************************************ +* * +\subsection{Support code} +* * +************************************************************************ + +alphaTyVars is a list of type variables for use in templates: + ["a", "b", ..., "z", "t1", "t2", ... ] +-} + +mkTemplateKindVar :: Kind -> TyVar +mkTemplateKindVar = mkTyVar (mk_tv_name 0 "k") + +mkTemplateKindVars :: [Kind] -> [TyVar] +-- k0 with unique (mkAlphaTyVarUnique 0) +-- k1 with unique (mkAlphaTyVarUnique 1) +-- ... etc +mkTemplateKindVars [kind] = [mkTemplateKindVar kind] + -- Special case for one kind: just "k" +mkTemplateKindVars kinds + = [ mkTyVar (mk_tv_name u ('k' : show u)) kind + | (kind, u) <- kinds `zip` [0..] ] +mk_tv_name :: Int -> String -> Name +mk_tv_name u s = mkInternalName (mkAlphaTyVarUnique u) + (mkTyVarOccFS (mkFastString s)) + noSrcSpan + +mkTemplateTyVarsFrom :: Int -> [Kind] -> [TyVar] +-- a with unique (mkAlphaTyVarUnique n) +-- b with unique (mkAlphaTyVarUnique n+1) +-- ... etc +-- Typically called as +-- mkTemplateTyVarsFrom (length kv_bndrs) kinds +-- where kv_bndrs are the kind-level binders of a TyCon +mkTemplateTyVarsFrom n kinds + = [ mkTyVar name kind + | (kind, index) <- zip kinds [0..], + let ch_ord = index + ord 'a' + name_str | ch_ord <= ord 'z' = [chr ch_ord] + | otherwise = 't':show index + name = mk_tv_name (index + n) name_str + ] + +mkTemplateTyVars :: [Kind] -> [TyVar] +mkTemplateTyVars = mkTemplateTyVarsFrom 1 + +mkTemplateTyConBinders + :: [Kind] -- [k1, .., kn] Kinds of kind-forall'd vars + -> ([Kind] -> [Kind]) -- Arg is [kv1:k1, ..., kvn:kn] + -- same length as first arg + -- Result is anon arg kinds + -> [TyConBinder] +mkTemplateTyConBinders kind_var_kinds mk_anon_arg_kinds + = kv_bndrs ++ tv_bndrs + where + kv_bndrs = mkTemplateKindTyConBinders kind_var_kinds + anon_kinds = mk_anon_arg_kinds (mkTyVarTys (binderVars kv_bndrs)) + tv_bndrs = mkTemplateAnonTyConBindersFrom (length kv_bndrs) anon_kinds + +mkTemplateKiTyVars + :: [Kind] -- [k1, .., kn] Kinds of kind-forall'd vars + -> ([Kind] -> [Kind]) -- Arg is [kv1:k1, ..., kvn:kn] + -- same length as first arg + -- Result is anon arg kinds [ak1, .., akm] + -> [TyVar] -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm] +-- Example: if you want the tyvars for +-- forall (r:RuntimeRep) (a:TYPE r) (b:*). blah +-- call mkTemplateKiTyVars [RuntimeRep] (\[r] -> [TYPE r, *]) +mkTemplateKiTyVars kind_var_kinds mk_arg_kinds + = kv_bndrs ++ tv_bndrs + where + kv_bndrs = mkTemplateKindVars kind_var_kinds + anon_kinds = mk_arg_kinds (mkTyVarTys kv_bndrs) + tv_bndrs = mkTemplateTyVarsFrom (length kv_bndrs) anon_kinds + +mkTemplateKiTyVar + :: Kind -- [k1, .., kn] Kind of kind-forall'd var + -> (Kind -> [Kind]) -- Arg is kv1:k1 + -- Result is anon arg kinds [ak1, .., akm] + -> [TyVar] -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm] +-- Example: if you want the tyvars for +-- forall (r:RuntimeRep) (a:TYPE r) (b:*). blah +-- call mkTemplateKiTyVar RuntimeRep (\r -> [TYPE r, *]) +mkTemplateKiTyVar kind mk_arg_kinds + = kv_bndr : tv_bndrs + where + kv_bndr = mkTemplateKindVar kind + anon_kinds = mk_arg_kinds (mkTyVarTy kv_bndr) + tv_bndrs = mkTemplateTyVarsFrom 1 anon_kinds + +mkTemplateKindTyConBinders :: [Kind] -> [TyConBinder] +-- Makes named, Specified binders +mkTemplateKindTyConBinders kinds = [mkNamedTyConBinder Specified tv | tv <- mkTemplateKindVars kinds] + +mkTemplateAnonTyConBinders :: [Kind] -> [TyConBinder] +mkTemplateAnonTyConBinders kinds = mkAnonTyConBinders VisArg (mkTemplateTyVars kinds) + +mkTemplateAnonTyConBindersFrom :: Int -> [Kind] -> [TyConBinder] +mkTemplateAnonTyConBindersFrom n kinds = mkAnonTyConBinders VisArg (mkTemplateTyVarsFrom n kinds) + +alphaTyVars :: [TyVar] +alphaTyVars = mkTemplateTyVars $ repeat liftedTypeKind + +alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar :: TyVar +(alphaTyVar:betaTyVar:gammaTyVar:deltaTyVar:_) = alphaTyVars + +alphaTys :: [Type] +alphaTys = mkTyVarTys alphaTyVars +alphaTy, betaTy, gammaTy, deltaTy :: Type +(alphaTy:betaTy:gammaTy:deltaTy:_) = alphaTys + +alphaTyVarsUnliftedRep :: [TyVar] +alphaTyVarsUnliftedRep = mkTemplateTyVars $ repeat (tYPE unliftedRepDataConTy) + +alphaTyVarUnliftedRep :: TyVar +(alphaTyVarUnliftedRep:_) = alphaTyVarsUnliftedRep + +alphaTysUnliftedRep :: [Type] +alphaTysUnliftedRep = mkTyVarTys alphaTyVarsUnliftedRep +alphaTyUnliftedRep :: Type +(alphaTyUnliftedRep:_) = alphaTysUnliftedRep + +runtimeRep1TyVar, runtimeRep2TyVar :: TyVar +(runtimeRep1TyVar : runtimeRep2TyVar : _) + = drop 16 (mkTemplateTyVars (repeat runtimeRepTy)) -- selects 'q','r' + +runtimeRep1Ty, runtimeRep2Ty :: Type +runtimeRep1Ty = mkTyVarTy runtimeRep1TyVar +runtimeRep2Ty = mkTyVarTy runtimeRep2TyVar + +openAlphaTyVar, openBetaTyVar :: TyVar +-- alpha :: TYPE r1 +-- beta :: TYPE r2 +[openAlphaTyVar,openBetaTyVar] + = mkTemplateTyVars [tYPE runtimeRep1Ty, tYPE runtimeRep2Ty] + +openAlphaTy, openBetaTy :: Type +openAlphaTy = mkTyVarTy openAlphaTyVar +openBetaTy = mkTyVarTy openBetaTyVar + +{- +************************************************************************ +* * + FunTyCon +* * +************************************************************************ +-} + +funTyConName :: Name +funTyConName = mkPrimTyConName (fsLit "->") funTyConKey funTyCon + +-- | The @(->)@ type constructor. +-- +-- @ +-- (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep). +-- TYPE rep1 -> TYPE rep2 -> * +-- @ +funTyCon :: TyCon +funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm + where + tc_bndrs = [ mkNamedTyConBinder Inferred runtimeRep1TyVar + , mkNamedTyConBinder Inferred runtimeRep2TyVar ] + ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty + , tYPE runtimeRep2Ty + ] + tc_rep_nm = mkPrelTyConRepName funTyConName + +{- +************************************************************************ +* * + Kinds +* * +************************************************************************ + +Note [TYPE and RuntimeRep] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +All types that classify values have a kind of the form (TYPE rr), where + + data RuntimeRep -- Defined in ghc-prim:GHC.Types + = LiftedRep + | UnliftedRep + | IntRep + | FloatRep + .. etc .. + + rr :: RuntimeRep + + TYPE :: RuntimeRep -> TYPE 'LiftedRep -- Built in + +So for example: + Int :: TYPE 'LiftedRep + Array# Int :: TYPE 'UnliftedRep + Int# :: TYPE 'IntRep + Float# :: TYPE 'FloatRep + Maybe :: TYPE 'LiftedRep -> TYPE 'LiftedRep + (# , #) :: TYPE r1 -> TYPE r2 -> TYPE (TupleRep [r1, r2]) + +We abbreviate '*' specially: + type * = TYPE 'LiftedRep + +The 'rr' parameter tells us how the value is represented at runtime. + +Generally speaking, you can't be polymorphic in 'rr'. E.g + f :: forall (rr:RuntimeRep) (a:TYPE rr). a -> [a] + f = /\(rr:RuntimeRep) (a:rr) \(a:rr). ... +This is no good: we could not generate code code for 'f', because the +calling convention for 'f' varies depending on whether the argument is +a a Int, Int#, or Float#. (You could imagine generating specialised +code, one for each instantiation of 'rr', but we don't do that.) + +Certain functions CAN be runtime-rep-polymorphic, because the code +generator never has to manipulate a value of type 'a :: TYPE rr'. + +* error :: forall (rr:RuntimeRep) (a:TYPE rr). String -> a + Code generator never has to manipulate the return value. + +* unsafeCoerce#, defined in Desugar.mkUnsafeCoercePair: + Always inlined to be a no-op + unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + a -> b + +* Unboxed tuples, and unboxed sums, defined in GHC.Builtin.Types + Always inlined, and hence specialised to the call site + (#,#) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + a -> b -> TYPE ('TupleRep '[r1, r2]) + +Note [PrimRep and kindPrimRep] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As part of its source code, in GHC.Core.TyCon, GHC has + data PrimRep = LiftedRep | UnliftedRep | IntRep | FloatRep | ...etc... + +Notice that + * RuntimeRep is part of the syntax tree of the program being compiled + (defined in a library: ghc-prim:GHC.Types) + * PrimRep is part of GHC's source code. + (defined in GHC.Core.TyCon) + +We need to get from one to the other; that is what kindPrimRep does. +Suppose we have a value + (v :: t) where (t :: k) +Given this kind + k = TyConApp "TYPE" [rep] +GHC needs to be able to figure out how 'v' is represented at runtime. +It expects 'rep' to be form + TyConApp rr_dc args +where 'rr_dc' is a promoteed data constructor from RuntimeRep. So +now we need to go from 'dc' to the corresponding PrimRep. We store this +PrimRep in the promoted data constructor itself: see TyCon.promDcRepInfo. + +-} + +tYPETyCon :: TyCon +tYPETyConName :: Name + +tYPETyCon = mkKindTyCon tYPETyConName + (mkTemplateAnonTyConBinders [runtimeRepTy]) + liftedTypeKind + [Nominal] + (mkPrelTyConRepName tYPETyConName) + +-------------------------- +-- ... and now their names + +-- If you edit these, you may need to update the GHC formalism +-- See Note [GHC Formalism] in GHC.Core.Lint +tYPETyConName = mkPrimTyConName (fsLit "TYPE") tYPETyConKey tYPETyCon + +mkPrimTyConName :: FastString -> Unique -> TyCon -> Name +mkPrimTyConName = mkPrimTcName BuiltInSyntax + -- All of the super kinds and kinds are defined in Prim, + -- and use BuiltInSyntax, because they are never in scope in the source + +mkPrimTcName :: BuiltInSyntax -> FastString -> Unique -> TyCon -> Name +mkPrimTcName built_in_syntax occ key tycon + = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (ATyCon tycon) built_in_syntax + +----------------------------- +-- | Given a RuntimeRep, applies TYPE to it. +-- see Note [TYPE and RuntimeRep] +tYPE :: Type -> Type +tYPE rr = TyConApp tYPETyCon [rr] + +{- +************************************************************************ +* * + Basic primitive types (@Char#@, @Int#@, etc.) +* * +************************************************************************ +-} + +-- only used herein +pcPrimTyCon :: Name -> [Role] -> PrimRep -> TyCon +pcPrimTyCon name roles rep + = mkPrimTyCon name binders result_kind roles + where + binders = mkTemplateAnonTyConBinders (map (const liftedTypeKind) roles) + result_kind = tYPE (primRepToRuntimeRep rep) + +-- | Convert a 'PrimRep' to a 'Type' of kind RuntimeRep +-- Defined here to avoid (more) module loops +primRepToRuntimeRep :: PrimRep -> Type +primRepToRuntimeRep rep = case rep of + VoidRep -> TyConApp tupleRepDataConTyCon [mkPromotedListTy runtimeRepTy []] + LiftedRep -> liftedRepDataConTy + UnliftedRep -> unliftedRepDataConTy + IntRep -> intRepDataConTy + Int8Rep -> int8RepDataConTy + Int16Rep -> int16RepDataConTy + Int32Rep -> int32RepDataConTy + Int64Rep -> int64RepDataConTy + WordRep -> wordRepDataConTy + Word8Rep -> word8RepDataConTy + Word16Rep -> word16RepDataConTy + Word32Rep -> word32RepDataConTy + Word64Rep -> word64RepDataConTy + AddrRep -> addrRepDataConTy + FloatRep -> floatRepDataConTy + DoubleRep -> doubleRepDataConTy + VecRep n elem -> TyConApp vecRepDataConTyCon [n', elem'] + where + n' = case n of + 2 -> vec2DataConTy + 4 -> vec4DataConTy + 8 -> vec8DataConTy + 16 -> vec16DataConTy + 32 -> vec32DataConTy + 64 -> vec64DataConTy + _ -> pprPanic "Disallowed VecCount" (ppr n) + + elem' = case elem of + Int8ElemRep -> int8ElemRepDataConTy + Int16ElemRep -> int16ElemRepDataConTy + Int32ElemRep -> int32ElemRepDataConTy + Int64ElemRep -> int64ElemRepDataConTy + Word8ElemRep -> word8ElemRepDataConTy + Word16ElemRep -> word16ElemRepDataConTy + Word32ElemRep -> word32ElemRepDataConTy + Word64ElemRep -> word64ElemRepDataConTy + FloatElemRep -> floatElemRepDataConTy + DoubleElemRep -> doubleElemRepDataConTy + +pcPrimTyCon0 :: Name -> PrimRep -> TyCon +pcPrimTyCon0 name rep + = pcPrimTyCon name [] rep + +charPrimTy :: Type +charPrimTy = mkTyConTy charPrimTyCon +charPrimTyCon :: TyCon +charPrimTyCon = pcPrimTyCon0 charPrimTyConName WordRep + +intPrimTy :: Type +intPrimTy = mkTyConTy intPrimTyCon +intPrimTyCon :: TyCon +intPrimTyCon = pcPrimTyCon0 intPrimTyConName IntRep + +int8PrimTy :: Type +int8PrimTy = mkTyConTy int8PrimTyCon +int8PrimTyCon :: TyCon +int8PrimTyCon = pcPrimTyCon0 int8PrimTyConName Int8Rep + +int16PrimTy :: Type +int16PrimTy = mkTyConTy int16PrimTyCon +int16PrimTyCon :: TyCon +int16PrimTyCon = pcPrimTyCon0 int16PrimTyConName Int16Rep + +int32PrimTy :: Type +int32PrimTy = mkTyConTy int32PrimTyCon +int32PrimTyCon :: TyCon +int32PrimTyCon = pcPrimTyCon0 int32PrimTyConName Int32Rep + +int64PrimTy :: Type +int64PrimTy = mkTyConTy int64PrimTyCon +int64PrimTyCon :: TyCon +int64PrimTyCon = pcPrimTyCon0 int64PrimTyConName Int64Rep + +wordPrimTy :: Type +wordPrimTy = mkTyConTy wordPrimTyCon +wordPrimTyCon :: TyCon +wordPrimTyCon = pcPrimTyCon0 wordPrimTyConName WordRep + +word8PrimTy :: Type +word8PrimTy = mkTyConTy word8PrimTyCon +word8PrimTyCon :: TyCon +word8PrimTyCon = pcPrimTyCon0 word8PrimTyConName Word8Rep + +word16PrimTy :: Type +word16PrimTy = mkTyConTy word16PrimTyCon +word16PrimTyCon :: TyCon +word16PrimTyCon = pcPrimTyCon0 word16PrimTyConName Word16Rep + +word32PrimTy :: Type +word32PrimTy = mkTyConTy word32PrimTyCon +word32PrimTyCon :: TyCon +word32PrimTyCon = pcPrimTyCon0 word32PrimTyConName Word32Rep + +word64PrimTy :: Type +word64PrimTy = mkTyConTy word64PrimTyCon +word64PrimTyCon :: TyCon +word64PrimTyCon = pcPrimTyCon0 word64PrimTyConName Word64Rep + +addrPrimTy :: Type +addrPrimTy = mkTyConTy addrPrimTyCon +addrPrimTyCon :: TyCon +addrPrimTyCon = pcPrimTyCon0 addrPrimTyConName AddrRep + +floatPrimTy :: Type +floatPrimTy = mkTyConTy floatPrimTyCon +floatPrimTyCon :: TyCon +floatPrimTyCon = pcPrimTyCon0 floatPrimTyConName FloatRep + +doublePrimTy :: Type +doublePrimTy = mkTyConTy doublePrimTyCon +doublePrimTyCon :: TyCon +doublePrimTyCon = pcPrimTyCon0 doublePrimTyConName DoubleRep + +{- +************************************************************************ +* * + The @State#@ type (and @_RealWorld@ types) +* * +************************************************************************ + +Note [The equality types story] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +GHC sports a veritable menagerie of equality types: + + Type or Lifted? Hetero? Role Built in Defining module + class? L/U TyCon +----------------------------------------------------------------------------------------- +~# T U hetero nominal eqPrimTyCon GHC.Prim +~~ C L hetero nominal heqTyCon GHC.Types +~ C L homo nominal eqTyCon GHC.Types +:~: T L homo nominal (not built-in) Data.Type.Equality +:~~: T L hetero nominal (not built-in) Data.Type.Equality + +~R# T U hetero repr eqReprPrimTy GHC.Prim +Coercible C L homo repr coercibleTyCon GHC.Types +Coercion T L homo repr (not built-in) Data.Type.Coercion +~P# T U hetero phantom eqPhantPrimTyCon GHC.Prim + +Recall that "hetero" means the equality can related types of different +kinds. Knowing that (t1 ~# t2) or (t1 ~R# t2) or even that (t1 ~P# t2) +also means that (k1 ~# k2), where (t1 :: k1) and (t2 :: k2). + +To produce less confusion for end users, when not dumping and without +-fprint-equality-relations, each of these groups is printed as the bottommost +listed equality. That is, (~#) and (~~) are both rendered as (~) in +error messages, and (~R#) is rendered as Coercible. + +Let's take these one at a time: + + -------------------------- + (~#) :: forall k1 k2. k1 -> k2 -> # + -------------------------- +This is The Type Of Equality in GHC. It classifies nominal coercions. +This type is used in the solver for recording equality constraints. +It responds "yes" to Type.isEqPrimPred and classifies as an EqPred in +Type.classifyPredType. + +All wanted constraints of this type are built with coercion holes. +(See Note [Coercion holes] in GHC.Core.TyCo.Rep.) But see also +Note [Deferred errors for coercion holes] in GHC.Tc.Errors to see how +equality constraints are deferred. + +Within GHC, ~# is called eqPrimTyCon, and it is defined in GHC.Builtin.Types.Prim. + + + -------------------------- + (~~) :: forall k1 k2. k1 -> k2 -> Constraint + -------------------------- +This is (almost) an ordinary class, defined as if by + class a ~# b => a ~~ b + instance a ~# b => a ~~ b +Here's what's unusual about it: + + * We can't actually declare it that way because we don't have syntax for ~#. + And ~# isn't a constraint, so even if we could write it, it wouldn't kind + check. + + * Users cannot write instances of it. + + * It is "naturally coherent". This means that the solver won't hesitate to + solve a goal of type (a ~~ b) even if there is, say (Int ~~ c) in the + context. (Normally, it waits to learn more, just in case the given + influences what happens next.) See Note [Naturally coherent classes] + in GHC.Tc.Solver.Interact. + + * It always terminates. That is, in the UndecidableInstances checks, we + don't worry if a (~~) constraint is too big, as we know that solving + equality terminates. + +On the other hand, this behaves just like any class w.r.t. eager superclass +unpacking in the solver. So a lifted equality given quickly becomes an unlifted +equality given. This is good, because the solver knows all about unlifted +equalities. There is some special-casing in GHC.Tc.Solver.Interact.matchClassInst to +pretend that there is an instance of this class, as we can't write the instance +in Haskell. + +Within GHC, ~~ is called heqTyCon, and it is defined in GHC.Builtin.Types. + + + -------------------------- + (~) :: forall k. k -> k -> Constraint + -------------------------- +This is /exactly/ like (~~), except with a homogeneous kind. +It is an almost-ordinary class defined as if by + class a ~# b => (a :: k) ~ (b :: k) + instance a ~# b => a ~ b + + * All the bullets for (~~) apply + + * In addition (~) is magical syntax, as ~ is a reserved symbol. + It cannot be exported or imported. + +Within GHC, ~ is called eqTyCon, and it is defined in GHC.Builtin.Types. + +Historical note: prior to July 18 (~) was defined as a + more-ordinary class with (~~) as a superclass. But that made it + special in different ways; and the extra superclass selections to + get from (~) to (~#) via (~~) were tiresome. Now it's defined + uniformly with (~~) and Coercible; much nicer.) + + + -------------------------- + (:~:) :: forall k. k -> k -> * + (:~~:) :: forall k1 k2. k1 -> k2 -> * + -------------------------- +These are perfectly ordinary GADTs, wrapping (~) and (~~) resp. +They are not defined within GHC at all. + + + -------------------------- + (~R#) :: forall k1 k2. k1 -> k2 -> # + -------------------------- +The is the representational analogue of ~#. This is the type of representational +equalities that the solver works on. All wanted constraints of this type are +built with coercion holes. + +Within GHC, ~R# is called eqReprPrimTyCon, and it is defined in GHC.Builtin.Types.Prim. + + + -------------------------- + Coercible :: forall k. k -> k -> Constraint + -------------------------- +This is quite like (~~) in the way it's defined and treated within GHC, but +it's homogeneous. Homogeneity helps with type inference (as GHC can solve one +kind from the other) and, in my (Richard's) estimation, will be more intuitive +for users. + +An alternative design included HCoercible (like (~~)) and Coercible (like (~)). +One annoyance was that we want `coerce :: Coercible a b => a -> b`, and +we need the type of coerce to be fully wired-in. So the HCoercible/Coercible +split required that both types be fully wired-in. Instead of doing this, +I just got rid of HCoercible, as I'm not sure who would use it, anyway. + +Within GHC, Coercible is called coercibleTyCon, and it is defined in +GHC.Builtin.Types. + + + -------------------------- + Coercion :: forall k. k -> k -> * + -------------------------- +This is a perfectly ordinary GADT, wrapping Coercible. It is not defined +within GHC at all. + + + -------------------------- + (~P#) :: forall k1 k2. k1 -> k2 -> # + -------------------------- +This is the phantom analogue of ~# and it is barely used at all. +(The solver has no idea about this one.) Here is the motivation: + + data Phant a = MkPhant + type role Phant phantom + + Phant <Int, Bool>_P :: Phant Int ~P# Phant Bool + +We just need to have something to put on that last line. You probably +don't need to worry about it. + + + +Note [The State# TyCon] +~~~~~~~~~~~~~~~~~~~~~~~ +State# is the primitive, unlifted type of states. It has one type parameter, +thus + State# RealWorld +or + State# s + +where s is a type variable. The only purpose of the type parameter is to +keep different state threads separate. It is represented by nothing at all. + +The type parameter to State# is intended to keep separate threads separate. +Even though this parameter is not used in the definition of State#, it is +given role Nominal to enforce its intended use. +-} + +mkStatePrimTy :: Type -> Type +mkStatePrimTy ty = TyConApp statePrimTyCon [ty] + +statePrimTyCon :: TyCon -- See Note [The State# TyCon] +statePrimTyCon = pcPrimTyCon statePrimTyConName [Nominal] VoidRep + +{- +RealWorld is deeply magical. It is *primitive*, but it is not +*unlifted* (hence ptrArg). We never manipulate values of type +RealWorld; it's only used in the type system, to parameterise State#. +-} + +realWorldTyCon :: TyCon +realWorldTyCon = mkLiftedPrimTyCon realWorldTyConName [] liftedTypeKind [] +realWorldTy :: Type +realWorldTy = mkTyConTy realWorldTyCon +realWorldStatePrimTy :: Type +realWorldStatePrimTy = mkStatePrimTy realWorldTy -- State# RealWorld + +-- Note: the ``state-pairing'' types are not truly primitive, +-- so they are defined in \tr{GHC.Builtin.Types}, not here. + + +voidPrimTy :: Type +voidPrimTy = TyConApp voidPrimTyCon [] + +voidPrimTyCon :: TyCon +voidPrimTyCon = pcPrimTyCon voidPrimTyConName [] VoidRep + +mkProxyPrimTy :: Type -> Type -> Type +mkProxyPrimTy k ty = TyConApp proxyPrimTyCon [k, ty] + +proxyPrimTyCon :: TyCon +proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName binders res_kind [Nominal,Phantom] + where + -- Kind: forall k. k -> TYPE (Tuple '[]) + binders = mkTemplateTyConBinders [liftedTypeKind] id + res_kind = unboxedTupleKind [] + + +{- ********************************************************************* +* * + Primitive equality constraints + See Note [The equality types story] +* * +********************************************************************* -} + +eqPrimTyCon :: TyCon -- The representation type for equality predicates + -- See Note [The equality types story] +eqPrimTyCon = mkPrimTyCon eqPrimTyConName binders res_kind roles + where + -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (Tuple '[]) + binders = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id + res_kind = unboxedTupleKind [] + roles = [Nominal, Nominal, Nominal, Nominal] + +-- like eqPrimTyCon, but the type for *Representational* coercions +-- this should only ever appear as the type of a covar. Its role is +-- interpreted in coercionRole +eqReprPrimTyCon :: TyCon -- See Note [The equality types story] +eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName binders res_kind roles + where + -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (Tuple '[]) + binders = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id + res_kind = unboxedTupleKind [] + roles = [Nominal, Nominal, Representational, Representational] + +-- like eqPrimTyCon, but the type for *Phantom* coercions. +-- This is only used to make higher-order equalities. Nothing +-- should ever actually have this type! +eqPhantPrimTyCon :: TyCon +eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName binders res_kind roles + where + -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (Tuple '[]) + binders = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id + res_kind = unboxedTupleKind [] + roles = [Nominal, Nominal, Phantom, Phantom] + +-- | Given a Role, what TyCon is the type of equality predicates at that role? +equalityTyCon :: Role -> TyCon +equalityTyCon Nominal = eqPrimTyCon +equalityTyCon Representational = eqReprPrimTyCon +equalityTyCon Phantom = eqPhantPrimTyCon + +{- ********************************************************************* +* * + The primitive array types +* * +********************************************************************* -} + +arrayPrimTyCon, mutableArrayPrimTyCon, mutableByteArrayPrimTyCon, + byteArrayPrimTyCon, arrayArrayPrimTyCon, mutableArrayArrayPrimTyCon, + smallArrayPrimTyCon, smallMutableArrayPrimTyCon :: TyCon +arrayPrimTyCon = pcPrimTyCon arrayPrimTyConName [Representational] UnliftedRep +mutableArrayPrimTyCon = pcPrimTyCon mutableArrayPrimTyConName [Nominal, Representational] UnliftedRep +mutableByteArrayPrimTyCon = pcPrimTyCon mutableByteArrayPrimTyConName [Nominal] UnliftedRep +byteArrayPrimTyCon = pcPrimTyCon0 byteArrayPrimTyConName UnliftedRep +arrayArrayPrimTyCon = pcPrimTyCon0 arrayArrayPrimTyConName UnliftedRep +mutableArrayArrayPrimTyCon = pcPrimTyCon mutableArrayArrayPrimTyConName [Nominal] UnliftedRep +smallArrayPrimTyCon = pcPrimTyCon smallArrayPrimTyConName [Representational] UnliftedRep +smallMutableArrayPrimTyCon = pcPrimTyCon smallMutableArrayPrimTyConName [Nominal, Representational] UnliftedRep + +mkArrayPrimTy :: Type -> Type +mkArrayPrimTy elt = TyConApp arrayPrimTyCon [elt] +byteArrayPrimTy :: Type +byteArrayPrimTy = mkTyConTy byteArrayPrimTyCon +mkArrayArrayPrimTy :: Type +mkArrayArrayPrimTy = mkTyConTy arrayArrayPrimTyCon +mkSmallArrayPrimTy :: Type -> Type +mkSmallArrayPrimTy elt = TyConApp smallArrayPrimTyCon [elt] +mkMutableArrayPrimTy :: Type -> Type -> Type +mkMutableArrayPrimTy s elt = TyConApp mutableArrayPrimTyCon [s, elt] +mkMutableByteArrayPrimTy :: Type -> Type +mkMutableByteArrayPrimTy s = TyConApp mutableByteArrayPrimTyCon [s] +mkMutableArrayArrayPrimTy :: Type -> Type +mkMutableArrayArrayPrimTy s = TyConApp mutableArrayArrayPrimTyCon [s] +mkSmallMutableArrayPrimTy :: Type -> Type -> Type +mkSmallMutableArrayPrimTy s elt = TyConApp smallMutableArrayPrimTyCon [s, elt] + + +{- ********************************************************************* +* * + The mutable variable type +* * +********************************************************************* -} + +mutVarPrimTyCon :: TyCon +mutVarPrimTyCon = pcPrimTyCon mutVarPrimTyConName [Nominal, Representational] UnliftedRep + +mkMutVarPrimTy :: Type -> Type -> Type +mkMutVarPrimTy s elt = TyConApp mutVarPrimTyCon [s, elt] + +{- +************************************************************************ +* * + The synchronizing variable type +* * +************************************************************************ +-} + +mVarPrimTyCon :: TyCon +mVarPrimTyCon = pcPrimTyCon mVarPrimTyConName [Nominal, Representational] UnliftedRep + +mkMVarPrimTy :: Type -> Type -> Type +mkMVarPrimTy s elt = TyConApp mVarPrimTyCon [s, elt] + +{- +************************************************************************ +* * + The transactional variable type +* * +************************************************************************ +-} + +tVarPrimTyCon :: TyCon +tVarPrimTyCon = pcPrimTyCon tVarPrimTyConName [Nominal, Representational] UnliftedRep + +mkTVarPrimTy :: Type -> Type -> Type +mkTVarPrimTy s elt = TyConApp tVarPrimTyCon [s, elt] + +{- +************************************************************************ +* * + The stable-pointer type +* * +************************************************************************ +-} + +stablePtrPrimTyCon :: TyCon +stablePtrPrimTyCon = pcPrimTyCon stablePtrPrimTyConName [Representational] AddrRep + +mkStablePtrPrimTy :: Type -> Type +mkStablePtrPrimTy ty = TyConApp stablePtrPrimTyCon [ty] + +{- +************************************************************************ +* * + The stable-name type +* * +************************************************************************ +-} + +stableNamePrimTyCon :: TyCon +stableNamePrimTyCon = pcPrimTyCon stableNamePrimTyConName [Phantom] UnliftedRep + +mkStableNamePrimTy :: Type -> Type +mkStableNamePrimTy ty = TyConApp stableNamePrimTyCon [ty] + +{- +************************************************************************ +* * + The Compact NFData (CNF) type +* * +************************************************************************ +-} + +compactPrimTyCon :: TyCon +compactPrimTyCon = pcPrimTyCon0 compactPrimTyConName UnliftedRep + +compactPrimTy :: Type +compactPrimTy = mkTyConTy compactPrimTyCon + +{- +************************************************************************ +* * + The ``bytecode object'' type +* * +************************************************************************ +-} + +-- Unlike most other primitive types, BCO is lifted. This is because in +-- general a BCO may be a thunk for the reasons given in Note [Updatable CAF +-- BCOs] in GHCi.CreateBCO. +bcoPrimTy :: Type +bcoPrimTy = mkTyConTy bcoPrimTyCon +bcoPrimTyCon :: TyCon +bcoPrimTyCon = pcPrimTyCon0 bcoPrimTyConName LiftedRep + +{- +************************************************************************ +* * + The ``weak pointer'' type +* * +************************************************************************ +-} + +weakPrimTyCon :: TyCon +weakPrimTyCon = pcPrimTyCon weakPrimTyConName [Representational] UnliftedRep + +mkWeakPrimTy :: Type -> Type +mkWeakPrimTy v = TyConApp weakPrimTyCon [v] + +{- +************************************************************************ +* * + The ``thread id'' type +* * +************************************************************************ + +A thread id is represented by a pointer to the TSO itself, to ensure +that they are always unique and we can always find the TSO for a given +thread id. However, this has the unfortunate consequence that a +ThreadId# for a given thread is treated as a root by the garbage +collector and can keep TSOs around for too long. + +Hence the programmer API for thread manipulation uses a weak pointer +to the thread id internally. +-} + +threadIdPrimTy :: Type +threadIdPrimTy = mkTyConTy threadIdPrimTyCon +threadIdPrimTyCon :: TyCon +threadIdPrimTyCon = pcPrimTyCon0 threadIdPrimTyConName UnliftedRep + +{- +************************************************************************ +* * +\subsection{SIMD vector types} +* * +************************************************************************ +-} + +#include "primop-vector-tys.hs-incl" |