Fixes.hs

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Fixes where

data Nat = Z | S Nat

data Fin (max :: Nat) where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n)

data Vec (n :: Nat) (a :: *) where
  Nil  :: Vec n a
  (:*) :: a -> Vec n a -> Vec ('S n) a

type family Map (f :: k -> l) (xs :: Vec n k) :: Vec n l where
  Map f 'Nil       = 'Nil
  Map f (x ':* xs) = f x ':* Map f xs

type family Index (i :: Fin n) (xs :: Vec n k) :: k where
  Index 'FZ     (x ':* _)  = x
  Index ('FS n) (_ ':* xs) = Index n xs

type family Range (n :: Nat) :: Vec n (Fin n) where
  Range 'Z     = 'Nil
  Range ('S n) = 'FZ ':* Map 'FS (Range n)

newtype Fixes (fs :: Vec n (Vec n * -> *)) (i :: Fin n)
  = Fixes (Index i fs (Map (Fixes fs) (Range n)))