    {-|
    Copyright  :  (C) 2016     , University of Twente,
                      2017-2018, QBayLogic B.V.,
                      2017     , Google Inc.
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

    Some \"magic\" classes and instances to get the "GHC.TypeLits.KnownNat.Solver"
    type checker plugin working.

    = Usage

    Let's say you defined a closed type family @Max@:

    @
    import Data.Type.Bool (If)
    import GHC.TypeLits

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a
    @

    if you then want the "GHC.TypeLits.KnownNat.Solver" to solve 'KnownNat'
    constraints over @Max@, given just 'KnownNat' constraints for the arguments
    of @Max@, then you must define:

    @
    \{\-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,
                 MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,
                 TypeApplications, TypeFamilies, TypeOperators,
                 UndecidableInstances \#-\}

    import Data.Proxy            (Proxy (..))
    import GHC.TypeLits.KnownNat

    instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where
      natSing2 = let x = natVal (Proxy @a)
                     y = natVal (Proxy @b)
                     z = max x y
                 in  'SNatKn' z
      \{\-# INLINE natSing2 \#-\}
    @

    = FAQ

    ==== 1. "GHC.TypeLits.KnownNat.Solver" does not seem to find the corresponding 'KnownNat2' instance for my type-level operation
    At the Core-level, GHCs internal mini-Haskell, type families that only have a
    single equation are treated like type synonyms.

    For example, let's say we defined a closed type family @Max@:

    @
    import Data.Type.Bool (If)
    import GHC.TypeLits

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max a b = If (a <=? b) b a
    @

    Now, a Haskell-level program might contain a constraint

    @
    KnownNat (Max a b)
    @

    , however, at the Core-level, this constraint is expanded to:

    @
    KnownNat (If (a <=? b) b a)
    @

    "GHC.TypeLits.KnownNat.Solver" never sees any reference to the @Max@ type
    family, so it will not look for the corresponding 'KnownNat2' instance either.
    To fix this, ensure that your type-level operations always have at
    least two equations. For @Max@ this means we have to redefine it as:

    @
    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a
    @
    -}

    {-# LANGUAGE AllowAmbiguousTypes   #-}
    {-# LANGUAGE CPP                   #-}
    {-# LANGUAGE DataKinds             #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE GADTs                 #-}
    {-# LANGUAGE KindSignatures        #-}
    {-# LANGUAGE MagicHash             #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds             #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TemplateHaskell       #-}
    {-# LANGUAGE TypeApplications      #-}
    {-# LANGUAGE TypeOperators         #-}
    {-# LANGUAGE TypeFamilies          #-}
    #if MIN_VERSION_ghc(8,6,0)
    {-# LANGUAGE NoStarIsType #-}
    #endif
    #if !MIN_VERSION_ghc(8,2,0)
    {-# LANGUAGE BangPatterns #-}
    #endif

    {-# LANGUAGE Trustworthy #-}

    {-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}
    {-# OPTIONS_HADDOCK show-extensions #-}

    module GHC.TypeLits.KnownNat
      ( -- * Singleton natural number
        SNatKn (..)
        -- * Constraint-level arithmetic classes
      , KnownNat1 (..)
      , KnownNat2 (..)
      , KnownNat3 (..)
        -- * Singleton boolean
      , SBool (..)
      , boolVal
        -- * KnownBool
      , KnownBool (..)
        -- ** Constraint-level boolean functions
      , SBoolKb (..)
      , KnownNat2Bool (..)
      , KnownBoolNat2 (..)
        -- * Template Haskell helper
      , nameToSymbol
      )
    where

    import GHC.Natural (shiftLNatural)
    import Data.Proxy (Proxy (..))
    import Data.Type.Bool (If)
    import GHC.Prim (Proxy#)
    import GHC.TypeNats
      (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=?), type (<=),
       type Mod, type Div, natVal)
    import GHC.TypeLits (Symbol)
    import Numeric.Natural (Natural)
    import Data.Type.Ord (OrdCond)
    import GHC.Types (Constraint)

    import GHC.TypeLits.KnownNat.TH

    -- | Singleton natural number
    newtype SNatKn (f :: Symbol) = SNatKn Natural

    -- | Class for arithmetic functions with /one/ argument.
    --
    -- The 'Symbol' /f/ must correspond to the fully qualified name of the
    -- type-level operation. Use 'nameToSymbol' to get the fully qualified
    -- TH Name as a 'Symbol'
    class KnownNat1 (f :: Symbol) (a :: Nat) where
      natSing1 :: SNatKn f

    -- | Class for arithmetic functions with /two/ arguments.
    --
    -- The 'Symbol' /f/ must correspond to the fully qualified name of the
    -- type-level operation. Use 'nameToSymbol' to get the fully qualified
    -- TH Name as a 'Symbol'
    class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where
      natSing2 :: SNatKn f

    -- | Class for arithmetic functions with /three/ arguments.
    --
    -- The 'Symbol' /f/ must correspond to the fully qualified name of the
    -- type-level operation. Use 'nameToSymbol' to get the fully qualified
    -- TH Name as a 'Symbol'
    class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where
      natSing3 :: SNatKn f

    -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'
    instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where
      natSing2 :: SNatKn "GHC.TypeNats.+"
    natSing2 = Nat -> SNatKn "GHC.TypeNats.+"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn (Proxy a -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a) Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))
      {-# INLINE natSing2 #-}

    -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'
    instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where
      natSing2 :: SNatKn "GHC.TypeNats.*"
    natSing2 = Nat -> SNatKn "GHC.TypeNats.*"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn (Proxy a -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a) Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    * Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))
      {-# INLINE natSing2 #-}

    -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'
    instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where
      natSing2 :: SNatKn "GHC.TypeNats.^"
    natSing2 = let x :: Nat
    x = Proxy a -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)
                     y :: Nat
    y = Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b)
                     z :: Nat
    z = case Nat
    x of
                           Nat
    2 -> Nat -> Int -> Nat
    shiftLNatural Nat
    1 (Nat -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Nat
    y)
                           Nat
    _ -> Nat
    x Nat -> Nat -> Nat
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Nat
    y
                 in  Nat -> SNatKn "GHC.TypeNats.^"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn Nat
    z
      {-# INLINE natSing2 #-}

    -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'
    instance (KnownNat a, KnownNat b, (b <= a) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''(-)) a b where
      natSing2 :: SNatKn "GHC.TypeNats.-"
    natSing2 = Nat -> SNatKn "GHC.TypeNats.-"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn (Proxy a -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a) Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))
      {-# INLINE natSing2 #-}

    instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Div) x y where
      natSing2 :: SNatKn "GHC.TypeNats.Div"
    natSing2 = Nat -> SNatKn "GHC.TypeNats.Div"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn (Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    quot (Proxy x -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @x)) (Proxy y -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @y)))

    instance (KnownNat x, KnownNat y, (1 <= y) ~ (() :: Constraint)) => KnownNat2 $(nameToSymbol ''Mod) x y where
      natSing2 :: SNatKn "GHC.TypeNats.Mod"
    natSing2 = Nat -> SNatKn "GHC.TypeNats.Mod"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn (Nat -> Nat -> Nat
    forall a. Integral a => a -> a -> a
    rem (Proxy x -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @x)) (Proxy y -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @y)))

    -- | Singleton version of 'Bool'
    data SBool (b :: Bool) where
      SFalse :: SBool 'False
      STrue  :: SBool 'True

    class KnownBool (b :: Bool) where
      boolSing :: SBool b

    instance KnownBool 'False where
      boolSing :: SBool 'False
    boolSing = SBool 'False
    SFalse

    instance KnownBool 'True where
      boolSing :: SBool 'True
    boolSing = SBool 'True
    STrue

    -- | Get the 'Bool' value associated with a type-level 'Bool'
    --
    -- Use 'boolVal' if you want to perform the standard boolean operations on the
    -- reified type-level 'Bool'.
    --
    -- Use 'boolSing' if you need a context in which the type-checker needs the
    -- type-level 'Bool' to be either 'True' or 'False'
    --
    -- @
    -- f :: forall proxy b r . KnownBool b => r
    -- f = case boolSing @b of
    --   SFalse -> -- context with b ~ False
    --   STrue  -> -- context with b ~ True
    -- @
    boolVal :: forall b proxy . KnownBool b => proxy b -> Bool
    boolVal :: forall (b :: Bool) (proxy :: Bool -> Type).
    KnownBool b =>
    proxy b -> Bool
    boolVal proxy b
    _ = case SBool b
    forall (b :: Bool). KnownBool b => SBool b
    boolSing :: SBool b of
      SBool b
    SFalse -> Bool
    False
      SBool b
    _      -> Bool
    True

    -- | Get the `Bool` value associated with a type-level `Bool`. See also
    -- 'boolVal' and 'Proxy#'.
    boolVal' :: forall b . KnownBool b => Proxy# b -> Bool
    boolVal' :: forall (b :: Bool). KnownBool b => Proxy# b -> Bool
    boolVal' Proxy# b
    _ = case SBool b
    forall (b :: Bool). KnownBool b => SBool b
    boolSing :: SBool b of
      SBool b
    SFalse -> Bool
    False
      SBool b
    _      -> Bool
    True

    -- | A type "representationally equal" to 'SBool', used for simpler
    -- implementation of constraint-level functions that need to create instances of
    -- 'KnownBool'
    newtype SBoolKb (f :: Symbol) = SBoolKb Bool

    -- | Class for binary functions with a Boolean result.
    --
    -- The 'Symbol' /f/ must correspond to the fully qualified name of the
    -- type-level operation. Use 'nameToSymbol' to get the fully qualified
    -- TH Name as a 'Symbol'
    class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where
      boolNatSing2 :: SBoolKb f

    instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''(<=?)) a b where
      boolNatSing2 :: SBoolKb "Data.Type.Ord.<=?"
    boolNatSing2 = Bool -> SBoolKb "Data.Type.Ord.<=?"
    forall (f :: Symbol). Bool -> SBoolKb f
    SBoolKb (Proxy a -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a) Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))
      {-# INLINE boolNatSing2 #-}

    instance (KnownNat a, KnownNat b) => KnownBoolNat2 $(nameToSymbol ''OrdCond) a b where
      boolNatSing2 :: SBoolKb "Data.Type.Ord.OrdCond"
    boolNatSing2 = Bool -> SBoolKb "Data.Type.Ord.OrdCond"
    forall (f :: Symbol). Bool -> SBoolKb f
    SBoolKb (Proxy a -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a) Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))
      {-# INLINE boolNatSing2 #-}

    -- | Class for ternary functions with a Natural result.
    --
    -- The 'Symbol' /f/ must correspond to the fully qualified name of the
    -- type-level operation. Use 'nameToSymbol' to get the fully qualified
    -- TH Name as a 'Symbol'
    class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where
      natBoolSing3 :: SNatKn f

    instance (KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool $(nameToSymbol ''If) a b c where
      natBoolSing3 :: SNatKn "Data.Type.Bool.If"
    natBoolSing3 = Nat -> SNatKn "Data.Type.Bool.If"
    forall (f :: Symbol). Nat -> SNatKn f
    SNatKn (if Proxy a -> Bool
    forall (b :: Bool) (proxy :: Bool -> Type).
    KnownBool b =>
    proxy b -> Bool
    boolVal (forall (t :: Bool). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a) then Proxy b -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b) else Proxy c -> Nat
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c))