believe_me too demanding ?

[nicolabotta]

The following program

> module Test

> Blt : Nat -> Type
> Blt b = (n : Nat ** so (n < b))
> idx : Vect n alpha -> Blt n -> alpha
> idx {n = 0} Nil b impossible
> idx (a :: as) (Z ** _) = a
> idx {n = S m} (a :: as) (S k ** q) = idx {n = m} as (k ** believe_me oh)
> xdi : (p : alpha -> alpha -> Bool) ->
>       (a : alpha) ->
>       (as : Vect n alpha) -> 
>       so (elemBy p a as) ->
>       Blt n
> xdi p a as q = (fromMaybe Z (findIndex (p a) as) ** believe_me oh)
> toVect : {b : Nat} -> (Blt b -> a) -> Vect b a
> toVect {b = Z} _ = Nil
> toVect {b = S b'} {a = a} f = ((f (Z ** oh)) :: toVect f') where
>   f' : Blt b' -> a
>   f' (k ** q) = f (S k ** believe_me oh)  

> nColumns : Nat
> nColumns = S 4
> X : Nat -> Type
> X t = Blt nColumns

> p1 : X t -> Bool
> p2 : (n : Nat) -> X t -> Bool

> xsp : (t : Nat) -> (n : Nat) -> (i : Nat ** Vect i (X t))
> xsp t n = filter f xs where
>   f : (X t) -> Bool
>   f x = p1 x && p2 n x
>   xs : Vect nColumns (X t)
>   xs = toVect id
> nX : (t : Nat) -> (n : Nat) -> Nat 
> nX t n = getWitness (xsp t n)
> xs : (t : Nat) -> (n : Nat) -> Vect (nX t n) (X t)
> xs t n = getProof (xsp t n)
> index : (n : Nat) ->
>         (x : X t ** (so (p1 x), so (p2 n x))) -> 
>         Blt (nX t n)
> index {t} n xp = xdi p x (xs t n) (believe_me oh) where
>   p : X t -> X t -> Bool
>   p a b = getWitness a == getWitness b
>   x : X t
>   x = getWitness xp
> xedni : (n : Nat) ->
>         Blt (nX t n) -> 
>         (x : X t ** (so (p1 x), so (p2 n x)))
> xedni {t} n i = (x ** (r,v)) where
>   x : X t
>   x = idx (xs t n) i
>   r : so (p1 x)
>   r = believe_me oh
>   v : so (p2 n x)  
>   v = believe_me oh
> indexSpec : (n' : Nat) ->
>             (xp : (x : X t ** (so (p1 x), so (p2 n' x)))) -> 
>             xp = xedni n' (index n' xp)
> indexSpec n xp = believe_me oh

type checks with version 0.9.9.2 (bef8dce2d7d21538dd8448cab53d4097ffdbd39b) but with version 0.9.10 the last line

> indexSpec n xp = believe_me oh

triggers a (very long) "Can't convert" error. Any idea how to avoid this problem ?

My impression is that believe_me has become more (too ?) demanding in recent Idris versions: I can type check without problems all those components of our dynamic programming framework that rely on unimplemented specifications (meta-variables).

But virtually all attempts at building applications (which requires implementing or, more realistically, postulating the specifications through suspension of disbelief) do fail because of "Can't convert" errors.

[JanBessai]

Try

indexSpec n' xp = believe_me oh

with n' instead of n. Names matter, because type inference is based on a heuristic. If you don't like that, you'd have to annotate the target type of oh

[nicolabotta]

That works, thanks ! What conclusions can we draw from this example ? Are there naming rules which should be adopted where possible ? How would annotation of the target type of oh look like ?

[JanBessai]

What I found useful was:

• always try to match parameter names with the type signature.
• never use the same name for entities of different universes
• if it still fails, try to get all implicits into scope
• if nothing else works, gradually introduce typed let bindings that get more and more concrete until you find the problem

The renamed version would need: indexSpec n xp = let res : (xp = xedni n (index n xp)) = believe_me oh in res

Another problem you might encounter sooner or later is that Ord is hard to use in proofs. All the "evil bool" talk aside this is related to default definitions of cmp or <=, < etc. Idris doesn't know that they don't contradict each other and that things like (cmp m n == 0) -> (m <= n) are valid assumptions. Last time I tried, I was unable to proof this because default definitions are opaque as soon as they are instantiated for a concrete type. Skipping Bool I wrote https://github.com/idris-lang/Idris-dev/blob/master/lib/Decidable/Order.idr but it has issues that are not yet solved and was commented out.

[nicolabotta]

Very helpful, thanks a lot !

[JanBessai]

One more hint for conversion errors:

• when calling functions with implicit parameters try to explicitly pass all of them and clean them out one by one

[david-christiansen]

What's the status of this issue? Is it documenting the need for a better error message, or is it resolved?

[nicolabotta]

I do not know. In my view the key observation is Jan's remark:

Try

indexSpec n' xp = believe_me oh

with n' instead of n. Names matter, because type inference is based on a heuristic. If you don't > like that, you'd have to annotate the target type of oh

From a user's viewpoint I found it disturbing that

> indexSpec : (n' : Nat) -> (xp : (x : X t ** (so (p1 x), so (p2 n' x)))) -> xp = xedni n' (index n' xp)
> indexSpec n xp = believe_me oh

did not type check but

> indexSpec : (n' : Nat) -> (xp : (x : X t ** (so (p1 x), so (p2 n' x)))) -> xp = xedni n' (index n' xp)
> indexSpec n' xp = believe_me oh

did type check (I cannot confirm this behavior now: because of the "Could not find module `Data.Map.Strict'" I am not able to install the latest Idris version).

If this behavior is to be expected (or, for whatever reason, unavoidable), users should be warned, I think. Whether this can be better done via tutorial or through more perspicuous error messages I do not know.

[edwinb]

In fact this typechecks with any name other than n. The clash appears to be with the binding in the definition of Blt, which is definitely very odd. I don't see why this could even cause a problem, so I will obviously have to look more closely.

Certainly, the choice of name in the pattern should be irrelevant. Which means it's definitely a bug in the elaborator rather than a need for a better error message or better documentation.

[edwinb]

Oh. I have found the source of the name clash. Testing a fix now.

By the way, this doesn't work quite as the original pasted code, because there's a few places it can't infer the implicit argument t, notably in applications of p1 and p2. This is because 'X' isn't necessarily injective. I believe the behaviour now is correct.