h*k-g      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~3.0.4(C) 2013 Richard EisenbergBSD-style (see LICENSE) Ryan Scott experimental non-portable Safe-Inferred ()*/016=V8 singletonsThe singleton type for functions. Functions have somewhat special treatment in  singletons (see the Haddocks for (.)9 for more information about this), and as a result, the E instance for 3 is one of the only such instances defined in the  singletons library rather than, say, singletons-base.& singletons Similar to '*, but for two-parameter type constructors.' singletons:Wrapper for converting the normal type-level arrow into a .. For example, given: data Nat = Zero | Succ Nat type family Map (a :: a ~> b) (a :: [a]) :: [b] Map f '[] = '[] Map f (x ': xs) = Apply f x ': Map f xs We can write: #Map (TyCon1 Succ) [Zero, Succ Zero]( singletonsAn "internal" defunctionalization symbol used primarily in the definition of *.3Note that this is only defined on GHC 8.6 or later.) singletonsAn "internal" defunctionalization symbol used primarily in the definition of *, as well as the C instances for ', &, etc.3Note that this is only defined on GHC 8.6 or later.* singletons-An "internal" definition used primary in the - instance for +.0Note that this only defined on GHC 8.6 or later.+ singletonsWorkhorse for the ', etc., types. This can be used directly in place of any of the TyConN$ types, but it will work only with  monomorphic types. When GHC#14645 is fixed, this should fully supersede the TyConN types.Note that this is only defined on GHC 8.6 or later. Prior to GHC 8.6, ' et al.% were defined as separate data types., singletonsAn infix synonym for -- singletonsType level function application. singletonsSomething of kind a . b is a defunctionalized type function that is not necessarily generative or injective. Defunctionalized type functions (also called "defunctionalization symbols") can be partially applied, even if the original type function cannot be. For more information on how this works, see the "Promotion and partial application" section of the  >https://github.com/goldfirere/singletons/blob/master/README.mdREADME.!The singleton for things of kind a . b is . / values can be constructed in one of two ways:  With the singFun* family of combinators (e.g., \ ). For example, if you have: 8 type Id :: a -> a sId :: Sing a -> Sing (Id a) 'Then you can construct a value of type E @(a . a) (that is,  @a @a like so:  sIdFun :: E @(a ./ a) IdSym0 sIdFun = singFun1 @IdSym0 sId Where  IdSym0 :: a . a# is the defunctionlized version of Id.  Using the C class. For example, D @IdSym0 is another way of defining sIdFun above. The  singletons-th% library automatically generates C7 instances for defunctionalization symbols such as IdSym0.Normal type-level arrows (->)3 can be converted into defunctionalization arrows (.) by the use of the +. family of types. (Refer to the Haddocks for ' to see an example of this in practice.) For this reason, we do not make an effort to define defunctionalization symbols for most type constructors of kind a -> b, as they can be used in defunctionalized settings by simply applying TyCon{N} with an appropriate N.This includes the (->), type constructor itself, which is of kind  ->  -> *. One can turn it into something of kind  .  .  by writing & (->), or something of kind  ->  .  by writing ' ((->) t) (where t :: )./ singletonsRepresentation of the kind of a type-level function. The difference between term-level arrows and this type-level arrow is that at the term level applications can be unsaturated, whereas at the type level all applications have to be fully saturated.0 singletonsA 0 wraps up a C instance for explicit handling.3 singletonsThe singleton for 6s. Informally, this is the singleton type for other singletons.6 singletonsA newtype around E.Since E is a type family, it cannot be used directly in type class instances. As one example, one cannot write a catch-all  instance SDecide k =>  TestEquality (E k). On the other hand, 6 is a perfectly ordinary data type, which means that it is quite possible to define an  instance SDecide k =>  TestEquality (6 k).9 singletonsAn existentially-quantified singleton. This type is useful when you want a singleton type, but there is no way of knowing, at compile-time, what the type index will be. To make use of this type, you will generally have to use a pattern-match: foo :: Bool -> ... foo b = case toSing b of SomeSing sb -> {- fancy dependently-typed code with sb -};An example like the one above may be easier to write using m.; singletonsThe ; class is a kind class. It classifies all kinds for which singletons are defined. The class supports converting between a singleton type and the base (unrefined) type which it is built from.For a ; instance to be well behaved, it should obey the following laws: > . = D 9 (\x -> m x =) D  4The final law can also be expressed in terms of the V pattern synonym: (\(V sing) -> V sing) D  < singletons6Get a base type from the promoted kind. For example,  Demote Bool will be the type Bool8. Rarely, the type and kind do not match. For example,  Demote Nat is Natural.= singletons-Convert a singleton to its unrefined version.> singletonsConvert an unrefined type to an existentially-quantified singleton type.? singletonsA version of the C* class lifted to binary type constructors.@ singletonsLift explicit singletons through a binary type constructor. You will likely need the ScopedTypeVariables0 extension to use this method the way you want.A singletonsA version of the C) class lifted to unary type constructors.B singletonsLift an explicit singleton through a unary type constructor. You will likely need the ScopedTypeVariables0 extension to use this method the way you want.C singletonsA C: constraint is essentially an implicitly-passed singleton.In contrast to the ; class, which is parameterized over data types promoted to the kind level, the C class is parameterized over values promoted to the type level. To explain this distinction another way, consider this code: f = fromSing (sing @(T :: K)) Here, f uses methods from both C and ;. However, the shape of each constraint is rather different: using D requires a SingI T constraint, whereas using = requires a  SingKind K constraint.If you need to satisfy this constraint with an explicit singleton, please see l or the W pattern synonym.D singletons;Produce the singleton explicitly. You will likely need the ScopedTypeVariables0 extension to use this method the way you want.E singletons'The singleton kind-indexed type family.F singletons Force GHC to unify the kinds of a and b . Note that  SameKind a b is different from KindOf a ~ KindOf b in that the former makes the kinds unify immediately, whereas the latter is a proposition that GHC considers as possibly false.G singletons=Convenient synonym to refer to the kind of a type variable: type KindOf (a :: k) = kV singletonsAn explicitly bidirectional pattern synonym for going between a singleton and the corresponding demoted term.As an  expression5: this takes a singleton to its demoted (base) type.:t FromSing \@Bool!FromSing \@Bool :: Sing a -> BoolFromSing SFalseFalseAs a pattern8: It extracts a singleton from its demoted (base) type.  singAnd ::  ->  -> 9  singAnd (V singBool1) (V singBool2) = 9 (singBool1 %&& singBool2) instead of writing it with m: singAnd bool1 bool2 = m bool1 $ singBool1 -> m bool2 $ singBool2 -> 9 (singBool1 %&& singBool2) W singletonsAn explicitly bidirectional pattern synonym for implicit singletons.As an  expression: Constructs a singleton Sing a( given a implicit singleton constraint SingI a.As a pattern: Matches on an explicit Sing a witness bringing an implicit SingI a constraint into scope.X singletons.Produce a singleton explicitly using implicit A and C( constraints. You will likely need the ScopedTypeVariables0 extension to use this method the way you want.Y singletons.Produce a singleton explicitly using implicit ? and C( constraints. You will likely need the ScopedTypeVariables0 extension to use this method the way you want.Z singletonsGet an implicit singleton (a C instance) from an explicit one.[ singletonsAn infix synonym for \ singletonsUse this function when passing a function on singletons as a higher-order function. You will need visible type application to get this to work. For example: falses = sMap (singFun1 @NotSym0 sNot) (STrue `SCons` STrue `SCons` SNil)There are a family of  singFun...? functions, keyed by the number of parameters of the function.d singletonsThis is the inverse of \, and likewise for the other  unSingFun... functions.l singletonsConvenience function for creating a context with an implicit singleton available.m singletons Convert a normal datatype (like ) to a singleton for that datatype, passing it into a continuation.n singletonsConvert a group of A and C constraints (representing a function to apply and its argument, respectively) into a single C constraint representing the application. You will likely need the ScopedTypeVariables/ extension to use this method the way you want.o singletonsConvert a group of ? and C constraints (representing a function to apply and its arguments, respectively) into a single C constraint representing the application. You will likely need the ScopedTypeVariables/ extension to use this method the way you want.p singletonsA convenience function useful when we need to name a singleton value multiple times. Without this function, each use of D could potentially refer to a different singleton, and one has to use type signatures (often with ScopedTypeVariables#) to ensure that they are the same.q singletonsA convenience function useful when we need to name a singleton value for a unary type constructor multiple times. Without this function, each use of X could potentially refer to a different singleton, and one has to use type signatures (often with ScopedTypeVariables$) to ensure that they are the same.r singletonsA convenience function useful when we need to name a singleton value for a binary type constructor multiple times. Without this function, each use of X could potentially refer to a different singleton, and one has to use type signatures (often with ScopedTypeVariables$) to ensure that they are the same.s singletonsA convenience function that names a singleton satisfying a certain property. If the singleton does not satisfy the property, then the function returns . The property is expressed in terms of the underlying representation of the singleton.t singletonsA convenience function that names a singleton for a unary type constructor satisfying a certain property. If the singleton does not satisfy the property, then the function returns . The property is expressed in terms of the underlying representation of the singleton.u singletonsA convenience function that names a singleton for a binary type constructor satisfying a certain property. If the singleton does not satisfy the property, then the function returns . The property is expressed in terms of the underlying representation of the singleton.v singletons7Allows creation of a singleton when a proxy is at hand.w singletonsAllows creation of a singleton for a unary type constructor when a proxy is at hand.x singletonsAllows creation of a singleton for a binary type constructor when a proxy is at hand.y singletons&Allows creation of a singleton when a proxy# is at hand.z singletonsAllows creation of a singleton for a unary type constructor when a proxy# is at hand.{ singletonsAllows creation of a singleton for a binary type constructor when a proxy# is at hand.| singletonsA convenience function that takes a type as input and demotes it to its value-level counterpart as output. This uses ; and C behind the scenes, so | = = D.*This function is intended to be used with TypeApplications. For example: demote @TrueTrue#demote @(Nothing :: Maybe Ordering)Nothingdemote @(Just EQ)Just EQdemote @'(True,EQ) (True,EQ)} singletonsA convenience function that takes a unary type constructor and its argument as input, applies them, and demotes the result to its value-level counterpart as output. This uses ;, A, and C behind the scenes, so } = = X.*This function is intended to be used with TypeApplications. For example:demote1 @Just @EQJust EQdemote1 @('(,) True) @EQ (True,EQ)~ singletonsA convenience function that takes a binary type constructor and its arguments as input, applies them, and demotes the result to its value-level counterpart as output. This uses ;, ?, and C behind the scenes, so ~ = = Y.*This function is intended to be used with TypeApplications. For example:demote2 @'(,) @True @EQ (True,EQ) singletonsNote that this instance's >7 implementation crucially relies on the fact that the ; instances for k1 and k2 both satisfy the ; laws. If they don't, > might produce strange results!m singletonsThe original datatype singletonsFunction expecting a singletonE[CDABX?@Y;<=>GF019:ZWlmVnovwx|}~yz{pqrstu6783452/.'&%$#"! -,+*)(\]^_`abcdefghijkTURSPQNOLMJKHI E[CDABX?@Y;<=>GF019:ZWlmVnovwx|}~yz{pqrstu6783452/.'&%$#"! -,+*)(\]^_`abcdefghijkTURSPQNOLMJKHI  9 9 9 0 0 0,9 .0[9 (C) 2013 Richard EisenbergBSD-style (see LICENSE) Ryan Scott experimental non-portable Safe-Inferred)*01B singletonsMembers of the  "kind" class support decidable equality. Instances of this class are generated alongside singleton definitions for datatypes that derive an  instance. singletons>Compute a proof or disproof of equality, given two singletons. singletonsA  about a type a0 is either a proof of existence or a proof that a cannot exist. singletons Witness for a singletonsProof that no a exists singletons,Because we can never create a value of type ", a function that type-checks at  a -> Void shows that objects of type a% can never exist. Thus, we say that a is  singletons&A suitable default implementation for  that leverages . singletons&A suitable default implementation for  that leverages .  4(C) 2017 Ryan ScottBSD-style (see LICENSE) Ryan Scott experimental non-portable Safe-Inferred016_& singletonsThe workhorse that powers . The only reason that  exists is to work around GHC's inability to put type families in the head of a quantified constraint (see  /https://gitlab.haskell.org/ghc/ghc/issues/14860this GHC issue for more details on this point). In other words, GHC will not let you define  like so: class (forall (z :: k).  (E z)) =>  k  By replacing  (E z) with  ShowSing' z;, we are able to avoid this restriction for the most part.The superclass of  is a bit peculiar: *class (forall (sing :: k -> Type). sing ~ E =>  (sing z)) =>  (z :: k) One might wonder why this superclass is used instead of this seemingly more direct equivalent: class  (E z) =>  (z :: k) Actually, these aren't equivalent! The latter's superclass mentions a type family in its head, and this gives GHC's constraint solver trouble when trying to match this superclass against other constraints. (See the discussion beginning at  =https://gitlab.haskell.org/ghc/ghc/-/issues/16365#note_189057 for more on this point). The former's superclass, on the other hand, does not mention a type family in its head, which allows it to match other constraints more easily. It may sound like a small difference, but it's the only reason that  is able to work at all without a significant amount of additional workarounds.The quantified superclass has one major downside. Although the head of the quantified superclass is more eager to match, which is usually a good thing, it can bite under certain circumstances. Because  (sing z) will match a  instance for any types sing :: k -> Type and z :: k , (where k is a kind variable), it is possible for GHC's constraint solver to get into a situation where multiple instances match  (sing z), and GHC will get confused as a result. Consider this example:  -- As in Data.Singletons newtype 6 :: forall k. k -> Type where 7 :: forall k (a :: k). { 8 :: E a } -> 6 a instance  k =>  (6 (a :: k)) where  _ s = : "WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}' When typechecking the  instance for 6), GHC must fill in a default definition  = defaultShow , where defaultShow ::  (6 a) => 6 a -> . GHC's constraint solver has two possible ways to satisfy the  (6 a) constraint for  defaultShow: 'The top-level instance declaration for  (6 (a :: k)) itself, and (sing (z :: k))= from the head of the quantified constraint arising from  k.In practice, GHC will choose (2), as local quantified constraints shadow global constraints. This confuses GHC greatly, causing it to error out with an error akin to )Couldn't match type Sing with WrappedSing. See  1https://gitlab.haskell.org/ghc/ghc/-/issues/17934$ for a full diagnosis of the issue.The bad news is that because of GHC#17934, we have to manually define  (and  ) in the  instance for 6 in order to avoid confusing GHC's constraint solver. In other words,  deriving  is a no-go for 6(. The good news is that situations like 6! are quite rare in the world of  singletons@most of the time, # instances for singleton types do not have the shape  (sing (z :: k)), where k is a polymorphic kind variable. Rather, most such instances instantiate k to a specific kind (e.g., Bool, or [a]), which means that they will not overlap the head of the quantified superclass in  as observed above.,Note that we define the single instance for  without the use of a quantified constraint in the instance context:  instance  (E z) =>  (z :: k) We could define this instance with a quantified constraint in the instance context, and it would be equally as expressive. But it doesn't provide any additional functionality that the non-quantified version gives, so we opt for the non-quantified version, which is easier to read. singletons8In addition to the promoted and singled versions of the  class that singletons-base< provides, it is also useful to be able to directly define  instances for singleton types themselves. Doing so is almost entirely straightforward, as a derived  instance does 90 percent of the work. The last 10 percent@getting the right instance context@is a bit tricky, and that's where  comes into play.As an example, let's consider the singleton type for lists. We want to write an instance with the following shape: instance ??? =>  (SList! (z :: [k])) where showsPrec p SNil$ = showString "SNil" showsPrec p (SCons sx sxs) = showParen (p > 10) $ showString "SCons " . showsPrec 11 sx . showSpace . showsPrec 11 sxs )To figure out what should go in place of ???=, observe that we require the type of each field to also be 4 instances. In other words, we need something like ( (E (a :: k)))4. But this isn't quite right, as the type variable a4 doesn't appear in the instance head. In fact, this a type is really referring to an existentially quantified type variable in the SCons constructor, so it doesn't make sense to try and use it like this. Luckily, the QuantifiedConstraints language extension provides a solution to this problem. This lets you write a context of the form  (forall a.  (E (a :: k)))/, which demands that there be an instance for  (E (a :: k))" that is parametric in the use of a/. This lets us write something closer to this: instance (forall a.  (E (a :: k))) => SList (E (z :: [k])) where ... The ! class is a thin wrapper around  (forall a.  (E (a :: k))). With /, our final instance declaration becomes this:  instance  k =>  (SList (z :: [k])) where ... &In fact, this instance can be derived: deriving instance  k =>  (SList (z :: [k])) $(Note that the actual definition of  is slightly more complicated than what this documentation might suggest. For the full story, refer to the documentation for .)When singling a derived  instance,  singletons-th will also generate a 5 instance for the corresponding singleton type using . In other words, if you give  singletons-th a derived 8 instance, then you'll receive the following in return: A promoted (PShow ) instance A singled (SShow ) instanceA  instance for the singleton typeWhat a bargain!(C) 2017 Ryan ScottBSD-style (see LICENSE) Ryan Scott experimental non-portable Safe-Inferred)*01f singletons3Project the second element out of a dependent pair. singletons2Project the first element out of a dependent pair. singletonsUnicode shorthand for . singletonsThe singleton type for . singletonsUnicode shorthand for . singletonsA dependent pair. singletons2Project the first element out of a dependent pair. singletons3Project the second element out of a dependent pair. singletonsProject the first element out of a dependent pair using continuation-passing style. singletonsProject the second element out of a dependent pair using continuation-passing style. singletons Map across a  value in a dependent fashion. singletonsZip two ( values together in a dependent fashion. singletons!Convert an uncurried function on  to a curried one. Together,  and  witness an isomorphism such that the following identities hold: 'id1 :: forall a (b :: a ~> Type) (c :: 0 a b ~> Type). (forall (p :: Sigma a b).  p -> c @% p) -> (forall (p :: Sigma a b).  p -> c  p) id1 f =  a b c ( a b -c f) id2 :: forall a (b :: a ~> Type) (c :: > a b ~> Type). (forall (x :: a) (sx :: Sing x) (y :: b  x). Sing (7 sx) -> Sing y -> c < (sx :&: y)) -> (forall (x :: a) (sx :: Sing x) (y :: b  x). Sing (7 sx) -> Sing y -> c  (sx :&: y)) id2 f =  a b c ( a b @c f)  singletonsConvert a curried function on  to an uncurried one. Together,  and : witness an isomorphism. (Refer to the documentation for  for more details.)EE44         !"#$%&&'()*+,-./01234567889:;<=>?@@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\K]^_4`abcdefghijklmnopqrstuvwxyz{|}~ 'singletons-3.0.4-3NvjhAEqkbIFt608Q1zd58Data.Singletons.DecideData.SingletonsData.Singletons.ShowSingData.Singletons.Sigma singletonsbaseGHC.BaseVoidData.Type.Equality:~:Refl Data.ProxyProxy@@@#@$$$@@@#@$$@@@#@$ ApplySym2 ApplySym1 ApplySym0~>@#@$$$~>@#@$$~>@#@$ KindOfSym1 KindOfSym0 SameKindSym2 SameKindSym1 SameKindSym0 DemoteSym1 DemoteSym0 SingFunction8 SingFunction7 SingFunction6 SingFunction5 SingFunction4 SingFunction3 SingFunction2 SingFunction1SLambda applySingTyCon8TyCon7TyCon6TyCon5TyCon4TyCon3TyCon2TyCon1ApplyTyConAux2ApplyTyConAux1 ApplyTyConTyCon@@Apply~>TyFun SingInstance UnwrapSing SWrappedSing SWrapSing sUnwrapSing WrappedSingWrapSing unwrapSingSomeSingSingKindDemotefromSingtoSingSingI2 liftSing2SingI1liftSingSingIsingSingSameKindKindOfSLambda8 applySing8SLambda7 applySing7SLambda6 applySing6SLambda5 applySing5SLambda4 applySing4SLambda3 applySing3SLambda2 applySing2FromSingsing1sing2 singInstancesingFun1singFun2singFun3singFun4singFun5singFun6singFun7singFun8 unSingFun1 unSingFun2 unSingFun3 unSingFun4 unSingFun5 unSingFun6 unSingFun7 unSingFun8 withSingI withSomeSing usingSingI1 usingSingI2withSing withSing1 withSing2singThat singThat1 singThat2 singByProxy singByProxy1 singByProxy2 singByProxy# singByProxy1# singByProxy2#demotedemote1demote2$fSingIWrappedSingWrapSing$fSingKindWrappedSing$fSingIFUNTyCon$fSingIFUNTyCon0$fSingIFUNTyCon1$fSingIFUNTyCon2$fSingIFUNTyCon3$fSingIFUNTyCon4$fSingIFUNTyCon5$fSingIFUNTyCon6 $fSingKindFUNSDecide%~DecisionProved DisprovedRefuteddecideEqualitydecideCoercion$fTestCoercionkWrappedSing$fTestEqualitykWrappedSing ShowSing'ShowSing $fShowSing'kz$fShowWrappedSing $fShowSingk$fShowSWrappedSingShowSingApply' ShowSingApply ShowApply' ShowApplySndSigmaFstSigmaSΣSSigma:%&:ΣSigma:&:fstSigmasndSigma projSigma1 projSigma2mapSigmazipSigma currySigma uncurrySigma$fSingISigma:&:$fShowApply'afx $fShowApplyaf $fShowSigma$fShowSingApply'afxz$fShowSingApplyaf $fShowSSigmaghc-prim GHC.TypesTypeidBool GHC.MaybeNothing GHC.ClassesEq testEqualityData.Type.Coercion testCoercionGHC.ShowShow showsPrec showStringshowStringshowList