An iso between Sing xs and Rec Sing xs

gistfile1.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE GADTs  #-}
{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE LambdaCase  #-}
{-# LANGUAGE TemplateHaskell  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE StandaloneDeriving  #-}
--{-# LANGUAGE AllowAmbiguousTypes  #-}

module VinylTest where
import Data.Singletons
import Data.Singletons.Prelude hiding (Head)
import Data.Singletons.TH
import Data.Typeable
import Data.Vinyl hiding (Dict)
import Data.Vinyl.TypeLevel
import Data.Vinyl.Functor
import qualified Data.Constraint as D
import GHC.Exts
import Data.Function
import Control.Lens
import Data.Constraint
import Data.Constraint.Unsafe

type family AllU (xs :: [u]) (c :: u -> Constraint) :: Constraint where
  AllU '[] c = ()
  AllU (r ':  rs) c = (c r, AllU rs c)

-- A helper to use the AllU constraint to build a Rec
class BuildRec xs where
  buildRec :: AllU xs SingI => Rec Sing xs

instance (SingI x, BuildRec xs) => BuildRec (x ': xs) where
  buildRec = sing :& buildRec

instance BuildRec '[] where
  buildRec = RNil

-- Two ways to make defaults

-- Using AllU
defaultRec1 :: forall xs
             . ( AllU xs SingI
               , BuildRec xs
               )
            => Rec Sing xs
defaultRec1 = buildRec

-- Using Sing xs
defaultRec :: SingI xs => Rec Sing xs
defaultRec = singToRec sing

-- An isomorphism between Sing xs and Rec Sing xs
singRec :: Iso (Sing xs) (Sing ys) (Rec Sing xs) (Rec Sing ys)
singRec = iso singToRec recToSing

singToRec :: Sing xs -> Rec Sing xs
singToRec = \case 
  SNil       -> RNil
  SCons x xs -> x :& singToRec xs

recToSing :: Rec Sing xs -> Sing xs
recToSing = \case 
  RNil    -> SNil
  r :& rs -> SCons r (recToSing rs)

-- Test
singletons [d| data Field = A | B | C 
                 deriving (Show)
             |]
             
instance Show (Sing A) where show _ = "A"
instance Show (Sing B) where show _ = "B"
instance Show (Sing C) where show _ = "C"   
             
data Semantics :: Field -> * where
  SemA :: Int    -> Semantics A
  SemB :: Double -> Semantics B
  SemC :: Bool   -> Semantics C

test :: Rec Sing '[A, B, C]
test = defaultRec1

test1 = show test