Use TypeLits in the meta-data encoding of GHC.Generics
[ghc.git] / libraries / base / GHC / Generics.hs
index 3e38930..43b210d 100644 (file)
@@ -1,10 +1,17 @@
 {-# LANGUAGE Trustworthy            #-}
 {-# LANGUAGE CPP                    #-}
 {-# LANGUAGE NoImplicitPrelude      #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE TypeSynonymInstances   #-}
 {-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE MagicHash              #-}
 {-# LANGUAGE KindSignatures         #-}
 {-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE StandaloneDeriving     #-}
 {-# LANGUAGE DeriveGeneric          #-}
 {-# LANGUAGE PolyKinds              #-}
@@ -13,7 +20,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.Generics
--- Copyright   :  (c) Universiteit Utrecht 2010-2011, University of Oxford 2012-2013
+-- Copyright   :  (c) Universiteit Utrecht 2010-2011, University of Oxford 2012-2014
 -- License     :  see libraries/base/LICENSE
 --
 -- Maintainer  :  libraries@haskell.org
@@ -66,14 +73,14 @@ module GHC.Generics  (
 -- @
 -- instance 'Generic' (Tree a) where
 --   type 'Rep' (Tree a) =
---     'D1' D1Tree
---       ('C1' C1_0Tree
---          ('S1' 'NoSelector' ('Par0' a))
+--     'D1' ('MetaData \"Tree\" \"Main\" \"package-name\" 'False)
+--       ('C1' ('MetaCons \"Leaf\" 'PrefixI 'False)
+--          ('S1' 'MetaNoSel ('Rec0' a))
 --        ':+:'
---        'C1' C1_1Tree
---          ('S1' 'NoSelector' ('Rec0' (Tree a))
+--        'C1' ('MetaCons \"Node\" 'PrefixI 'False)
+--          ('S1' 'MetaNoSel ('Rec0' (Tree a))
 --           ':*:'
---           'S1' 'NoSelector' ('Rec0' (Tree a))))
+--           'S1' 'MetaNoSel ('Rec0' (Tree a))))
 --   ...
 -- @
 --
@@ -81,11 +88,6 @@ module GHC.Generics  (
 -- the @-ddump-deriv@ flag. In GHCi, you can expand a type family such as 'Rep' using
 -- the @:kind!@ command.
 --
-#if 0
--- /TODO:/ Newer GHC versions abandon the distinction between 'Par0' and 'Rec0' and will
--- use 'Rec0' everywhere.
---
-#endif
 -- This is a lot of information! However, most of it is actually merely meta-information
 -- that makes names of datatypes and constructors and more available on the type level.
 --
@@ -95,7 +97,7 @@ module GHC.Generics  (
 -- @
 -- instance 'Generic' (Tree a) where
 --   type 'Rep' (Tree a) =
---     'Par0' a
+--     'Rec0' a
 --     ':+:'
 --     ('Rec0' (Tree a) ':*:' 'Rec0' (Tree a))
 -- @
@@ -104,7 +106,7 @@ module GHC.Generics  (
 -- is combined using the binary type constructor ':+:'.
 --
 -- The first constructor consists of a single field, which is the parameter @a@. This is
--- represented as @'Par0' a@.
+-- represented as @'Rec0' a@.
 --
 -- The second constructor consists of two fields. Each is a recursive field of type @Tree a@,
 -- represented as @'Rec0' (Tree a)@. Representations of individual fields are combined using
@@ -112,22 +114,24 @@ module GHC.Generics  (
 --
 -- Now let us explain the additional tags being used in the complete representation:
 --
---    * The @'S1' 'NoSelector'@ indicates that there is no record field selector associated with
---      this field of the constructor.
+--    * The @'S1' 'MetaNoSel@ indicates that there is no record field selector
+--      associated with this field of the constructor.
 --
---    * The @'C1' C1_0Tree@ and @'C1' C1_1Tree@ invocations indicate that the enclosed part is
+--    * The @'C1' ('MetaCons \"Leaf\" 'PrefixI 'False)@ and
+--      @'C1' ('MetaCons \"Node\" 'PrefixI 'False)@ invocations indicate that the enclosed part is
 --      the representation of the first and second constructor of datatype @Tree@, respectively.
---      Here, @C1_0Tree@ and @C1_1Tree@ are datatypes generated by the compiler as part of
---      @deriving 'Generic'@. These datatypes are proxy types with no values. They are useful
---      because they are instances of the type class 'Constructor'. This type class can be used
---      to obtain information about the constructor in question, such as its name
---      or infix priority.
---
---    * The @'D1' D1Tree@ tag indicates that the enclosed part is the representation of the
---      datatype @Tree@. Again, @D1Tree@ is a datatype generated by the compiler. It is a
---      proxy type, and is useful by being an instance of class 'Datatype', which
---      can be used to obtain the name of a datatype, the module it has been defined in, and
---      whether it has been defined using @data@ or @newtype@.
+--      Here, the meta-information regarding constructor names, fixity and whether
+--      it has named fields or not is encoded at the type level. The @'MetaCons@
+--      type is also an instance of the type class 'Constructor'. This type class can be used
+--      to obtain information about the constructor at the value level.
+--
+--    * The @'D1' ('MetaData \"Tree\" \"Main\" \"package-name\" 'False)@ tag
+--      indicates that the enclosed part is the representation of the
+--      datatype @Tree@. Again, the meta-information is encoded at the type level.
+--      The @'MetaData@ type is an instance of class 'Datatype', which
+--      can be used to obtain the name of a datatype, the module it has been
+--      defined in, the package it is located under, and whether it has been
+--      defined using @data@ or @newtype@ at the value level.
 
 -- ** Derived and fundamental representation types
 --
@@ -144,14 +148,16 @@ module GHC.Generics  (
 --
 -- |
 --
--- The type constructors 'Par0' and 'Rec0' are variants of 'K1':
+-- The type constructor 'Rec0' is a variant of 'K1':
 --
 -- @
--- type 'Par0' = 'K1' 'P'
 -- type 'Rec0' = 'K1' 'R'
 -- @
 --
--- Here, 'P' and 'R' are type-level proxies again that do not have any associated values.
+-- Here, 'R' is a type-level proxy that does not have any associated values.
+--
+-- There used to be another variant of 'K1' (namely 'Par0'), but it has since
+-- been deprecated.
 
 -- *** Meta information: 'M1'
 --
@@ -189,7 +195,8 @@ module GHC.Generics  (
 --
 -- @
 -- instance 'Generic' Empty where
---   type 'Rep' Empty = 'D1' D1Empty 'V1'
+--   type 'Rep' Empty =
+--     'D1' ('MetaData \"Empty\" \"Main\" \"package-name\" 'False) 'V1'
 -- @
 
 -- **** Constructors without fields: 'U1'
@@ -202,8 +209,8 @@ module GHC.Generics  (
 -- @
 -- instance 'Generic' Bool where
 --   type 'Rep' Bool =
---     'D1' D1Bool
---       ('C1' C1_0Bool 'U1' ':+:' 'C1' C1_1Bool 'U1')
+--     'D1' ('MetaData \"Bool\" \"Data.Bool\" \"package-name\" 'False)
+--       ('C1' ('MetaCons \"False\" 'PrefixI 'False) 'U1' ':+:' 'C1' ('MetaCons \"True\" 'PrefixI 'False) 'U1')
 -- @
 
 -- *** Representation of types with many constructors or many fields
@@ -450,17 +457,19 @@ module GHC.Generics  (
 --
 -- The above declaration causes the following representation to be generated:
 --
+-- @
 -- instance 'Generic1' Tree where
 --   type 'Rep1' Tree =
---     'D1' D1Tree
---       ('C1' C1_0Tree
---          ('S1' 'NoSelector' 'Par1')
+--     'D1' ('MetaData \"Tree\" \"Main\" \"package-name\" 'False)
+--       ('C1' ('MetaCons \"Leaf\" 'PrefixI 'False)
+--          ('S1' 'MetaNoSel 'Par1')
 --        ':+:'
---        'C1' C1_1Tree
---          ('S1' 'NoSelector' ('Rec1' Tree)
+--        'C1' ('MetaCons \"Node\" 'PrefixI 'False)
+--          ('S1' 'MetaNoSel ('Rec1' Tree)
 --           ':*:'
---           'S1' 'NoSelector' ('Rec1' Tree)))
+--           'S1' 'MetaNoSel ('Rec1' Tree)))
 --   ...
+--  @
 --
 -- The representation reuses 'D1', 'C1', 'S1' (and thereby 'M1') as well
 -- as ':+:' and ':*:' from 'Rep'. (This reusability is the reason that we
@@ -476,7 +485,7 @@ module GHC.Generics  (
 --
 -- |
 --
--- Unlike 'Par0' and 'Rec0', the 'Par1' and 'Rec1' type constructors do not
+-- Unlike 'Rec0', the 'Par1' and 'Rec1' type constructors do not
 -- map to 'K1'. They are defined directly, as follows:
 --
 -- @
@@ -502,11 +511,11 @@ module GHC.Generics  (
 -- @
 -- class 'Rep1' WithInt where
 --   type 'Rep1' WithInt =
---     'D1' D1WithInt
---       ('C1' C1_0WithInt
---         ('S1' 'NoSelector' ('Rec0' Int)
+--     'D1' ('MetaData \"WithInt\" \"Main\" \"package-name\" 'False)
+--       ('C1' ('MetaCons \"WithInt\" 'PrefixI 'False)
+--         ('S1' 'MetaNoSel ('Rec0' Int)
 --          ':*:'
---          'S1' 'NoSelector' 'Par1'))
+--          'S1' 'MetaNoSel 'Par1'))
 -- @
 --
 -- If the parameter @a@ appears underneath a composition of other type constructors,
@@ -521,11 +530,11 @@ module GHC.Generics  (
 -- @
 -- class 'Rep1' Rose where
 --   type 'Rep1' Rose =
---     'D1' D1Rose
---       ('C1' C1_0Rose
---         ('S1' 'NoSelector' 'Par1'
+--     'D1' ('MetaData \"Rose\" \"Main\" \"package-name\" 'False)
+--       ('C1' ('MetaCons \"Fork\" 'PrefixI 'False)
+--         ('S1' 'MetaNoSel 'Par1'
 --          ':*:'
---          'S1' 'NoSelector' ([] ':.:' 'Rec1' Rose)
+--          'S1' 'MetaNoSel ([] ':.:' 'Rec1' Rose)
 -- @
 --
 -- where
@@ -585,9 +594,9 @@ module GHC.Generics  (
 -- @
 -- instance 'Generic' IntHash where
 --   type 'Rep' IntHash =
---     'D1' D1IntHash
---       ('C1' C1_0IntHash
---         ('S1' 'NoSelector' 'UInt'))
+--     'D1' ('MetaData \"IntHash\" \"Main\" \"package-name\" 'False)
+--       ('C1' ('MetaCons \"IntHash\" 'PrefixI 'False)
+--         ('S1' 'MetaNoSel 'UInt'))
 -- @
 --
 -- Currently, only the six unlifted types listed above are generated, but this
@@ -614,12 +623,13 @@ module GHC.Generics  (
   , type UFloat, type UInt, type UWord
 
   -- ** Synonyms for convenience
-  , Rec0, Par0, R, P
+  , Rec0, R
   , D1, C1, S1, D, C, S
 
   -- * Meta-information
   , Datatype(..), Constructor(..), Selector(..), NoSelector
-  , Fixity(..), Associativity(..), Arity(..), prec
+  , Fixity(..), FixityI(..), Associativity(..), prec
+  , Meta(..)
 
   -- * Generic type classes
   , Generic(..), Generic1(..)
@@ -627,17 +637,21 @@ module GHC.Generics  (
   ) where
 
 -- We use some base types
+import GHC.Integer ( Integer, integerToInt )
 import GHC.Prim ( Addr#, Char#, Double#, Float#, Int#, Word# )
 import GHC.Ptr ( Ptr )
 import GHC.Types
-import Data.Maybe ( Maybe(..) )
+import Data.Maybe  ( Maybe(..) )
 import Data.Either ( Either(..) )
 
 -- Needed for instances
 import GHC.Classes ( Eq, Ord )
-import GHC.Read ( Read )
-import GHC.Show ( Show )
-import Data.Proxy
+import GHC.Read    ( Read )
+import GHC.Show    ( Show )
+
+-- Needed for metadata
+import Data.Proxy   ( Proxy(..), KProxy(..) )
+import GHC.TypeLits ( Nat, Symbol, KnownSymbol, KnownNat, symbolVal, natVal )
 
 --------------------------------------------------------------------------------
 -- Representation types
@@ -663,7 +677,7 @@ newtype K1 (i :: *) c (p :: *) = K1 { unK1 :: c }
   deriving (Eq, Ord, Read, Show, Generic)
 
 -- | Meta-information (constructor names, etc.)
-newtype M1 (i :: *) (c :: *) f (p :: *) = M1 { unM1 :: f p }
+newtype M1 (i :: *) (c :: Meta) f (p :: *) = M1 { unM1 :: f p }
   deriving (Eq, Ord, Read, Show, Generic)
 
 -- | Sums: encode choice between constructors
@@ -723,15 +737,9 @@ type UWord   = URec Word
 
 -- | Tag for K1: recursion (of kind *)
 data R
--- | Tag for K1: parameters (other than the last)
-data P
 
 -- | Type synonym for encoding recursion (of kind *)
 type Rec0  = K1 R
--- | Type synonym for encoding parameters (other than the last)
-type Par0  = K1 P
-{-# DEPRECATED Par0 "'Par0' is no longer used; use 'Rec0' instead" #-} -- deprecated in 7.6
-{-# DEPRECATED P "'P' is no longer used; use 'R' instead" #-} -- deprecated in 7.6
 
 -- | Tag for M1: datatype
 data D
@@ -750,51 +758,51 @@ type C1 = M1 C
 type S1 = M1 S
 
 -- | Class for datatypes that represent datatypes
-class Datatype (d :: *) where
+class Datatype d where
   -- | The name of the datatype (unqualified)
-  datatypeName :: t d (f :: * -> *) (a :: *) -> [Char]
+  datatypeName :: t d (f :: * -> *) a -> [Char]
   -- | The fully-qualified name of the module where the type is declared
-  moduleName   :: t d (f :: * -> *) (a :: *) -> [Char]
+  moduleName   :: t d (f :: * -> *) a -> [Char]
   -- | The package name of the module where the type is declared
-  packageName :: t d (f :: * -> *) (a :: *) -> [Char]
+  packageName :: t d (f :: * -> *) a -> [Char]
   -- | Marks if the datatype is actually a newtype
-  isNewtype    :: t d (f :: * -> *) (a :: *) -> Bool
+  isNewtype    :: t d (f :: * -> *) a -> Bool
   isNewtype _ = False
 
-
--- | Class for datatypes that represent records
-class Selector (s :: *) where
-  -- | The name of the selector
-  selName :: t s (f :: * -> *) (a :: *) -> [Char]
-
--- | Used for constructor fields without a name
-data NoSelector
-
-instance Selector NoSelector where selName _ = ""
+instance (KnownSymbol n, KnownSymbol m, KnownSymbol p, SingI nt)
+    => Datatype ('MetaData n m p nt) where
+  datatypeName _ = symbolVal (Proxy :: Proxy n)
+  moduleName   _ = symbolVal (Proxy :: Proxy m)
+  packageName  _ = symbolVal (Proxy :: Proxy p)
+  isNewtype    _ = fromSing  (sing  :: Sing nt)
 
 -- | Class for datatypes that represent data constructors
-class Constructor (c :: *) where
+class Constructor c where
   -- | The name of the constructor
-  conName :: t c (f :: * -> *) (a :: *) -> [Char]
+  conName :: t c (f :: * -> *) a -> [Char]
 
   -- | The fixity of the constructor
-  conFixity :: t c (f :: * -> *) (a :: *) -> Fixity
+  conFixity :: t c (f :: * -> *) a -> Fixity
   conFixity _ = Prefix
 
   -- | Marks if this constructor is a record
-  conIsRecord :: t c (f :: * -> *) (a :: *) -> Bool
+  conIsRecord :: t c (f :: * -> *) a -> Bool
   conIsRecord _ = False
 
-
--- | Datatype to represent the arity of a tuple.
-data Arity = NoArity | Arity Int
-  deriving (Eq, Show, Ord, Read, Generic)
+instance (KnownSymbol n, SingI f, SingI r)
+    => Constructor ('MetaCons n f r) where
+  conName     _ = symbolVal (Proxy :: Proxy n)
+  conFixity   _ = fromSing  (sing  :: Sing f)
+  conIsRecord _ = fromSing  (sing  :: Sing r)
 
 -- | Datatype to represent the fixity of a constructor. An infix
 -- | declaration directly corresponds to an application of 'Infix'.
 data Fixity = Prefix | Infix Associativity Int
   deriving (Eq, Show, Ord, Read, Generic)
 
+-- | This variant of 'Fixity' appears at the type level.
+data FixityI = PrefixI | InfixI Associativity Nat
+
 -- | Get the precedence of a fixity value.
 prec :: Fixity -> Int
 prec Prefix      = 10
@@ -806,6 +814,23 @@ data Associativity = LeftAssociative
                    | NotAssociative
   deriving (Eq, Show, Ord, Read, Generic)
 
+-- | Class for datatypes that represent records
+class Selector s where
+  -- | The name of the selector
+  selName :: t s (f :: * -> *) a -> [Char]
+
+-- | Used for constructor fields without a name
+-- Deprecated in 7.9
+{-# DEPRECATED NoSelector "'NoSelector' is no longer used" #-}
+data NoSelector
+instance Selector NoSelector        where selName _ = ""
+
+instance (KnownSymbol s) => Selector ('MetaSel s) where
+  selName _ = symbolVal (Proxy :: Proxy s)
+
+instance Selector 'MetaNoSel where
+  selName _ = ""
+
 -- | Representable types of kind *.
 -- This class is derivable in GHC with the DeriveGeneric flag on.
 class Generic a where
@@ -827,15 +852,39 @@ class Generic1 f where
   -- | Convert from the representation to the datatype
   to1    :: (Rep1 f) a -> f a
 
+--------------------------------------------------------------------------------
+-- Meta-data
+--------------------------------------------------------------------------------
+
+-- | Datatype to represent metadata associated with a datatype (@MetaData@),
+-- constructor (@MetaCons@), or field (@MetaSel@ and @MetaNoSel@).
+--
+-- * In @MetaData n m p nt@, @n@ is the datatype's name, @m@ is the module in
+--   which the datatype is defined, @p@ is the package in which the datatype
+--   is defined, and @nt@ is @'True@ if the datatype is a @newtype@.
+--
+-- * In @MetaCons n f s@, @n@ is the constructor's name, @f@ is its fixity,
+--   and @s@ is @'True@ if the constructor contains record selectors.
+--
+-- * Fields with record selectors are tagged with @MetaSel s@, where @s@ is
+--   the record selector name.
+--
+-- * Fields without record selectors are tagged with @MetaNoSel@.
+data Meta = MetaData Symbol Symbol Symbol Bool
+          | MetaCons Symbol FixityI Bool
+          | MetaSel  Symbol
+          | MetaNoSel
 
 --------------------------------------------------------------------------------
 -- Derived instances
 --------------------------------------------------------------------------------
+
 deriving instance Generic [a]
 deriving instance Generic (Maybe a)
 deriving instance Generic (Either a b)
 deriving instance Generic Bool
 deriving instance Generic Ordering
+deriving instance Generic (Proxy t)
 deriving instance Generic ()
 deriving instance Generic ((,) a b)
 deriving instance Generic ((,,) a b c)
@@ -847,6 +896,7 @@ deriving instance Generic ((,,,,,,) a b c d e f g)
 deriving instance Generic1 []
 deriving instance Generic1 Maybe
 deriving instance Generic1 (Either a)
+deriving instance Generic1 Proxy
 deriving instance Generic1 ((,) a)
 deriving instance Generic1 ((,,) a b)
 deriving instance Generic1 ((,,,) a b c)
@@ -855,78 +905,70 @@ deriving instance Generic1 ((,,,,,) a b c d e)
 deriving instance Generic1 ((,,,,,,) a b c d e f)
 
 --------------------------------------------------------------------------------
--- Primitive representations
+-- Copied from the singletons package
 --------------------------------------------------------------------------------
 
--- Int
-data D_Int
-data C_Int
-
-instance Datatype D_Int where
-  datatypeName _ = "Int"
-  moduleName   _ = "GHC.Int"
-  packageName  _ = "base"
-
-instance Constructor C_Int where
-  conName _ = "" -- JPM: I'm not sure this is the right implementation...
-
-instance Generic Int where
-  type Rep Int = D1 D_Int (C1 C_Int (S1 NoSelector (Rec0 Int)))
-  from x = M1 (M1 (M1 (K1 x)))
-  to (M1 (M1 (M1 (K1 x)))) = x
-
-
--- Float
-data D_Float
-data C_Float
-
-instance Datatype D_Float where
-  datatypeName _ = "Float"
-  moduleName   _ = "GHC.Float"
-  packageName  _ = "base"
-
-instance Constructor C_Float where
-  conName _ = "" -- JPM: I'm not sure this is the right implementation...
-
-instance Generic Float where
-  type Rep Float = D1 D_Float (C1 C_Float (S1 NoSelector (Rec0 Float)))
-  from x = M1 (M1 (M1 (K1 x)))
-  to (M1 (M1 (M1 (K1 x)))) = x
-
-
--- Double
-data D_Double
-data C_Double
-
-instance Datatype D_Double where
-  datatypeName _ = "Double"
-  moduleName   _ = "GHC.Float"
-  packageName  _ = "base"
-
-instance Constructor C_Double where
-  conName _ = "" -- JPM: I'm not sure this is the right implementation...
-
-instance Generic Double where
-  type Rep Double = D1 D_Double (C1 C_Double (S1 NoSelector (Rec0 Double)))
-  from x = M1 (M1 (M1 (K1 x)))
-  to (M1 (M1 (M1 (K1 x)))) = x
-
-
--- Char
-data D_Char
-data C_Char
-
-instance Datatype D_Char where
-  datatypeName _ = "Char"
-  moduleName   _ = "GHC.Base"
-  packageName  _ = "base"
-
-instance Constructor C_Char where
-  conName _ = "" -- JPM: I'm not sure this is the right implementation...
-
-instance Generic Char where
-  type Rep Char = D1 D_Char (C1 C_Char (S1 NoSelector (Rec0 Char)))
-  from x = M1 (M1 (M1 (K1 x)))
-  to (M1 (M1 (M1 (K1 x)))) = x
-
-deriving instance Generic (Proxy t)
+-- | The singleton kind-indexed data family.
+data family Sing (a :: k)
+
+-- | A 'SingI' constraint is essentially an implicitly-passed singleton.
+-- If you need to satisfy this constraint with an explicit singleton, please
+-- see 'withSingI'.
+class SingI (a :: k) where
+  -- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@
+  -- extension to use this method the way you want.
+  sing :: Sing a
+
+-- | The 'SingKind' class is essentially 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.
+class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
+  -- | Get a base type from a proxy for the promoted kind. For example,
+  -- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.
+  type DemoteRep kparam :: *
+
+  -- | Convert a singleton to its unrefined version.
+  fromSing :: Sing (a :: k) -> DemoteRep kparam
+
+-- Singleton booleans
+data instance Sing (a :: Bool) where
+  STrue  :: Sing 'True
+  SFalse :: Sing 'False
+
+instance SingI 'True  where sing = STrue
+instance SingI 'False where sing = SFalse
+
+instance SingKind ('KProxy :: KProxy Bool) where
+  type DemoteRep ('KProxy :: KProxy Bool) = Bool
+  fromSing STrue  = True
+  fromSing SFalse = False
+
+-- Singleton Fixity
+data instance Sing (a :: FixityI) where
+  SPrefix :: Sing 'PrefixI
+  SInfix  :: Sing a -> Integer -> Sing ('InfixI a n)
+
+instance SingI 'PrefixI where sing = SPrefix
+instance (SingI a, KnownNat n) => SingI ('InfixI a n) where
+  sing = SInfix (sing :: Sing a) (natVal (Proxy :: Proxy n))
+
+instance SingKind ('KProxy :: KProxy FixityI) where
+  type DemoteRep ('KProxy :: KProxy FixityI) = Fixity
+  fromSing SPrefix      = Prefix
+  fromSing (SInfix a n) = Infix (fromSing a) (I# (integerToInt n))
+
+-- Singleton Associativity
+data instance Sing (a :: Associativity) where
+  SLeftAssociative  :: Sing 'LeftAssociative
+  SRightAssociative :: Sing 'RightAssociative
+  SNotAssociative   :: Sing 'NotAssociative
+
+instance SingI 'LeftAssociative  where sing = SLeftAssociative
+instance SingI 'RightAssociative where sing = SRightAssociative
+instance SingI 'NotAssociative   where sing = SNotAssociative
+
+instance SingKind ('KProxy :: KProxy Associativity) where
+  type DemoteRep ('KProxy :: KProxy Associativity) = Associativity
+  fromSing SLeftAssociative  = LeftAssociative
+  fromSing SRightAssociative = RightAssociative
+  fromSing SNotAssociative   = NotAssociative