{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RoleAnnotations     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

module Logic.Implicit
    ( Fact
    , known
    , note
    , on
    ) where

import           Logic.Proof
import           Theory.Named

import           Unsafe.Coerce

-- | A @Fact p@ is an implicit proof of @p@, propagated by Haskell's constraint solver.
--   @Fact@s can be used to implicitly introduce or propagate proofs. However, there is
--   a small run-time cost associated with using @Fact@s: typeclass dictionaries for
--   @Fact@s are still passed around. In many cases they will be optimized away, but this
--   is not guaranteed.
class Fact p

-- | Recall a known @Fact@ from the implicit context.
known :: Fact p => Proof p
known = axiom

newtype WithFact p t = WithFact (Fact p => t)
type role WithFact nominal nominal

-- | Add a proof to the implicit context.
note :: forall p t. Proof p -> (Fact p => t) -> t
note _ k = unsafeCoerce (WithFact k :: WithFact p t) ()

{-| Apply an implication to a predicate in the implicit context. The @(a ~~ n)@
    parameter is not actually used; it's type is used to help select a specific
    fact from the context.

@
-- A safe 'head' function, using an implicitly-passed safety proof.
head :: Fact (IsCons xs) => ([a] ~~ xs) -> a
head xs = Prelude.head (the xs)

-- Reverse, and a lemma.
reverse :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
revConsLemma :: Proof (IsCons xs) -> Proof (IsCons (Reverse xs))

-- Implement a safe 'last' function.
last :: Fact (IsCons xs) => ([a] ~~ xs) -> a
last xs = note (revConsLemma `on` xs) $ head (reverse xs)
-}
on :: Fact (p n) => (Proof (p n) -> Proof q) -> (a ~~ n) -> Proof q
on impl _ = impl known