I have a datatype that depends on a predicate P : a -> Type, meaning that some of its data constructors refer have an implicit P x as argument. I would like idris to be able to automatically infer this implicit. For this, I annotated the implicit with the keyword auto and I wrote a function isP : (x : a) -> Dec (P x) with a %hint annotation before the type declaration. Namely, something like:
module P
P : a -> Type
%hint
isP : (x : a) -> Dec (P x)
and in a separate file
module Main
import P
data Foo : Type where
Bar : (x : a) -> .{auto prf : P x} -> Foo
That said, I can't declare values of said Foo type because Idris claims the it can't infer prf.
Is this because prf has type P x instead of Dec (P x) or is it because the %hint flag does not get imported?
In either case, how can I get Idris to use a Dec value to try to find an implicit?
The %hint flag is imported, as you guess, it's because Dec (P x) is different than P x.
There's a trick though, you can use this datatype:
data IsYes : prop -> Type where
SoTrue : IsYes (Yes prop)
(basically, you define a type that holds a Yes for a given property)
and then you can use default instead of auto to check if the property holds:
data Foo : Type where
Bar : (x : a) -> .{default SoTrue prf : IsYes (isP x)} -> Foo
Note: with this trick, you don't even need %hint anymore, you just check the outcome of isP at compile time.