Path inductionで型レベル同値関係から値レベル同値関係を導く

kequiv.hs

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, TypeOperators, FlexibleInstances, MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications, TypeInType, GADTs, RankNTypes #-}

import GHC.Types
import Data.Type.Equality
import Unsafe.Coerce

-- 仮定：Path Induction
indEquiv ::
    forall k (t :: forall (x :: k) (y :: k). (x :~: y) -> Type).
    (forall x. t ('Refl :: x :~: x)) -> forall a b (p :: a :~: b). t p
indEquiv f = unsafeCoerce f

-- ヘルパ
data SEq a b (p :: a :~: b)
  where
    SRefl :: SEq a a Refl

sRefl :: forall x. SEq x x ('Refl :: x :~: x)
sRefl = SRefl

-- 型レベル同値関係 → 値レベル同値関係
singEq :: forall x y (p :: x :~: y). x :~: y
singEq = case (indEquiv sRefl :: SEq x y p) of {SRefl -> Refl}



main :: IO ()
main = putStrLn $ castWith (singEq @ String @ String @ 'Refl) $ "Hello, world!"