Say I have the following interface in idris:

interface I a b where
  x : a
  y : b

And then I try to define the following function:

x' : I a b => a
x' = x

But then I get this error:

Error: While processing right hand side of x'. Can't find an implementation for I a ?b.

Main:06:6--06:7
 02 |   x : a
 03 |   y : b
 04 | 
 05 | x' : I a b => a
 06 | x' = x
           ^

How do I specify to idris that x is the x from I a b and not the x from I a ?b?

Say I have the following interface in idris:

interface I a b where
  x : a
  y : b

And then I try to define the following function:

x' : I a b => a
x' = x

But then I get this error:

Error: While processing right hand side of x'. Can't find an implementation for I a ?b.

Main:06:6--06:7
 02 |   x : a
 03 |   y : b
 04 | 
 05 | x' : I a b => a
 06 | x' = x
           ^

How do I specify to idris that x is the x from I a b and not the x from I a ?b?

• interface
• idris
• idris2

1 Answer 1

Found the answer! b is essentially an implicit argument to x so you can set it just like you would for a function:

x' : I a b => a
x' = x { b = b }