GHC TypeLits Overhead

Question

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

 {-# LANGUAGE DataKinds #-} module Test (test) where import GHC.TypeLits test :: Integer test = fromSing (sing :: Sing 5) 

GHC generates kernel 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 to Test.test = __integer 5 , and will the value be computed at compile time or not?

Answer 1

Yes, this is equivalent to Test.test = __integer 5 , the cast part is just system noise (you can read about what this means in the document “System F with Enforcement of Equality of Types” by Martin Sulzman, Manuel M.T. Chakravarti, Simon Peyton Jones and Kevin Donnelly). Relevant quote:

Cast expressions have no effect, but they serve to explain the type system when you need to treat the value of one type as another.

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