GHC TypeLits开销

Question

是否存在使用来自Sing的GHC.TypeLits的开销？例如，对于程序：

{-# 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部分只是类型系统噪声(你可以在马丁·苏兹曼、曼努埃尔·T·查克拉瓦蒂、西蒙·佩顿·琼斯和凯文·唐纳利的论文““具有相等矫顽力子的F系统””中读到它的含义)。相关引文：

Cast表达式没有操作效果，但它们可以向类型系统解释一种类型的值应该被视为另一种类型的值。

编辑:实际上，对于GHC7.6，装配代码 for test = fromSing (sing :: Sing 5)不同于test = 5代码，显然存在一些开销，但是这个问题似乎已经解决了。