Inequality of equals?

[nicolabotta]

The program

> import Data.Fin
> import Control.Isomorphism

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

> Finite : Type -> Type
> Finite A = DPair Nat (\ n => Iso A (Fin n))

> Finite1 : {A : Type} -> (P : A -> Type) -> Type
> Finite1 {A} P = (a : A) -> Finite (P a) 

> M : Type -> Type
> All : {A : Type} -> (P : A -> Type) -> M A -> Type
> Foo : (t : Nat) -> Type
> Bar : (t : Nat) -> (x : Foo t) -> Type
> foos : (t : Nat) -> (x : Foo t) -> (y : Bar t x) -> M (Foo (S t))
> Good : {t : Nat} -> (n : Nat) -> Foo t -> Type

> finAll : {A : Type} -> {P : A -> Type} -> Finite1 P -> (ma : M A) -> Finite (All P ma)
> finGood : {t : Nat} -> {n : Nat} -> (x : Foo t) -> Finite (Good {t} n x)

> finAllGood : {t : Nat} -> {n : Nat} -> 
>                 (x : Foo t) -> (y : Bar t x) -> 
>                 Finite (All (Good {t = S t} n) (foos t x y))
> finAllGood {t} {n} x y = finAll (finGood {t = S t} {n}) (foos t x y)

> {-

> FiniteAll : Type
> FiniteAll = {A : Type} -> {P : A -> Type} -> 
>             Finite1 P -> (ma : M A) -> Finite (All P ma)

> FiniteGood : Type
> FiniteGood = {t : Nat} -> {n : Nat} -> 
>              (x : Foo t) -> Finite (Good {t} n x)

> FiniteAllGood : Type
> FiniteAllGood = {t : Nat} -> {n : Nat} -> 
>                 (x : Foo t) -> (y : Bar t x) -> 
>                 Finite (All (Good {t = S t} n) (foos t x y))

> finiteAll : FiniteAll
> finiteGood : FiniteGood

> finiteAllGood : FiniteAllGood
> finiteAllGood {t} {n} x y = finiteAll (finiteGood {t = S t} {n}) (foos t x y)

> ---}

type checks fine. But uncommenting the comment block yields

- + Errors (1)
 `-- 3134_transparency.lidr line 48 col 14:
     When checking left hand side of finiteAllGood:
     t is not an implicit argument of Main.finiteAllGood

This seems to be an error given that the types of finAll and finiteAll, finGood and finiteGood and finAllGood and finiteAllGood are equal, I believe.

[edwinb]

Not quite. I'd expect this, because scoped implicits don't work the same way as top level implicits (laregely for historical reasons), and I haven't implemented the ability to fill in scoped implicits this way yet.

[nicolabotta]

Hmmm ... I am afraid I do not get the difference between scoped implicits and top level implicits.

To me it seems that t is an implicit parameter of finiteAllGood and that the problem here is just that

> finiteAllGood : FiniteAllGood

is not equivalent to

> finiteAllGood : {t : Nat} -> {n : Nat} -> 
>                 (x : Foo t) -> (y : Bar t x) -> 
>                 Finite (All (Good {t = S t} n) (foos t x y))

in spite of the fact that

> FiniteAllGood = {t : Nat} -> {n : Nat} -> 
>                 (x : Foo t) -> (y : Bar t x) -> 
>                 Finite (All (Good {t = S t} n) (foos t x y))

!