Type-level Haskell programming to ensure that type versions are "migratable"

Migratatable.hs

-- | A type-level, constraint-writing function that ensures that some
-- versioned type is migratable throughout its entire version history.
--
-- Assumes that type version history starts at '1'.

{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import           Data.Kind
import           Data.Ord
import           GHC.Exts
import           GHC.TypeNats

-- | "Dummy" constraint
class NoConstraint (a :: Nat -> *) where
instance NoConstraint a where

-- | Haskell does not allow us to define a type family instance for
-- both a concrete and a polymorphic type, so we work around it by
-- using peano representation.
data Nat1 = Zero | Succ Nat1

type family FromNat1 (n :: Nat1) :: Nat where
  FromNat1 Zero = 0
  FromNat1 (Succ n) = 1 + FromNat1 n

type family ToNat1 (n :: Nat) :: Nat1 where
  ToNat1 0 = Zero
  ToNat1 1 = Succ (ToNat1 0)
  ToNat1 2 = Succ (ToNat1 1)
  ToNat1 3 = Succ (ToNat1 2)
  ToNat1 4 = Succ (ToNat1 3)
  ToNat1 5 = Succ (ToNat1 4)
  ToNat1 6 = Succ (ToNat1 5)
  ToNat1 7 = Succ (ToNat1 6)
  ToNat1 8 = Succ (ToNat1 7)
  ToNat1 9 = Succ (ToNat1 8)
  ToNat1 10 = Succ (ToNat1 9)
  ToNat1 11 = Succ (ToNat1 10)

type family MigrateBound (n :: Nat1) :: (Nat -> Type) -> Constraint
type instance MigrateBound Zero = NoConstraint
type instance MigrateBound (Succ n) = Migrate (FromNat1 (Succ n))

class ((1 <= n), MigrateBound (ToNat1 (n - 1)) t) => Migrate (n :: Nat) (t :: Nat -> Type) where
  migrate :: t (n - 1) -> t n

data Event (version :: Nat) = SomeEvent

instance Migrate 3 Event where
  migrate = undefined

-- -- as expected:
-- --
-- Migrate.hs:27:10-24: error:
--     • No instance for (Migrate 2 Event)
--         arising from the superclasses of an instance declaration
--     • In the instance declaration for ‘Migrate 3 Event’
--    |
-- 27 | instance Migrate 3 Event where
--    |          ^^^^^^^^^^^^^^^
-- Failed, no modules loaded.

-- -- so lets make it happy:

instance Migrate 2 Event where
  migrate = undefined

instance Migrate 1 Event where
  migrate = undefined

-- bonus, if we tried to define:
--
-- instance Migrate 0 Event where
--   migrate = undefined
--
-- we get a type error:
--
-- /tmp/Constraints.hs:78:10-24: error:
--     • Couldn't match type ‘'False’ with ‘'True’
--         arising from the superclasses of an instance declaration
--     • In the instance declaration for ‘Migrate 0 Event’
--    |
-- 78 | instance Migrate 0 Event where