GHC TypeLitsオーバーヘッド

Question

GHC.TypeLitsからSingを使用するオーバーヘッドはありますか？たとえば、プログラムの：

{-# LANGUAGE DataKinds #-} 

module Test (test) where 

import GHC.TypeLits 

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

GHCは、コアコードを生成する：

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) 

はTest.test = __integer 5と値のこのコードの等価物は、コンパイル時に、またはしない計算されますか？

Answer 1

はい、これはTest.test = __integer 5に相当し、cast一部は（あなたはそれがマーティンSulzmann、マヌエル・M. T. Chakravarty、サイモンペイトンジョーンズとケビン・ドネリーによって紙"System F with Type Equality Coercions"に何を意味するのかについて読むことができます）だけのタイプのシステムノイズです。関連引用：1型の値が別として 扱われるべき時に型システムへの説明

キャスト式はなし作用効果を持っているが、彼らは に仕えます。

編集：test = fromSing (sing :: Sing 5)ためassembly codeが明らかに存在しtest = 5ためのコードとは異なるとされGHC 7.6で実際には、実際には、いくつかのオーバーヘッドですが、この問題はHEADで修正されるようです。