StubbedProof.hs

-- SPDX-FileCopyrightText: 2023 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Utilities for (slightly unsafely) stubbing typelevel proofs.
module Morley.Util.StubbedProof
  ( assumeKnown
  , assumeSing
  , stubProof
  ) where

import Data.Singletons (Sing)
import Data.Type.Equality ((:~:)(..))
import GHC.Exts qualified as GHC (Any)
import Unsafe.Coerce (unsafeCoerce)

import Morley.Util.Type (KList(..))

-- | A class to constrain unsafe operations to a stubbed proof. 'GHC.Any' is
-- uninhabited, making it impossible to define an instance of this class.
class GHC.Any => Stubbed where
  -- | Assume a @KnownList@ by providing a fake 'KList'. Can only be done inside a
  -- 'Stubbed' proof. This is not entirely safe due to the existence of things
  -- like @Any@, and with enough effort one could theoretically get an
  -- 'unsafeCoerce' out of a proof that uses this, but arguably it's "safe
  -- enough".
  assumeKnown :: forall xs. KList xs

  -- | Assume @SingI@ by providing a fake 'Sing'. Can only be done inside a
  -- 'Stubbed' proof. Same caveats apply as with 'assumeKnown'.
  assumeSing :: forall x. Sing x

-- | Ignore the first argument and instead 'unsafeCoerce' the result. It is
-- assumed that the first argument constitutes a semi-proper proof.
stubProof :: forall a b. (Stubbed => a :~: b) -> a :~: b
stubProof _ = unsafeCoerce Refl
{-# INLINE stubProof #-}