main.hs

{-# LANGUAGE DataKinds, TypeOperators, GADTs, KindSignatures, RankNTypes #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality(type (==), (:~:)(Refl))
import Unsafe.Coerce

data Vec t (n :: Nat) where
  VNil  :: Vec t 0
  VCons :: t -> Vec t n -> Vec t (n+1)

-- This function is OK
insert :: (Ord t) => t -> Vec t n -> Vec t (n+1)
insert x VNil = VCons x VNil
insert x (VCons y ys) | x >  y = VCons y (insert x ys)
insert x (VCons y ys) | x <= y = VCons y (insert x ys)

-- Proxy type for kind Nat
data NatProxy :: Nat -> * where
  NatProxy :: NatProxy n
                                 
sort :: (Ord t) => Vec t n -> Vec t n
sort l = sort'
         (NatProxy :: NatProxy n) (NatProxy :: NatProxy n) (NatProxy :: NatProxy 0)
         Refl l VNil

-- This function does not compile
sort' :: forall l n1 n2 t. (Ord t) =>
         NatProxy l -> NatProxy n1 -> NatProxy n2 -> (l :~: n1 + n2) ->
         Vec t n1 -> Vec t n2 -> Vec t l
-- This case is fine.
sort' p1 p2 p3 Refl VNil acc = acc
-- This one fails with hideous type errors.
sort' p1 p2 p3 witness (VCons x xs) acc =
  case Refl of
   Refl -> 
     sort'
     (NatProxy :: NatProxy l) (NatProxy :: NatProxy (n1-1)) (NatProxy :: NatProxy (n2+1))
     (Refl :: l :~: (n1-1) + (n2+1))
     xs (insert x acc)

main :: IO ()
main = return ()