如何从作用域内的约束族推导Haskell的typeclass实例？

编辑：我已发布了更具体的后续问题，感谢各位答主，后续问题能更好地解释我在此处引入的一些混淆。

概要 #

我在使用构造函数带存在性约束的GADT时，无法将约束证明引入表达式中。（这个表述非常拗口，抱歉！）

我把问题简化为如下场景：我定义了一个简单的GADT，其中X构造子表示点，F构造子表示函数应用，X构造子的参数要求满足Object约束。

data GADT ix a where
  X :: Object ix a => a -> GADT ix a
  F :: (a -> b) -> GADT ix a -> GADT ix b

Constrained指代内部元素受某种条件约束的容器，Object就是对应的约束条件。*编辑：*我实际遇到的问题涉及constrained-categories库中的Category和Cartesian类。

-- | 我可以对kind为`* -> *`的容器内部的值添加约束
class Constrained (ix :: * -> *) where
  type Object ix a :: Constraint

-- | 这里是一个简化的约束示例，更复杂的约束可能会包含`Typeable a`之类的条件
instance Constrained (GADT ix) where
  type Object (GADT ix) a = (Constrained ix, Object ix a)

我想要编写如下表达式：

-- 报错：无法推导：使用‘X’时需要满足的 Object ix Int 约束
ex0 :: GADT ix String
ex0 = F show (X (3 :: Int))

虽然最直接的解决方案可以通过类型检查，但构建更复杂的表达式时，约束声明会变得非常冗长：

-- 可以通过类型检查，但如果程序规模变大，需要显式声明的约束会非常多
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))

我认为理想的解决方案应该是如下形式，但依然无法通过编译：

-- 报错：无法推导：使用‘X’时需要满足的 Object ix Int 约束
ex2 :: Constrained ix => GADT ix String
ex2 = F show (X (3 :: Int))

但我还是没法获得Object ix Int的证明。我相信问题的解法比我想得更简单，我已经尝试过在GADT的类实例中为Object约束族添加约束、在表达式签名中声明约束、使用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

-- | 我可以对kind为`* -> *`的容器内部的值添加约束
class Constrained (ix :: * -> *) where
  type Object ix a :: Constraint

-- | 这里是一个简化的约束示例，更复杂的约束可能会包含`Typeable a`之类的条件
instance Constrained (GADT ix) where
  type Object (GADT ix) a = (Constrained ix, Object ix a)

-- | 示例GADT，支持函数应用（'F'）和点值（'X'），其中点值带约束
data GADT ix a where
  X :: Object ix a => a -> GADT ix a
  F :: (a -> b) -> GADT ix a -> GADT ix b

-- -- 无法编译
-- -- 报错：无法推导：使用‘X’时需要满足的 Object ix Int 约束
-- ex0 :: GADT ix String
-- ex0 = F show (X (3 :: Int))

-- 可正常通过类型检查
-- 但如果程序规模变大，需要显式声明的约束会非常多
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))

-- -- 我期望的写法，但无法编译
-- ex2 :: Constrained ix => GADT ix String
-- ex2 = F show (X (3 :: Int))

内容的提问来源于stack exchange，提问作者Josh.F