A sketch of how we might single visible type applications

SingletonsVTA.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SingletonsVTA where

import Data.Kind

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (f :: a ~> b) @@ (x :: a) :: b

type Sing :: forall k. k -> Type
data family Sing

newtype instance Sing (f :: k1 ~> k2) =
  SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }
type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t. Sing t -> SingFunction1 (f @@ t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))

data instance Sing :: forall a. [a] -> Type where
  SNil  :: Sing '[]
  SCons :: Sing x -> Sing xs -> Sing (x:xs)

constBA :: forall b a. a -> b -> a
constBA x _ = x

type ConstBA :: forall b a. a -> b -> a
type family ConstBA x y where
  ConstBA x _ = x

type ConstBASym0 :: forall b a. a ~> b ~> a
data ConstBASym0 x
type instance ConstBASym0 @@ x = ConstBASym1 x

type ConstBASym1 :: forall b a. a -> b ~> a
data ConstBASym1 x y
type instance ConstBASym1 x @@ y = ConstBA x y

sConstBA :: forall b a (x :: a) (y :: b).
            Sing x -> Sing y -> Sing (ConstBASym0 @@ x @@ y :: a)
sConstBA sx _ = sx

blah :: forall b a. [a] -> [b -> a]
blah x = map (constBA @b) x

type Map :: forall a b. (a ~> b) -> [a] -> [b]
type family Map f xs where
  Map _ '[]    = '[]
  Map f (x:xs) = (f @@ x) : Map f xs

sMap :: forall a b (f :: a ~> b) (xs :: [a]).
        Sing f -> Sing xs -> Sing (Map f xs :: [b])
sMap _  SNil         = SNil
sMap sf (SCons x xs) = (sf @@ x) `SCons` sMap sf xs

type Blah :: forall b a. [a] -> [b ~> a]
type family Blah x where
  Blah @b x = Map (ConstBASym0 @b) x

type BlahSym0 :: forall b a. [a] ~> [b ~> a]
data BlahSym0 x
type instance BlahSym0 @@ x = Blah x

sBlah :: forall b a (x :: [a]). Sing x -> Sing (BlahSym0 @@ x :: [b ~> a])
sBlah sx = sMap (singFun2 @(ConstBASym0 @b) sConstBA) sx