{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Represents different versions of a config file
data ConfigVersion = V1 | V2 | V3

-- | Represents the config itself, at different versions
data VersionedConfig (v :: ConfigVersion) where
  CV1 :: Int -> VersionedConfig V1
  CV2 :: Integer -> VersionedConfig V2
  CV3 :: String -> VersionedConfig V3
  
deriving instance Show (VersionedConfig v)
  
-- | Proof term for migration between versions
data MigrateableProof (from :: ConfigVersion) (to :: ConfigVersion) where
  MigrateableProof :: (VersionedConfig from -> VersionedConfig to) -> MigrateableProof from to
  
class MigrateableFromTo (from :: ConfigVersion) (to :: ConfigVersion) where
  migrateFromTo :: MigrateableProof from to
  
instance MigrateableFromTo V1 V2 where
  migrateFromTo = MigrateableProof (\(CV1 a) -> CV2 (toEnum a))
  
instance MigrateableFromTo V2 V3 where
  migrateFromTo = MigrateableProof (\(CV2 a) -> CV3 (show a))
  
instance forall from intermediate to.
  (MigrateableFromTo from intermediate, MigrateableFromTo intermediate to)
  => MigrateableFromTo from to where
  migrateFromTo = MigrateableProof (applyMigration @intermediate . applyMigration)
    
applyMigration :: MigrateableFromTo from to => VersionedConfig from -> VersionedConfig to
applyMigration = let MigrateableProof f = migrateFromTo in f 

main :: IO ()
main = do
  let
    cv1 = CV1 5
    cv3 = (applyMigration cv1) :: VersionedConfig V3
  print cv3