VarF.hs

{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module VarF where

import           Data.Constraint       (Dict (..))
import           Data.Functor.Classes
import           Data.Functor.Const
import           Data.Kind             (Constraint, Type)
import           Data.Proxy            (Proxy (Proxy))
import           Data.Row
import           Data.Row.Internal
import           GHC.TypeLits          (Symbol)

type family ApRow (r :: Row (k -> Type)) (x :: k) :: Row Type where
    ApRow (R r) x = R (ApLT r x)

type family ApLT (r :: [LT (k -> Type)]) (x :: k) :: [LT Type] where
    ApLT '[] _ = '[]
    ApLT (lbl :-> f : rest) x = lbl :-> f x : ApLT rest x

-- apLaw :: forall (l :: Symbol) (ρ :: Row (k -> Type)) (x :: k).
         -- Dict ((ApRow ρ x .! l) ~ (ρ .! l) x)
-- apLaw = Dict

newtype VarF (r :: Row (k -> Type)) (x :: k) = VarF { unVarF :: Var (ApRow r x) }

newtype FlipApp a f = FlipApp (f a)

newtype VarF' (x :: k) (r :: Row (k -> Type)) = VarF' { unVarF' :: Var (ApRow r x) }

varFAlg
    :: forall (c :: (Type -> Type) -> Constraint) (r :: Row (Type -> Type)) (x :: Type) (y :: Type). Forall r c
    => (forall f. c f => f x -> y)
    -> VarF r x
    -> y
varFAlg f = getConst . go . VarF' . unVarF
    where
        go :: VarF' x r -> Const y r
        go = metamorph @(Type -> Type) @r @c @Either @(VarF' x) @(Const y) @(FlipApp x) proxy doNil doUncons doCons
        proxy :: Proxy (Proxy (FlipApp x), Proxy Either)
        proxy = Proxy
        doNil :: VarF' x Empty -> Const y Empty
        doNil = impossible . unVarF'
        doUncons :: forall l τ ρ. (KnownSymbol l, HasType l τ ρ)
                 => Label l
                 -> VarF' x ρ
                 -> Either (VarF' x (ρ .- l)) (FlipApp x τ)
        doUncons l (VarF' v) =
            case trial v l of
              _ -> undefined
              -- Right (tx :: _) -> Right (FlipApp tx)
              -- Left v' -> Left (VarF' v')
        doCons :: forall l τ ρ. (KnownSymbol l, FrontExtends l τ ρ, AllUniqueLabels (Extend l τ ρ))
               => Label l
               -> Either (Const y ρ) (FlipApp x τ)
               -> Const y (Extend l τ ρ)
        doCons _ _ = undefined