How to use lists with the Haskell singletons library?

Question

I'm trying to make a type using the singletons library where I use a list:

import Data.Singletons.TH (singletons)

$(singletons [d|

    data LLVMType
        = IntegerType
        | FloatType
        | FunctionType { argumentTypes :: [LLVMType] }

    |])

foo :: SLLVMType ('FunctionType '[ 'IntegerType ])
foo = ???

I tried to make foo be: SFunctionType [SIntegerType], however it results in this error:

• Couldn't match expected type ‘Data.Singletons.Sing '['IntegerType]’
              with actual type ‘[Data.Singletons.Sing 'IntegerType]’
• In the first argument of ‘SFunctionType’, namely ‘[SIntegerType]’
  In the expression: SFunctionType [SIntegerType]
  In an equation for ‘foo’: foo = SFunctionType [SIntegerType]

How do I make an expression for foo that typechecks? Or how can I achieve this in another way?

Github repo with the code.

Answer 1

You're very close, but you need to use list singletons.

{-# language TemplateHaskell, DataKinds, GADTs, TypeFamilies #-}
module SingList where

import Data.Singletons.TH (singletons)
import Data.Singletons.Prelude.List (Sing (SNil, SCons))

$(singletons [d|

    data LLVMType
        = IntegerType
        | FloatType
        | FunctionType { argumentTypes :: [LLVMType] }

    |])

foo :: SLLVMType ('FunctionType '[ 'IntegerType ])
foo = SFunctionType (SCons SIntegerType SNil)