    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE Unsafe #-}
    {-|
    Copyright        : (c) Galois, Inc 2014-2021

    An unsafe module that provides functionality for constructing equality proofs
    that GHC cannot prove on its own.
    -}
    module Data.Parameterized.Axiom
      ( unsafeAxiom, unsafeHeteroAxiom
      ) where

    import Data.Type.Equality
    import Unsafe.Coerce (unsafeCoerce)

    -- | Assert a proof of equality between two types.
    -- This is unsafe if used improperly, so use this with caution!
    unsafeAxiom :: forall a b. a :~: b
    unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom = (a :~: a) -> a :~: b
    forall a b. a -> b
    unsafeCoerce (forall (a :: k). a :~: a
    forall {k} (a :: k). a :~: a
    Refl @a)
    {-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]

    -- | Assert a proof of heterogeneous equality between two types.
    -- This is unsafe if used improperly, so use this with caution!
    unsafeHeteroAxiom :: forall a b. a :~~: b
    unsafeHeteroAxiom :: forall {k1} {k2} (a :: k1) (b :: k2). a :~~: b
    unsafeHeteroAxiom = (a :~~: a) -> a :~~: b
    forall a b. a -> b
    unsafeCoerce (forall (a :: k1). a :~~: a
    forall {k1} (a :: k1). a :~~: a
    HRefl @a)
    {-# NOINLINE unsafeHeteroAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]

    {-
    Note [Mark unsafe axioms as NOINLINE]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We take care to mark definitions that use unsafeCoerce to construct proofs
    (e.g., unsafeAxiom = unsafeCoerce Refl) as NOINLINE. There are at least two
    good reasons to do so:

    1. On old version of GHC (prior to 9.0), GHC was liable to optimize
       `unsafeCoerce` too aggressively, leading to unsound runtime behavior.
       See https://gitlab.haskell.org/ghc/ghc/-/issues/16893 for an example.

    2. If GHC too heavily optimizes a program which cases on a proof of equality,
       where the equality is between two types that can be determined not to be
       equal statically (e.g., case (unsafeAxiom :: Bool :~: Int) of ...), then the
       optimized program can crash at runtime. See
       https://gitlab.haskell.org/ghc/ghc/-/issues/16310. Using NOINLINE is
       sufficient to work around the issue.
    -}