Is the %hint annotation imported/Dec and auto annotation?

Question

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?

Nicolas Nicolas · Accepted Answer · 2019-04-23T06:46:50

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.

Is the %hint annotation imported/Dec and auto annotation?

1 Answers