GHC TypeLits Overhead

Question

Gibt es einen Overhead von von GHC.TypeLits? Zum Beispiel für das Programm:

{-# LANGUAGE DataKinds #-} 

module Test (test) where 

import GHC.TypeLits 

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

GHC erzeugt Kern-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) 

Ist dieser Code äquivalent Test.test = __integer 5 und Wert wird in der Kompilierung oder nicht berechnet werden?

Answer 1

Ja, dies ist äquivalent zu Test.test = __integer 5, der cast Teil Lärm nur Typ-Systems ist (man kann darüber lesen, was es bedeutet, in dem Papier "System F with Type Equality Coercions" von Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones und Kevin Donnelly). Relevante Zitat:

Guss Ausdrücke haben keine operative Wirkung, aber sie dienen dazu, den Typ System erklären, wenn ein Wert eines Typs soll als andere behandelt werden.

Edit: Eigentlich mit GHC 7.6 die assembly code für test = fromSing (sing :: Sing 5) für test = 5 aus dem Code anders ist und anscheinend gibt tatsächlich ist einige Overhead, aber dieses Problem scheint in HEAD fixiert werden.