edit:我又跟进了一个具体问题 https://stackoverflow.com/questions/70088443/how-can-i-use-a-constraint-family-thats-in-scope-to-prove-instances-within-the。谢谢这里的回答者，我认为后续问题可以更好地解释我在这里引入的一些困惑。
TL;DR我正在努力将约束证明放入表达式中，同时在构造函数上使用具有存在约束的 GADT。 （这是一个严肃的口，对不起！）
我将问题归结为以下内容。我有一个简单的 GADT 来表示称为X和函数应用程序称为F。要点X被限制为Objects.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
Constrained指的是其对象受约束的容器某物 and Object就是它某物. (edit:我真正的问题涉及Category and Cartesian课程来自受限类别 https://hackage.haskell.org/package/constrained-categories-0.4.1.0)
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for ex
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
我想写一个表达式：
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex0 :: GADT ix String
ex0 = F show (X (3 :: Int))
虽然显而易见的解决方案有效，但在构建更大的表达式时它很快就会变得冗长：
-- Typechecks, but eventually verbose
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
我认为正确的解决方案应该是这样的：
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex2 :: Constrained ix => GADT ix String
ex2 = F show (X (3 :: Int))
但我还是拿不到证据Object ix Int.
我确信这比我想象的要简单。我尝试过添加约束Object约束族中GADT类实例。我尝试在表达式的签名中提供约束。我努力了QuantifiedConstraints，不过，我不确定我是否完全掌握了它。请各位聪明人帮助我！
可运行：
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
module Test where
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Const
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for instance
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
-- | A demo GADT that has function application ('F'), and points ('X'). The
-- points are constrained.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
-- -- Broken
-- -- error: Could not deduce: Object ix Int arising from a use of ‘X’
-- ex0 :: GADT ix String
-- ex0 = F show (X (3 :: Int))
-- Typechecks
-- but for larger programs becomes verbose, requiring many explicit constraints
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
-- -- What I want, but, it's broken
-- ex2 :: Constrained ix => GADT ix String
-- ex2 = F show (X (3 :: Int))
