    {-# LANGUAGE CPP #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeSynonymInstances #-}
    {-|
    Copyright        : (c) Galois, Inc 2019

    This module declares a class with a single method that can be used to
    derive a 'KnownRepr' constraint from an explicit 'Repr' argument.
    Clients of this method need only create an empty instance. The default
    implementation suffices.

    For example, suppose we have defined a 'Repr' type for 'Peano' numbers:

    @
    data Peano = Z | S Peano

    data PeanoRepr p where
        ZRepr :: PeanoRepr Z
        SRepr :: PeanoRepr p -> PeanoRepr (S p)

    -- KnownRepr instances
    @

    Then the instance for this class
    @
    instance IsRepr PeanoRepr
    @

    means that functions with 'KnownRepr' constraints can be used after
    pattern matching.

    @
    f :: KnownRepr PeanoRepr a => ...

    example :: PeanoRepr n -> ...
    example ZRepr = ...
    example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...
    @

    NOTE: The type 'f' must be a *singleton* type--- i.e.  for a given
    type 'a' there should be only one value that inhabits 'f a'. If that
    is not the case, this operation can be used to subvert coherence.

    Credit: the unsafe implementation of 'withRepr' is taken from the
    'withSingI' function in the singletons library
    <http://hackage.haskell.org/package/singletons-2.5.1/>.  Packaging
    this method in a class here makes it more flexible---we do not have to
    define a dedicated 'Sing' type, but can use any convenient singleton
    as a 'Repr'.

    NOTE: if this module is compiled without UNSAFE_OPS, the default
    method will not be available.

    -}
    module Data.Parameterized.WithRepr(IsRepr(..)) where

    import Data.Kind
    import Data.Parameterized.Classes

    #ifdef UNSAFE_OPS
    import Data.Constraint(Dict(..))
    import Unsafe.Coerce(unsafeCoerce)

    import Data.Parameterized.NatRepr (NatRepr)
    import Data.Parameterized.SymbolRepr (SymbolRepr)
    import Data.Parameterized.Peano (PeanoRepr)
    import Data.Parameterized.Context(Assignment)
    import Data.Parameterized.List(List)
    #else
    import Data.Parameterized.Peano (PeanoRepr,PeanoView(..))
    #endif
    import Data.Parameterized.BoolRepr

    -- | Turn an explicit Repr value into an implict KnownRepr constraint
    class IsRepr (f :: k -> Type) where

      withRepr :: f a -> (KnownRepr f a => r) -> r

    #ifdef UNSAFE_OPS
      withRepr f a
    si KnownRepr f a => r
    r = case f a -> Dict (KnownRepr f a)
    forall {k} (f :: k -> *) (a :: k).
    IsRepr f =>
    f a -> Dict (KnownRepr f a)
    reprInstance f a
    si of
                         Dict (KnownRepr f a)
    Dict -> r
    KnownRepr f a => r
    r

    reprInstance :: forall f a . IsRepr f => f a -> Dict (KnownRepr f a)
    reprInstance :: forall {k} (f :: k -> *) (a :: k).
    IsRepr f =>
    f a -> Dict (KnownRepr f a)
    reprInstance f a
    s = (KnownRepr f a => Dict (KnownRepr f a)) -> Dict (KnownRepr f a)
    with_repr Dict (KnownRepr f a)
    KnownRepr f a => Dict (KnownRepr f a)
    forall (a :: Constraint). a => Dict a
    Dict
       where
         with_repr :: (KnownRepr f a => Dict (KnownRepr f a)) -> Dict (KnownRepr f a)
         with_repr :: (KnownRepr f a => Dict (KnownRepr f a)) -> Dict (KnownRepr f a)
    with_repr KnownRepr f a => Dict (KnownRepr f a)
    si = DI f a -> f a -> Dict (KnownRepr f a)
    forall a b. a -> b
    unsafeCoerce ((KnownRepr f a => Dict (KnownRepr f a)) -> DI f a
    forall {k} (f :: k -> *) (a :: k).
    (KnownRepr f a => Dict (KnownRepr f a)) -> DI f a
    Don'tInstantiate Dict (KnownRepr f a)
    KnownRepr f a => Dict (KnownRepr f a)
    si) f a
    s

    newtype DI f a = Don'tInstantiate (KnownRepr f a => Dict (KnownRepr f a))
    #endif

    ------------------------------------
    -- Instances for types defined in parameterized-utils

    #ifdef UNSAFE_OPS
    instance IsRepr NatRepr
    instance IsRepr SymbolRepr
    instance IsRepr PeanoRepr
    instance IsRepr BoolRepr
    instance IsRepr f => IsRepr (List f)
    instance IsRepr f => IsRepr (Assignment f)
    #else
    -- awful, slow implementation for PeanoRepr
    instance IsRepr PeanoRepr where
      withRepr ZRepr f     = f
      withRepr (SRepr m) f = withRepr m f

    instance IsRepr BoolRepr where
      withRepr TrueRepr f = f
      withRepr FalseRepr f = f
    #endif