在签名中找不到具有约束的实现

Question

我有一个依赖于另一个接口的接口，具有一些依赖类型，我无法让编译器在相关函数中约束一个类型

import Data.Vect

interface Distribution (0 event : Nat) (dist : Nat -> Nat -> Type) where

data Gaussian : Nat -> Nat -> Type where

Distribution e Gaussian where

interface Distribution targets marginal =>
 Model (targets : Nat) (marginal : Nat -> Nat -> Type) model where
  marginalise : model -> Vect s Double -> marginal targets s

foo : m -> Model 1 Gaussian m => Vect s Double -> Nat
foo model x = let marginal = marginalise model x in ?rhs

我明白了

While processing right hand side of foo. Can't find an implementation for Model ?targets ?marginal m.

foo model x = let marginal = marginalise model x in ?rhs  
                             ^^^^^^^^^^^^^^^^^^^

这怎么可能？

如果我使用 marginalise {marginal=Gaussian} {targets=1} model x 它会进行类型检查，但我不明白为什么这还没有由类型签名确定。

我不认为this qu我问过同样的领域适用于这里

Answer 1

我开始写这篇评论作为评论，并在中途意识到它可能作为一个完整的答案。

Model 1 Gaussan m 表示您有一个带有targets = 1、marginal = Gaussian 和model = m 的Model 接口的实现。然后，marginal 的 let 绑定需要Model a b m，即Model 的实现，其中targets = a、marginal = b 和model = m。但是没有要求a = 1和b = Gaussian！

我的猜测是，一旦你阅读了determining parameters，你会发现你想要这样的东西：

interface Distribution targets marginal =>
 Model (targets : Nat) (marginal : Nat -> Nat -> Type) model | model where