通过 SomeNat 上的模式匹配产生的类型变量的范围是什么？

Question

我无法理解此代码的原因：

-- someNatVal test case
--
-- David Banas <capn.freako@gmail.com>
-- August 5, 2018

{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import GHC.TypeLits
import Data.Proxy

tellNat :: forall n. KnownNat n => Integer
tellNat = natVal (Proxy :: Proxy n)

foo :: Integer -> Integer
foo n =
  let SomeNat (_ :: Proxy m) =
        fromMaybe (error "Negative Nat!") (someNatVal n)
   in tellNat @m

main :: IO ()
main = print $ foo 1 == 1

产生此编译错误：

[1 of 1] Compiling Main ( someNatValTest.hs, someNatValTest.o )

someNatValTest.hs:22:16: error: Not in scope: type variable ‘m’

根据@Carl，此代码：

{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import GHC.TypeLits
import Data.Maybe
import Data.Proxy

tellNat :: forall n. KnownNat n => Integer
tellNat = natVal (Proxy :: Proxy n)

foo :: Integer -> Integer
foo n =
  case n' of
    SomeNat (_ :: Proxy m) ->
      tellNat @m
  where n' = fromMaybe (error "Negative Nat!") (someNatVal n)

main :: IO ()
main = print $ foo 1 == 1

作品：

dca9047d694f:tmp a594349$ stack runghc someNatValTest.hs
True

Answer 1

有趣 - 如果您尝试类似的操作，GHC 通常会告诉您它的大脑爆炸了。我想在你的情况下，SomeNat 只是一个存在的，而不是真正的 GADT，因此你不会收到有趣的错误消息。

无论如何，如果要访问隐藏在数据类型中的类型，则需要将构造函数与 case 表达式而不是 let 匹配。

通过 SomeNat 上的模式匹配产生的类型变量的范围是什么？

What is the scope of a type variable brought into existence by pattern matching on SomeNat?

haskell

types

existential-type

type-level-computation