{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Versioning.Upgrade
( Adapt (..)
, Upgrade
, upgrade
, Downgrade
, downgrade
)
where
import Data.Kind (Type)
import Versioning.Base
import Versioning.Internal.Equality (type (==))
class Adapt (v :: V) (w :: V) (a :: V -> Type) where
adapt :: a v -> a w
upgrade :: forall v w a. Upgrade v w a => a v -> a w
upgrade :: a v -> a w
upgrade = forall (eq :: Bool) (v :: V) (w :: V) (a :: V -> *).
Upgrade' eq v w a =>
a v -> a w
forall (v :: V) (w :: V) (a :: V -> *).
Upgrade' (v == w) v w a =>
a v -> a w
upgrade' @(v == w)
type Upgrade v w a = Upgrade' (v == w) v w a
class Upgrade' (eq :: Bool) (v :: V) (w :: V) (a :: V -> Type) where
upgrade' :: a v -> a w
instance (v ~ w) => Upgrade' 'True v w a where
upgrade' :: a v -> a w
upgrade' a v
x = a v
a w
x
instance (Adapt v (VSucc v) a, Upgrade' (VSucc v == w) (VSucc v) w a)
=> Upgrade' 'False v w a where
upgrade' :: a v -> a w
upgrade' a v
x = a (VSucc v) -> a w
forall (eq :: Bool) (v :: V) (w :: V) (a :: V -> *).
Upgrade' eq v w a =>
a v -> a w
upgrade' @(VSucc v == w) @(VSucc v) @w (a v -> a (VSucc v)
forall (v :: V) (w :: V) (a :: V -> *). Adapt v w a => a v -> a w
adapt @v @(VSucc v) a v
x)
downgrade :: forall v w a. Downgrade v w a => a v -> a w
downgrade :: a v -> a w
downgrade = forall (eq :: Bool) (v :: V) (w :: V) (a :: V -> *).
Downgrade' eq v w a =>
a v -> a w
forall (v :: V) (w :: V) (a :: V -> *).
Downgrade' (v == w) v w a =>
a v -> a w
downgrade' @(v == w)
type Downgrade v w a = Downgrade' (v == w) v w a
class Downgrade' (eq :: Bool) (v :: V) (w :: V) (a :: V -> Type) where
downgrade' :: a v -> a w
instance (v ~ w) => Downgrade' 'True v w a where
downgrade' :: a v -> a w
downgrade' a v
x = a v
a w
x
instance (Adapt v (VPred v) a, Downgrade' (VPred v == w) (VPred v) w a)
=> Downgrade' 'False v w a where
downgrade' :: a v -> a w
downgrade' a v
x = a (VPred v) -> a w
forall (eq :: Bool) (v :: V) (w :: V) (a :: V -> *).
Downgrade' eq v w a =>
a v -> a w
downgrade' @(VPred v == w) @(VPred v) @w (a v -> a (VPred v)
forall (v :: V) (w :: V) (a :: V -> *). Adapt v w a => a v -> a w
adapt @v @(VPred v) a v
x)