I'm using Idris 2 v0.3. I can't see why the compiler can't find an implementation for Gaussian of Distribution in
interface Distribution dist where
mean : dist -> Double
data Gaussian : Type where
MkGaussian : Double -> Gaussian
Distribution Gaussian where
mean (MkGaussian mean') = mean'
KnowledgeBased : Distribution d => (d : Type) -> Type
ei : KnowledgeBased Gaussian
I'm getting error
"src/Foo.idr" 12L, 459C written
Error: While processing type of ei. Can't find an implementation for Distribution ?d.
.../src/Foo.idr:12:6--12:29
|
12 | ei : KnowledgeBased Gaussian
| ^^^^^^^^^^^^^^^^^^^^^^^
Your scoping is wrong; in Distribution d => (d : Type) -> Type, the Distribution d part implicitly binds d, and then it is shadowed by d : Type.
Instead what you want is:
KnowledgeBased : (d : Type) -> Distribution d => Type
Here, the first d : Type binds d with a Pi; it parses as (d : Type) -> (Distribution d => Type). So the d in Distribution d is now bound, and no automatic implicit binding is done.
However, this is not idiomatic Idris. Instead, you should use the Distribution d-bound implicit parameter and not worry about tricks to make it explicit:
KnowledgeBased : Distribution d => Type
ei : KnowledgeBased {d = Gaussian}