    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE Unsafe #-}
    {-# LANGUAGE CPP #-}
    {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}

    -- |
    -- Copyright   :  (C) 2011-2021 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Unsafe utilities used throughout @constraints@. As the names suggest, these
    -- functions are unsafe in general and can cause your program to segfault if
    -- used improperly. Handle with care.

    module Data.Constraint.Unsafe
      ( Coercible
      , unsafeAxiom
      , unsafeCoerceConstraint
      , unsafeDerive
      , unsafeUnderive

    #if MIN_VERSION_base(4,18,0)
        -- * Unsafely creating @GHC.TypeLits@ singleton values
      , unsafeSChar
      , unsafeSNat
      , unsafeSSymbol
    #endif
      ) where

    import Data.Coerce
    import Data.Constraint
    import Unsafe.Coerce

    #if MIN_VERSION_base(4,18,0)
    import GHC.TypeLits (SChar, SNat, SSymbol)
    import Numeric.Natural (Natural)
    #endif

    -- | Unsafely create a dictionary for any constraint.
    unsafeAxiom :: Dict c
    unsafeAxiom :: forall (c :: Constraint). Dict c
    unsafeAxiom = Dict (() :: Constraint) -> Dict c
    forall a b. a -> b
    unsafeCoerce (Dict (() :: Constraint)
    forall (a :: Constraint). a => Dict a
    Dict :: Dict ())

    -- | Coerce a dictionary unsafely from one type to another
    unsafeCoerceConstraint :: a :- b
    unsafeCoerceConstraint :: forall (a :: Constraint) (b :: Constraint). a :- b
    unsafeCoerceConstraint = (ZonkAny 0 :- ZonkAny 0) -> a :- b
    forall a b. a -> b
    unsafeCoerce ZonkAny 0 :- ZonkAny 0
    forall (a :: Constraint). a :- a
    refl

    -- | Coerce a dictionary unsafely from one type to a newtype of that type
    unsafeDerive :: Coercible n o => (o -> n) -> t o :- t n
    unsafeDerive :: forall n o (t :: * -> Constraint).
    Coercible n o =>
    (o -> n) -> t o :- t n
    unsafeDerive o -> n
    _ = t o :- t n
    forall (a :: Constraint) (b :: Constraint). a :- b
    unsafeCoerceConstraint

    -- | Coerce a dictionary unsafely from a newtype of a type to the base type
    unsafeUnderive :: Coercible n o => (o -> n) -> t n :- t o
    unsafeUnderive :: forall n o (t :: * -> Constraint).
    Coercible n o =>
    (o -> n) -> t n :- t o
    unsafeUnderive o -> n
    _ = t n :- t o
    forall (a :: Constraint) (b :: Constraint). a :- b
    unsafeCoerceConstraint

    #if MIN_VERSION_base(4,18,0)
    -- NB: if https://gitlab.haskell.org/ghc/ghc/-/issues/23478 were implemented,
    -- then we could avoid using 'unsafeCoerce' in the definitions below.

    -- | Unsafely create an 'SChar' value directly from a 'Char'. Use this function
    -- with care:
    --
    -- * The 'Char' value must match the 'Char' @c@ encoded in the return type
    --   @'SChar' c@.
    --
    -- * Be wary of using this function to create multiple values of type
    --   @'SChar' T@, where @T@ is a type family that does not reduce (e.g.,
    --   @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of
    --   the values and replace it with the other during a common subexpression
    --   elimination pass. If the two values have different underlying 'Char'
    --   values, this could be disastrous.
    unsafeSChar :: Char -> SChar c
    unsafeSChar :: forall (c :: Char). Char -> SChar c
    unsafeSChar = Char -> SChar c
    forall a b. a -> b
    unsafeCoerce

    -- | Unsafely create an 'SNat' value directly from a 'Natural'. Use this
    -- function with care:
    --
    -- * The 'Natural' value must match the 'Nat' @n@ encoded in the return type
    --   @'SNat' n@.
    --
    -- * Be wary of using this function to create multiple values of type
    --   @'SNat' T@, where @T@ is a type family that does not reduce (e.g.,
    --   @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of
    --   the values and replace it with the other during a common subexpression
    --   elimination pass. If the two values have different underlying 'Natural'
    --   values, this could be disastrous.
    unsafeSNat :: Natural -> SNat n
    unsafeSNat :: forall (n :: Nat). Nat -> SNat n
    unsafeSNat = Nat -> SNat n
    forall a b. a -> b
    unsafeCoerce

    -- | Unsafely create an 'SSymbol' value directly from a 'String'. Use this
    -- function with care:
    --
    -- * The 'String' value must match the 'Symbol' @s@ encoded in the return type
    --   @'SSymbol' s@.
    --
    -- * Be wary of using this function to create multiple values of type
    --   @'SSymbol' T@, where @T@ is a type family that does not reduce (e.g.,
    --   @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of
    --   the values and replace it with the other during a common subexpression
    --   elimination pass. If the two values have different underlying 'String'
    --   values, this could be disastrous.
    unsafeSSymbol :: String -> SSymbol s
    unsafeSSymbol :: forall (s :: Symbol). String -> SSymbol s
    unsafeSSymbol = String -> SSymbol s
    forall a b. a -> b
    unsafeCoerce
    #endif