{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | This module provides type-level functions that need proofs to work
-- properly.
module Options.Harg.Het.Proofs
  ( type (++),
    Proof (..),
    hgcastWith,
  )
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 :: (a :~~: b) -> ((a ~~ b) => r) -> r
hgcastWith HRefl x :: (a ~~ b) => r
x = r
(a ~~ b) => r
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 :: ('[] ++ '[]) :~~: '[]
proofNil = ('[] ++ '[]) :~~: '[]
forall k1 (a :: k1). a :~~: a
HRefl

instance ProofNil xs => ProofNil (x ': xs) where
  proofNil :: ((x : xs) ++ '[]) :~~: (x : xs)
proofNil = ((xs ++ '[]) :~~: xs)
-> (((xs ++ '[]) ~~ xs) => (x : (xs ++ '[])) :~~: (x : xs))
-> (x : (xs ++ '[])) :~~: (x : xs)
forall k k' (a :: k) (b :: k') r.
(a :~~: b) -> ((a ~~ b) => r) -> r
hgcastWith (ProofNil xs => (xs ++ '[]) :~~: xs
forall k (xs :: [k]). ProofNil xs => (xs ++ '[]) :~~: xs
proofNil @xs) ((xs ++ '[]) ~~ xs) => (x : (xs ++ '[])) :~~: (x : xs)
forall k1 (a :: k1). a :~~: a
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 :: ((x : xs) ++ '[y]) :~~: (((x : xs) ++ '[y]) ++ '[])
proof = (((xs ++ '[y]) ++ '[]) :~~: (xs ++ '[y]))
-> ((((xs ++ '[y]) ++ '[]) ~~ (xs ++ '[y])) =>
    (x : (xs ++ '[y])) :~~: (x : ((xs ++ '[y]) ++ '[])))
-> (x : (xs ++ '[y])) :~~: (x : ((xs ++ '[y]) ++ '[]))
forall k k' (a :: k) (b :: k') r.
(a :~~: b) -> ((a ~~ b) => r) -> r
hgcastWith (ProofNil (xs ++ '[y]) => ((xs ++ '[y]) ++ '[]) :~~: (xs ++ '[y])
forall k (xs :: [k]). ProofNil xs => (xs ++ '[]) :~~: xs
proofNil @(xs ++ '[y])) (((xs ++ '[y]) ++ '[]) ~~ (xs ++ '[y])) =>
(x : (xs ++ '[y])) :~~: (x : ((xs ++ '[y]) ++ '[]))
forall k1 (a :: k1). a :~~: a
HRefl

instance Proof '[] y zs where
  proof :: ('[] ++ (y : zs)) :~~: (('[] ++ '[y]) ++ zs)
proof = ('[] ++ (y : zs)) :~~: (('[] ++ '[y]) ++ zs)
forall k1 (a :: k1). a :~~: a
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 :: (x : (xs ++ (y : z : zs))) :~~: (x : ((xs ++ '[y]) ++ (z : zs)))
proof = ((xs ++ (y : z : zs)) :~~: ((xs ++ '[y]) ++ (z : zs)))
-> (((xs ++ (y : z : zs)) ~~ ((xs ++ '[y]) ++ (z : zs))) =>
    (x : (xs ++ (y : z : zs))) :~~: (x : ((xs ++ '[y]) ++ (z : zs))))
-> (x : (xs ++ (y : z : zs))) :~~: (x : ((xs ++ '[y]) ++ (z : zs)))
forall k k' (a :: k) (b :: k') r.
(a :~~: b) -> ((a ~~ b) => r) -> r
hgcastWith (Proof xs y (z : zs) =>
(xs ++ (y : z : zs)) :~~: ((xs ++ '[y]) ++ (z : zs))
forall k (xs :: [k]) (y :: k) (zs :: [k]).
Proof xs y zs =>
(xs ++ (y : zs)) :~~: ((xs ++ '[y]) ++ zs)
proof @xs @y @(z ': zs)) ((xs ++ (y : z : zs)) ~~ ((xs ++ '[y]) ++ (z : zs))) =>
(x : (xs ++ (y : z : zs))) :~~: (x : ((xs ++ '[y]) ++ (z : zs)))
forall k1 (a :: k1). a :~~: a
HRefl

instance Proof '[] y '[] where
  proof :: ('[] ++ '[y]) :~~: (('[] ++ '[y]) ++ '[])
proof = ('[] ++ '[y]) :~~: (('[] ++ '[y]) ++ '[])
forall k1 (a :: k1). a :~~: a
HRefl