這個遞回定義T無法進行型別檢查。
class C a where
type T a :: Type
newtype Compose (f :: Type -> Type) (g :: Type -> Type) (a :: Type) = Compose {getCompose :: f (g a)}
instance C (Maybe a) where
type T (Maybe a) = NP (Compose T Identity) '[a]
具體錯誤：
? The associated type family ‘T’ should have 1 argument, but has been given none
? In the type instance declaration for ‘T’
In the instance declaration for ‘C (Maybe a)’
|
32 | type T (Maybe a) = NP (Compose T Identity) '[a]
| ^
- 為什么 GHC 無法做到這一點？
- 有解決方法嗎？
真正的類/實體如下所示：
instance Ema (MultiSite models) where
type RouteFor (MultiSite models) = NP (Compose RouteFor Site) models
這表示“多站點的路由是各個站點的路由的 n 元乘積”，因此RouteFor必須遞回定義。
uj5u.com熱心網友回復：
型別族是無法匹配的，必須完全飽和。這意味著它們不能部分作為引數傳遞。這基本上是錯誤訊息所說的
? 關聯的型別族“
T”應該有 1 個引數，但沒有給出
目前，這在種類級別上沒有區別（參見不飽和型別家庭提案），但在 GHC 中存在非常明顯的區別。
根據:kind兩者T和Identity具有相同的種類，而實際上Identity是可匹配的并且T是不可匹配的：
Identity :: Type -> @M Type
T :: Type -> @U Type
因為 are 的引數Compose不能Type -> @M Type傳遞不匹配的型別族。型別語言是第一順序！（Haskell 中的高階型別級編程）并且目前無法定義Compose接受無法匹配的函式。
如果您比較稍加修改的T1and的種類T2，第一個在兩個引數中都不匹配，而第二個在其第二個引數中是可匹配的
type C1 :: Type -> @M Constraint
class C1 a where
-- T1 :: Type -> @U Type -> @U Type
type T1 a (b :: Type) :: Type
type C2 :: Type -> @M Contraint
class C2 a where
-- T2 :: Type -> @U Type -> @M Type
type T2 a :: Type -> Type
一種可能性是將其包裝在（可匹配的）新型別中
type Wrapp'T :: Type -> @M Type
newtype Wrapp'T a = Wrapp'd (T a)
instance C (Maybe a) where
type T (Maybe a) = NP (Compose Wrapp'T Identity) '[a]
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/427270.html