Subtyping.hs

{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Subtyping where

import Data.Proxy

type family SubtypeOf a :: [*]

type family Head (as :: [k]) :: k where
    Head (a ': _) = a

type family Append as bs :: [k] where
    Append '[]       bs = bs
    Append (a ': as) bs = a ': Append as bs

type family ConcatMapPaths p a bs :: [[*]] where
    ConcatMapPaths p a '[]       = '[]
    ConcatMapPaths p a (b ': bs) = Append (Paths p a b) (ConcatMapPaths p a bs)

type family Paths p a b :: [[*]] where
    Paths p a a = p ': '[]
    Paths p a b = ConcatMapPaths (b ': p) a (SubtypeOf b)

type family Path a b where
    Path a b = Head (Paths '[] a b)

class a <! b where
    upcastDirect :: a -> b

upcastDirectTo :: a <! b => proxy b -> a -> b
upcastDirectTo _ = upcastDirect

class UpcastBy ps a c where
    upcastBy :: Proxy ps -> a -> c

instance a ~ c => UpcastBy '[] a c where
    upcastBy _ = id

instance (a <! b, UpcastBy ps b c) => UpcastBy (b ': ps) a c where
    upcastBy _ = upcastBy (Proxy @ps) . upcastDirectTo (Proxy @b)

upcast :: forall a c. UpcastBy (Path a c) a c => a -> c
upcast = upcastBy $ Proxy @(Path a c)

--------------------

{-
     Err4
       |
     Err3      Err5
    /    \    /
Err1      Err2
-}

data Err1 = Err1                    deriving (Show)
data Err2 = Err2                    deriving (Show)
data Err3 = Err31 Err1 | Err32 Err2 deriving (Show)
newtype Err4 = Err43 Err3           deriving (Show)
newtype Err5 = Err52 Err2           deriving (Show)

type instance SubtypeOf Err1 = '[]
type instance SubtypeOf Err2 = '[]
type instance SubtypeOf Err3 = '[Err1, Err2]
type instance SubtypeOf Err4 = '[Err3]
type instance SubtypeOf Err5 = '[Err2]

instance Err1 <! Err3 where
    upcastDirect = Err31

instance Err2 <! Err3 where
    upcastDirect = Err32

instance Err3 <! Err4 where
    upcastDirect = Err43

instance Err2 <! Err5 where
    upcastDirect = Err52

test1 :: Err1 -> Err3
test1 = upcast

test2 :: Err2 -> Err3
test2 = upcast

test3 :: Err1 -> Err4
test3 = upcast

test4 :: Err2 -> Err4
test4 = upcast

test5 :: Err2 -> Err5
test5 = upcast