带约束的循环类型

Question

{-# LANGUAGE GADTs, ScopedTypeVariables #-}

module Foo where

import Data.Proxy
import Data.Typeable

data HiddenType where
  Hidden :: (Typeable a) => Proxy a -> HiddenType

foo :: (i,HiddenType)
foo = (undefined, Hidden (Proxy::Proxy Int))

data Foo where
  Foo :: i -> Foo

bar :: Foo
bar = 
  let (x,h) = foo
  in case h of 
    (Hidden (p::Proxy i)) -> Foo (x :: i)

foo :: (Typeable i) => (i,HiddenType)

Foo.hs:20:15:
    No instance for (Typeable t0) arising from a use of ‘foo’
    The type variable ‘t0’ is ambiguous
    Relevant bindings include x :: t0 (bound at Foo.hs:20:8)
    Note: there are several potential instances:
      instance [overlap ok] Typeable ()
        -- Defined in ‘Data.Typeable.Internal’
      instance [overlap ok] Typeable Bool
        -- Defined in ‘Data.Typeable.Internal’
      instance [overlap ok] Typeable Char
        -- Defined in ‘Data.Typeable.Internal’
      ...plus 14 others
    In the expression: foo
    In a pattern binding: (x, h) = foo
    In the expression:
      let (x, h) = foo
      in case h of { (Hidden (p :: Proxy i)) -> Foo (x :: i) }

Foo.hs:22:35:
    Couldn't match expected type ‘a’ with actual type ‘t0’
      because type variable ‘a’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a pattern with constructor
        Hidden :: forall a. Typeable a => Proxy a -> HiddenType,
      in a case alternative
      at Foo.hs:22:6-24
    Relevant bindings include
      p :: Proxy a (bound at Foo.hs:22:14)
      x :: t0 (bound at Foo.hs:20:8)
    In the first argument of ‘Foo’, namely ‘(x :: i)’
    In the expression: Foo (x :: i)
Failed, modules loaded: none.

bar :: Foo
bar = 
  let (x :: i,h) = foo
      (Hidden (p::Proxy i)) = h
  in Foo x

这将使约束在范围内，为foo提供额外的参数。这里我的意图是h包含一些（隐藏的）具体类型i，它应该用作多态函数GHC compulins的具体类型：

Foo.hs:19:8:
    You cannot bind scoped type variable ‘i’
      in a pattern binding signature
    In the pattern: x :: i
    In the pattern: (x :: i, h)
    In a pattern binding:
      (x :: i, h) = foo

Foo.hs:20:8:
    My brain just exploded
    I can't handle pattern bindings for existential or GADT data constructors.
    Instead, use a case-expression, or do-notation, to unpack the constructor.
    In the pattern: Hidden (p :: Proxy i)
    In a pattern binding: (Hidden (p :: Proxy i)) = h
    In the expression:
      let
        (x :: i, h) = foo
        (Hidden (p :: Proxy i)) = h
      in Foo x

我的用例的假设是1。foo同时计算i和hiddentype2。隐藏类型的值涉及（至少部分）第一个元组元素的计算。这意味着我不想在bar中调用foo两次（一次是获取hiddentype，一次是使用该类型绑定第一个元组元素）。在foo存在约束的情况下，是否有某种方法使bar的定义成为可能？

Answer 1

我认为问题是foo的返回值实际上不是多态的。foo本身是多态的，但返回的值必须存在于特定类型中。不幸的是，您要使用的类型还不可用，并且由于循环引用，无法将其带入foo的调用站点的作用域中。如果我们把foo在伪核心中的定义写出来，问题就很清楚了：

foo (@ iType) _ = (undefined @ iType, HiddenType...)

这里的@itype是一个类型参数。在获得hiddenType之前，我们需要首先执行foo的类型应用程序（以及未使用的字典应用程序），因此没有办法使其原样工作。

幸运的是，有一种方法可以让ghc相信foo应该返回一个实际的多态值：

{-# LANGUAGE GADTs, ScopedTypeVariables #-}
{-# LANGUAGE ImpredicativeTypes #-}

module Foo where

import Data.Proxy
import Data.Typeable

data HiddenType where
  Hidden :: (Typeable a) => Proxy a -> HiddenType

foo :: (forall i. Typeable i => i,HiddenType)
foo = (undefined, Hidden (Proxy::Proxy Int))

data Foo where
  Foo :: i -> Foo

bar = 
  let (x,h) = foo
  in case h of
    Hidden p -> Foo (x `asProxyTypeOf` p)

list1 :: forall t. Typeable t => [t]

list2 :: [forall t. Typeable t => t]

它不是一个常用的扩展，但偶尔会有用。

foo的非谓词版本的核心也有点不同：

foo = (\(@ iType) _ -> undefined @ iType, HiddenType...)

您可以看到，如果您向let添加批注，则这允许x根据需要是多态的：

bar :: Foo
bar = 
  let (x :: forall i. Typeable i => i,h) = foo
  in case h of
    Hidden p -> Foo (x `asProxyTypeOf` p)