wrap a data in Just if it is missing

CountM.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module CountM where
import Data.Proxy
import Control.Monad

data N = Z | S N

type family CountM m x where
  CountM m (m x) = S (CountM m x)
  CountM m x = Z

type family Sub x y where
  Sub (S x) (S y) = Sub x y
  Sub x Z = x

f :: x -> Proxy (S Z `Sub` CountM Maybe x)
f _ =Proxy

ensure1Maybe :: forall n x x'. (n ~ (S Z `Sub` CountM Maybe x) ,ReturnN Maybe n x x') => x -> x'
ensure1Maybe = returnN (Proxy :: Proxy Maybe) (Proxy :: Proxy n)

class Monad m => ReturnN (m :: * -> *) (n :: N) x x' | m n x -> x' where
  returnN :: Proxy m -> Proxy n -> x -> x'

instance Monad m => ReturnN m Z x x where
    returnN _ _ = id

instance (Monad m, ReturnN m n x x') => ReturnN m (S n) x (m x') where
    returnN pm _ = return . returnN pm (Proxy :: Proxy n)


{- |

>>> kristoffer "x" "y"
Just "xy"

>>> kristoffer "x" (Just "y")
Just "xy"

>>> kristoffer (Just "x") (Just "y")
Just "xy"

>>> kristoffer "x" (Just "y")
Just "xy"

-}
kristoffer x y = liftM2 (++) (ensure1Maybe x) (ensure1Maybe y)