twice . half of even = id.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import Data.Type.Equality

data N = Z | S N

type IsEven :: N -> Type
data IsEven n where
  ZIsEven :: IsEven Z
  SSIsEven :: IsEven n -> IsEven (S (S n))

type Half :: N -> N
type family Half x where
  Half Z = Z
  Half (S Z) = Z
  Half (S (S x)) = S (Half x)

type Twice :: N -> N
type family Twice x where
  Twice Z = Z
  Twice (S n) = S (S (Twice n))

type Cong :: forall f a b. a :~: b -> f a :~: f b
type family Cong p where
  Cong Refl = Refl

type TwiceOfHalfOfEven :: forall (x :: N) -> IsEven x -> Twice (Half x) :~: x
type family TwiceOfHalfOfEven x p where
  TwiceOfHalfOfEven Z ZIsEven = Refl
  TwiceOfHalfOfEven (S (S x)) (SSIsEven p) = Cong (Cong (TwiceOfHalfOfEven x p))