eliminate term-level code

[LeanderK]

(I hope term-level is the right expression...). I have a HList:

data HList (ts :: [Type]) where
    HNil :: HList '[]
    (:&:) :: t -> HList ts -> HList (t ': ts)

infixr 5 :&:

And I want to write the following method:

length :: HList ts -> Sing (Length ts)

by not explicitly storing the length, but recursing on the HList(just like length for the normal list) and "reflecting it back to the type-level (withSomeSing)". Can I prove that this is correct (using eliminators)? I don't see a way to do this.

[RyanGlScott]

I think you might be over-complicating the problem a bit. Here are three ways you could write your length functions, none of which require the use of eliminators:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Bug where

import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List
import Data.Singletons.TypeLits

data HList :: [Type] -> Type where
  HNil  :: HList '[]
  (:&:) :: t -> HList ts -> HList (t:ts)
infixr 5 :&:

length1 :: SingI (Length ts) => HList ts -> Sing (Length ts)
length1 _ = sing

length2 :: forall (ts :: [Type]). SingI ts => HList ts -> Sing (Length ts)
length2 _ = sLength (sing @_ @ts)

length3 :: HList ts -> Sing (Length ts)
length3 HNil = SNat @0
length3 (_ :&: xs) = SNat @1 %:+ length3 xs

length3 could, conceivably, be rewritten to use an eliminator over HLists, but that would first require writing Sing/SingKind instances for HList and, well, doing so isn't pretty. So I'd avoid that if possible.

[LeanderK]

ah ok, that's enlightening 🙂 Edit: length3is what I want.