{-# 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 :: a :~: b
unsafeAxiom = (a :~: a) -> a :~: b
forall a b. a -> b
unsafeCoerce (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 :: a :~~: b
unsafeHeteroAxiom = (a :~~: a) -> a :~~: b
forall a b. a -> b
unsafeCoerce (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.
-}