Constraining a function type with an Idris interface

Question

I'd like to create a function with type constrained by an interface. My intention is to build a simple monoid solver using VerifiedMonoid defined inClasses.Verified module from contrib package.

Idris gives me the following error:

 Monoid-prover.idr line 29 col 5:
 When checking type of MonoidProver.eval:
 Can't find implementation for VerifiedMonoid a

for the type signature of eval:

eval : VerifiedMonoid a => Expr n -> Env a n -> a

Am I doing something silly or missing something? Such constrained types (like eval's type) can be interpreted like Haskell's types?

The complete code is shown below.

module MonoidProver

import Classes.Verified

import Data.Fin
import Data.Vect

%default total

infixl 5 :+:

data Expr : Nat -> Type where
   Var  : Fin n -> Expr n
   Id   : Expr n
   (:+:) : Expr n -> Expr n -> Expr n

Env : VerifiedMonoid a => (a : Type) -> Nat -> Type
Env a n = Vect n a

eval : VerifiedMonoid a => Expr n -> Env a n -> a
eval (Var i) env    = index i env
eval Id      env    = neutral
eval (e :+: e') env = eval e env <+> eval e' env

I think your type signature for Env scopes a wrongly: I think the type you've given is equivalent to Env : VerifiedMonoid a => (b : Type) -> Nat -> Type. Also, what does the VerifiedMonoid constraint on Env supposed to buy you? If you remove it from Env's signature, your code typechecks. — Cactus

Peter Amidon Peter Amidon · Accepted Answer · 2016-08-22T17:00:12

As @Cactus mentioned in a comment, the problem here is that the type signature for Env is not correct. Specifically, since the constraint is on the value of the argument, it is a dependent (pi) type, and Idris enforces that dependent types go left-to-right (be introduced before they are used). My understanding is that basically the compiler will see the argument x : a as being shorthand for $\Pi_{(x\;:\;a)}B(x)$ , where $B(x)$ is the part of the type signature to the right of the quantifier. This means that (a : Type) actually binds a fresh a, which is not the same a that was used in the VerifiedMonoid a constraint (which is implicitly universally bound).

Luckily, since Idris isn't Haskell (where all type class constraints must be at the head of the type signature), this is easy to fix: just change your type signature to Env : (a : Type) -> VerifiedMonoid a => Nat -> Type, so that a is bound before it is used!

Constraining a function type with an Idris interface

1 Answers