CODEWITHSUNDEEP
dependent-typeidris
Rodrigo Ribeiro
Rodrigo Ribeiro

Reputation: 3218

Strange error message in Idris

I'm implementing in Idris the algorithm and proofs of first-order unification by structural recursion (current status of the development available here).

Idris in giving me the following error message

`-- UnifyProofs.idr line 130 col 60:
   When checking right hand side of maxEquiv with expected type
           (Max p n f -> Max q n f, Max q n f -> Max p n f)

   When checking argument b to constructor Builtins.MkPair:
           No such variable k

when it tries to type check the following function

maxEquiv : p .=. q -> Max p .=. Max q 
maxEquiv pr n f = ( \ a => ( fst (pr n f) (fst a) 
                          , \ n1 => \ g => \pr1 => (snd a) n1 g 
                                                   (snd (pr n1 g) pr1))
                  , \ a' => (snd (pr n f) (fst a') 
                          , \ n2 => \ g' => \ pr2 => (snd a') n2 g' 
                                                     (fst (pr n2 g') pr2)))

where Max and .=. are defined as

Property : (m : Nat) -> Type
Property m = (n : Nat) -> (Fin m -> Term n) -> Type

infix 5 .=.
(.=.) : Property m -> Property m -> Type
(.=.) {m = m} P Q = (n : Nat) -> (f : Fin m -> Term n) -> 
                                 Pair (P n f -> Q n f) 
                                      (Q n f -> P n f)

Max : (p : Property m) -> Property m
Max {m = m} p = \n => \f => (p n f , (k : Nat) -> (f' : Fin m -> Term k) -> 
                                                   p k f' -> f' .< f)

I've tried to pass all function arguments explicitly in order to avoid problems with implicit argument inference. But the error persists. Could someone provide me some tip on how can I solve this?

Upvotes: 1

Views: 87

Answers (1)

Rodrigo Ribeiro
Rodrigo Ribeiro

Reputation: 3218

Here is the solution to my question:

Max : (p : Property m) -> Property m
Max {m = m} p = \n => \f => (p n f , (k : Nat) -> (f' : Fin m -> Term k) -> p k f' -> f' .< f)

applySnd : Max {m = m} p n f -> (k : Nat) -> (f' : Fin m -> Term k) -> p k f' -> f' .< f
applySnd = snd

maxEquiv : p .=. q -> Max p .=. Max q 
maxEquiv pr n f = ( \ a => ( fst (pr n f) (fst a) 
                       , \ n1 => \ g => \pr1 => (applySnd a) n1 g (snd (pr n1 g) pr1))
              , \ a' => (snd (pr n f) (fst a
                        , \ n2 => \ g' => \ pr2 => (applySnd a') n2 g' (fst (pr n2 g') pr2)))

I just have used a function applySnd to make the same thing as snd. I do not know why this is necessary... Probably a Idris bug...

Upvotes: 0

Related Questions