GHC TypeLits overhead

Question

Is there any overhead of using Sing from GHC.TypeLits? For example for the program:

{-# LANGUAGE DataKinds #-}

module Test (test) where

import GHC.TypeLits

test :: Integer
test = fromSing (sing :: Sing 5)

GHC generates core code:

Test.test1 :: GHC.Integer.Type.Integer
[GblId,
 Str=DmdType,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Arity=0, Value=True,
         ConLike=True, WorkFree=True, Expandable=True,
         Guidance=IF_ARGS [] 100 0}]
Test.test1 = __integer 5

Test.test :: GHC.Integer.Type.Integer
[GblId,
 Str=DmdType,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Arity=0, Value=True,
         ConLike=True, WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(unsat_ok=True,boring_ok=True)}]
Test.test =
  Test.test1
  `cast` (<GHC.TypeLits.NTCo:SingI> <GHC.TypeLits.Nat> <5> ; (<GHC.TypeLits.TFCo:R:SingNatn
                                                                 <5>> ; <GHC.TypeLits.NTCo:R:SingNatn
                                                                           <5>>)
          :: GHC.TypeLits.SingI GHC.TypeLits.Nat 5
               ~#
             GHC.Integer.Type.Integer)

Is this code equivalent of Test.test = __integer 5 and value will be computed in compile time or not?

Answer 1

Yes, this is equivalent to Test.test = __integer 5, the cast part is just type system noise (you can read about what it means in the paper "System F with Type Equality Coercions" by Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones and Kevin Donnelly). Relevant quote:

Cast expressions have no operational effect, but they serve to explain to the type system when a value of one type should be treated as another.

Edit: Actually, with GHC 7.6 the assembly code for test = fromSing (sing :: Sing 5) is different from the code for test = 5 and apparently there actually is some overhead, but this issue seems to be fixed in HEAD.