{-# LANGUAGE GADTs        #-}
{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Singletons

-- | inductive structure
data Foo = Foo Foo | End

-- | the isomorphic type for 'Foo'
data RealFoo = RFoo RealFoo | REnd
  deriving (Show)

data instance Sing (a :: Foo) where
  EndS :: Sing 'End
  FooS :: Sing a -> Sing ('Foo a)

instance SingI 'End where
  sing = EndS
instance SingI a => SingI ('Foo a) where
  sing = FooS sing

instance SingKind Foo where
  type DemoteRep Foo = RealFoo
  fromSing EndS = REnd
  fromSing (FooS s) = RFoo (fromSing s)
  toSing REnd = SomeSing EndS
  toSing (RFoo r) = case toSing r of
    SomeSing s -> SomeSing (FooS s)

main :: IO ()
main = do
  print $ fromSing (sing :: Sing 'End)        -- => REnd
  print $ fromSing (sing :: Sing ('Foo 'End)) -- => RFoo REnd