-- | This module provides type-level functions that need proofs to work
-- properly.
{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE InstanceSigs         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
module Options.Harg.Het.Proofs where

import Data.Kind          (Type)
import Data.Type.Equality


-- | Same as 'Data.Type.Equality.gcastWith' but for heterogeneous propositional
-- equality
hgcastWith
  :: forall (a :: k) (b :: k') (r :: Type).
     (a :~~: b)
  -> (a ~~ b => r)
  -> r
hgcastWith HRefl x = x

-- * Concatenation of type-level lists

-- | Append two type-level lists
--
-- @
-- > :kind! '[Int, Bool] ++ '[Char, Maybe Int]
-- '[Int, Bool, Char, Maybe Int]
-- @
--
type family (xs :: [k]) ++ (ts :: [k]) = (res :: [k]) where
  '[]       ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

-- | Proof that appending an empty list to any list has no effect on the latter.
class ProofNil xs where
  proofNil :: xs ++ '[] :~~: xs

instance ProofNil '[] where
  proofNil = HRefl

instance ProofNil xs => ProofNil (x ': xs) where
  proofNil = hgcastWith (proofNil @xs) HRefl

-- | Proof that appending two lists is the same as appending the first element
-- of the second list to the first one, and then appending the rest.
class Proof xs y zs where
  proof :: xs ++ (y ': zs) :~~: (xs ++ '[y]) ++ zs

instance ProofNil (xs ++ '[y]) => Proof (x ': xs) y '[] where
  proof = hgcastWith (proofNil @(xs ++ '[y])) HRefl

instance Proof '[] y zs where
  proof = HRefl

-- | Induction on the tail of the list
instance Proof xs y (z ': zs) => Proof (x ': xs) y (z ': zs) where
  proof
    ::   x ': (xs ++ (y ': z ': zs))
    :~~: x ': ((xs ++ '[y]) ++ (z ': zs))
  proof = hgcastWith (proof @xs @y @(z ': zs)) HRefl

instance Proof '[] y '[] where
  proof = HRefl