Type mismatch in DPair proof argument

[nicolabotta]

The program (inspired by a post by J. T. Errington on Idris-lang):

> import Data.Fin
> import Syntax.PreorderReasoning

> %default total
> %access public export
> %auto_implicits on

> foo :  (n : Nat) -> LTE n m -> Fin (S m)
> foo  Z     LTEZero    = FZ
> foo (S n) (LTESucc p) = FS (foo n p)

> bar : (m : Nat) -> Fin (S m) -> DPair Nat (\ n => LTE n m)
> bar  _     FZ    = (Z ** LTEZero)
> bar  Z    (FS k) = FinZElim k
> bar (S m) (FS k) = (S (fst (bar m k)) ** LTESucc (snd (bar m k)))

> barFooLemma : (m : Nat) -> (n : Nat) -> (p : LTE n m) -> bar m (foo n p) = (n ** p)
> barFooLemma  _     Z     LTEZero    = Refl
> barFooLemma (S m) (S n) (LTESucc p) = 
>     ( bar (S m) (foo (S n) (LTESucc p)) )
>   ={ Refl }=
>     ( bar (S m) (FS (foo n p)) )
>   ={ Refl }=
>     ( (S (fst (bar m (foo n p))) ** LTESucc (snd (bar m (foo n p)))) )
>   ={ ?kuka }= 
>     ( (S (fst (n ** p)) ** LTESucc (snd (n ** p))) )
>   ={ ?kika }=
>     ( (S n ** LTESucc p) )
>   QED

fails to type check with

- + Errors (1)
 `-- ./issues/finToNat.lidr line 26 col 42:
     When checking right hand side of barFooLemma with expected type
             bar (S m) (foo (S n) (LTESucc p)) = (S n ** LTESucc p)

     When checking argument pf to constructor Builtins.MkDPair:
             Type mismatch between
                     LTE n m (Type of p)
             and
                     P n (Expected type)

Is this the expected behavior? What is P in the error message?

[ahmadsalim]

@nicolabotta The error is that it can not infer the type of (n ** p) in ( (S (fst (n ** p)) ** LTESucc (snd (n ** p))) ) and it works if you explicitly annotate the type as such:

( (S (fst (the (n : Nat ** LTE n m) (n ** p))) ** LTESucc (snd (the (n : Nat ** LTE n m) (n ** p))) ))

P is from the definition of dependent pairs. I agree that the error message could be improved, but I will close this one since we have many similar issues reported.

[nicolabotta]

I find it very strange that Idris cannot infer the type of (n ** p) given that the types of n and of p are fully determined. Is this a duplication of which open issue?

[ahmadsalim]

@nicolabotta E.g. #3620 , but I think there is a general issue with error messages in Idris regarding variables in error messages that are not directly given by the user. I am not very familiar with the inference mechanism in Idris, so I am unsure why the given example can not be inferred, but note that it's hard to infer the precise types for dependent pairs in general even one know the types of the components e.g. what is the type of:

(true ** S Z)

There are infinite types one could give, e.g.:

(b : Bool ** Nat)
(b : Bool ** if b then Nat else Bool)
(b : Bool ** if b then Nat else Void)
(b : Bool ** ComplexType b n m)      -- n and m are some context dependent variables

[nicolabotta]

Thanks Ahmad but I am not sure that solving #3620 would also solve the current issue. On the problem of deducing the type of DPair values: I understand that this is difficult in general but in the specific case the type of (n ** p) seems to be fully determined by :t n = Nat and :t (LTESucc p) = LTE (S n) (S m). This information and the type of LTESucc should be enough to deduce :t (n ** p) = DPair Nat (\ n => LTE n m), it seems to me.

[ahmadsalim]

@nicolabotta The duplicate was of the error message. I am not sure the inference issue is solveable, since there are many possible types still one could given, the following could also be possible:

DPair Nat (\n => P n m)

P Z m  = Void
P (S n) = LTE (S (S n)) (S (S m))

I understand that writing type annotations is not fairly nice, but I think that is the only consistent and sound way we know to solve this issue for now. I would of course love a better inference algorithm myself, but I think that that would be beyond this issue in terms of description.

[nicolabotta]

I am probably missing something obvious but it does not seem to me that the type of (h ** p) could be DPair Nat (\n => P n m). At least, the annotated version does not type check with P as above. It seems to me that there is really only one P : Nat -> Nat -> Type that makes P n m equal to LTE n m for every m and n. Also, the error message seems to suggest that the type checker does deduce the type of p correctly but expects a more general type. No matter, I have no problem with the annotated version but we need an error message that tells us what to annotate, I guess. Best, Nicola