{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
module T13910 where

import Data.Kind
import Data.Type.Equality

data family Sing (a :: k)

class SingKind k where
  type Demote k = (r :: Type) | r -> k
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

data SomeSing k where
  SomeSing :: Sing (a :: k) -> SomeSing k

withSomeSing :: forall k r
              . SingKind k
             => Demote k
             -> (forall (a :: k). Sing a -> r)
             -> r
withSomeSing x f =
  case toSing x of
    SomeSing x' -> f x'

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@

data FunArrow = (:->) | (:~>)

class FunType (arr :: FunArrow) where
  type Fun (k1 :: Type) arr (k2 :: Type) :: Type

class FunType arr => AppType (arr :: FunArrow) where
  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2

type FunApp arr = (FunType arr, AppType arr)

instance FunType (:->) where
  type Fun k1 (:->) k2 = k1 -> k2

$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter

instance AppType (:->) where
  type App k1 (:->) k2 (f :: k1 -> k2) x = f x

instance FunType (:~>) where
  type Fun k1 (:~>) k2 = k1 ~> k2

$(return [])

instance AppType (:~>) where
  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x

infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2

data instance Sing (z :: a :~: b) where
  SRefl :: Sing Refl

instance SingKind (a :~: b) where
  type Demote (a :~: b) = a :~: b
  fromSing SRefl = Refl
  toSing Refl = SomeSing SRefl

(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
           Sing r
        -> p @@ Refl
        -> p @@ r
(~>:~:) SRefl pRefl = pRefl

type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
                    (y :: t) (e :: from :~: y) = App t arr Type p y
data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
  :: forall (y :: t). from :~: y ~> Type
type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
  = WhyReplacePoly arr from p y x

replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
           p from
        -> from :~: to
        -> p to
replace = replacePoly @(:->)

replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
                p @@ from
             -> from :~: to
             -> p @@ to
replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p

replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
                      (p :: (t -?> Type) arr).
               FunApp arr
            => App t arr Type p from
            -> from :~: to
            -> App t arr Type p to
replacePoly from eq =
  withSomeSing eq $ \(singEq :: Sing r) ->
    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from

type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
  = App t arr Type f a -> App t arr Type f z
data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
  :: t ~> Type
type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z

leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
                      (a :: t) (b :: t).
               FunApp arr
            => a :~: b
            -> App t arr Type f a
            -> App t arr Type f b
leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id

leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
           a :~: b
        -> f a
        -> f b
leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
-- The line above is what you get if you inline the definition of leibnizPoly.
-- It causes a panic, however.
--
-- An equivalent implementation is commented out below, which does *not*
-- cause GHC to panic.
--
-- leibniz = leibnizPoly @(:->)

leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
                a :~: b
             -> f @@ a
             -> f @@ b
leibnizTyFun = leibnizPoly @(:~>) @_ @f