CODEWITHSUNDEEP
idris
joel
joel

Reputation: 7868

Can't find implementation with constraint in signature

I have an interface that depends on another interface, with some dependent types, and I can't get the compiler to constrain a type in a related function

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

I get

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  
                             ^^^^^^^^^^^^^^^^^^^

How could this be?

If I use marginalise {marginal=Gaussian} {targets=1} model x it type checks, but I don't get why this isn't already determined by the type signature.

I don't think this qu I asked about the same area applies here

Upvotes: 0

Views: 178

Answers (1)

Cactus
Cactus

Reputation: 27626

I started writing this as a comment and realized halfway through that it might work as a full-blown answer.

Model 1 Gaussan m means that you have an implementation of the Model interface with targets = 1, marginal = Gaussian and model = m. Then, the let-binding of marginal requires Model a b m, i.e. an implementation of Model where targets = a , marginal = b and model = m. But there is no requirement that a = 1 and b = Gaussian!

My guess is that once you read up on determining parameters, you will discover that you want something like:

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

Upvotes: 1

Related Questions