相关疑难解决方法(0)

我创建了一个使用GADT和DataKinds的问题的一个非常简单的例子.我的实际应用显然更复杂,但这清楚地捕捉了我的情况的本质.我正在尝试创建一个可以返回Test类型的任何值(T1,T2)的函数.有没有办法实现这一目标,还是我进入了依赖类型的领域？这里的问题看起来很相似,但我无法从他们那里找到(或理解)我的问题的答案.我刚开始理解这些GHC扩展.谢谢.

类似的问题1

类似的问题2

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, KindSignatures #-}

module Test where

data TIdx = TI | TD

data Test :: TIdx -> * where
  T1 :: Int -> Test TI
  T2 :: Double -> Test TD

type T1 = Test TI
type T2 = Test TD

prob :: T1 -> T2 -> Test TIdx
prob x y = undefined

----这是错误---- Test.hs:14:26:

Kind mis-match

The first argument of `Test' should have kind `TIdx',

but `TIdx' has kind `*'

In …