Implementation arguments containing injective functions

[nicolabotta]

The program

> LTB : Nat -> Type
> LTB b = DPair Nat (\ n  => LT n b)

> implementation Uninhabited (LTB Z) where
>   uninhabited (MkDPair n prf) = absurd prf

type checks fine in 0.99.1-git:PRE. But with 1.0 one gets

- + Errors (1)
 `-- ./BoundedNat/issues/implemantation.lidr line 4 col 17:
     (n : Nat **
      LTE (S n) 0)  cannot be a parameter of Prelude.Uninhabited.Uninhabited
     (Implementation arguments must be type or data constructors)

which seems like an Idris error given that LTB Z is indeed a type.

[ahmadsalim]

@nicolabotta I believe this was previously a bug, which is now fixed. I believe the general idea is that one should not be able to write implementations that work on functions instead of type constructors.

[nicolabotta]

I am not sure that I understand what you mean, here LTB Z is a legal type, not a function. I am also not aware of any report in which the pre-1.0 behavior was identified as being erroneous.

This late change in Idris breaks tons of legacy code and effectively makes types that are not introduced via data declarations second-class types. From a user's perspective, this is very annoying and rather pointless.

What have we gained through this new limitation?

[ahmadsalim]

As far as I understand, the mechanism was only guaranteed to work with type and data constructors, because they guarantee injectivity. I think there were some issues with the old approach, which was fixed prior to the release of 1.0. For more details, I think you need to ask Edwin, since I do not completely understand the implementation search mechanism of Idris myself.

[nicolabotta]

Thanks Ahmad, for the time being I will go back to 0.99 and try to see if I can make the framework 1.0 compatible.

[edwinb]

Yes, this is correct. I hadn't realised there was code out there which exploited this bug but I'll see if I can think of a way to deal with this kind of implementation.

The problem with this kind of implementation constraint is that unification is not fancy enough to deal with it. Maybe the thing to do is revisit unification.

[ahmadsalim]

@nicolabotta I think you can use instead:

> implementation Uninhabited (DPair Nat (\ n  => LT n Z)) where
>   uninhabited (MkDPair n prf) = absurd prf

It's a bit more ugly, but should work.

[nicolabotta]

Hmmm ... it does not seem to work with 1.0-git:981b014:

> implementation Uninhabited DPair Nat (\ n  => LT n Z) where
>   uninhabited (MkDPair n prf) = absurd prf

yields

- + Errors (1)
 `-- ./BoundedNat/issues/implementation.lidr line 1 col 17:
     When checking type of Main.DPair, Nat, \n => LT n 0 implementation of Prelude.Uninhabited.Uninhabited:
     When checking argument t to type constructor Prelude.Uninhabited.Uninhabited:
             Type mismatch between
                     (a : Type) -> (a -> Type) -> Type (Type of DPair)
             and
                     Type (Expected type)

and

> implementation Uninhabited (DPair Nat (\ n  => LT n Z)) where
>   uninhabited (MkDPair n prf) = absurd prf

yields

- + Errors (1)
 `-- ./BoundedNat/issues/implementation.lidr line 1 col 17:
     (n : Nat **
      LTE (S n) 0)  cannot be a parameter of Prelude.Uninhabited.Uninhabited
     (Implementation arguments must be type or data constructors)

[ahmadsalim]

@nicolabotta I forgot the paranthesis in my initial comment, but I had corrected it a second later.
However, if you read this from the mail, you may not have gotten the edit, so please try:

> implementation Uninhabited (DPair Nat (\ n  => LT n Z)) where
>   uninhabited (MkDPair n prf) = absurd prf

[nicolabotta]

@ahmadsalim Thanks, I realized that but also the parenthesized version does not type check with 1.0-git:981b014:

- + Errors (1)
 `-- ./BoundedNat/issues/implementation.lidr line 1 col 17:
     (n : Nat **
      LTE (S n) 0)  cannot be a parameter of Prelude.Uninhabited.Uninhabited
     (Implementation arguments must be type or data constructors)

[ahmadsalim]

@nicolabotta Ah, sorry, I accidentally tested this on 0.99. Yeah, this does seem like an issue.

[nicolabotta]

@ahmadsalim Thanks Ahmad! I am then going back to 0.99 for the time being. Hope that interfaces will be fixed soon. Best, Nicola

[nicolabotta]

Would it be possible to come up with an authoritative decision on this issue? The issue is labelled as A-Confirmed and C-Moderate Effort but the last exchange I had with Edwin on the subject (in Aug. 2017) suggests that the error might actually be difficult to eradicate. I see two possibilities:

1. Decide that, from Idris 1.0 onwards, DPair, Subset and Exists cannot implement any interface or, in other words, that they cannot be member of any type class.

2. Decide that the fact that

> implementation Uninhabited (DPair Nat (\ n  => LT n Z)) where
>   uninhabited (MkDPair n prf) = absurd prf

does not type check is an error that will hopefully be eradicated.

I am open to either decision although 1) would obviously make Sigma types in Idris rather pointless. I understand that in case of 2) it might take a long time to fix the issue. Still, a decision would allow me to make a plan: this issue is the reason why I am still stuck with Idris 0.99.
Thanks for looking into this again! Best, Nicola

[ahmadsalim]

@nicolabotta Would it work fine for you if it was possible to use named instances with this kind of pattern?

[ahmadsalim]

So e.g.

implementation [uninhabitedlt] Uninhabited (DPair Nat (\ n  => LT n Z)) where
   uninhabited (MkDPair n prf) = absurd prf

would type check.

[nicolabotta]

@ahmadsalim I do not know! It depends on what are the implications of using named instances. If it was possible to write something like

> LTE : (x, y : NonNegDouble) -> Type
> NonNegDouble : Type
> NonNegDouble = Subset Double (\ x => 0.0 `LTE` x)
> implementation [numnnd] Num NonNegDouble where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat
> x : NonNegDouble
> y : NonNegDouble
> z : NonNegDouble
> z = x + y

for suitable definitions of LTE, plus, mult and fromNat then it would be fine for me. But if naming the instance would force me to also name every usage of (+), (*), etc. than the approach wouldn't bring anything to the game, I am afraid. Perhaps I am missing something?

[ahmadsalim]

@nicolabotta I think you can use using implementation numnnd, but I am not entirely sure.

[ahmadsalim]

Because using implementation might depend on instance search, which is fragile in presence of non-injective constructors.

[ahmadsalim]

Thinking about this, this might still be better than the current situation.
If the implementation search can not find such instance, one can just provide it manually (which is not possible for unnamed ones).

[nicolabotta]

Can we start with the instance declaration? The first step would be to make

> implementation [lala] Uninhabited (DPair Nat (\ n  => LT n Z)) where
>   uninhabited (MkDPair n prf) = absurd prf

type check. How difficult would this be?

[ahmadsalim]

@nicolabotta I am currently trying to do this in the background, let me see if it compiles/has any issues.

[nicolabotta]

@ahmadsalim Great, thanks!

[nicolabotta]

Great, next step is to make the instance declaration usable! The code

> LTB : Nat -> Type
> LTB b = DPair Nat (\ n  => LT n b)

> implementation [gugu] Uninhabited (LTB Z) where
>   uninhabited (MkDPair n prf) = absurd prf

> toFin : {b : Nat} -> LTB b -> Fin b
> fromFin : {b : Nat} -> Fin b -> LTB b

> fromFinToFinLemma : {b : Nat} -> (n : LTB b) -> fromFin (toFin n) = n
> fromFinToFinLemma {b = Z} k = absurd k

fails to type check with

- + Errors (1)
 `-- ./BoundedNat/issues/implementation.lidr line 16 col 20:
     When checking right hand side of fromFinToFinLemma with expected type
             fromFin (toFin k) = k
     
     Can't find implementation for Uninhabited (LTB 0)

but it type checks fine in Idris 0.99. Any idea how to proceed? Thanks, Nicola

[ahmadsalim]

@nicolabotta There are two ways you could use the named implementation, either:

LTB : Nat -> Type
LTB b = DPair Nat (\ n  => LT n b)

implementation [gugu] Uninhabited (LTB Z) where
   uninhabited (MkDPair n prf) = absurd prf

toFin : {b : Nat} -> LTB b -> Fin b
fromFin : {b : Nat} -> Fin b -> LTB b

using implementation gugu
  fromFinToFinLemma : {b : Nat} -> (n : LTB b) -> fromFin (toFin n) = n
  fromFinToFinLemma {b = Z} k = absurd k

   {- Other code relying on gugu -}

or

LTB : Nat -> Type
LTB b = DPair Nat (\ n  => LT n b)

implementation [gugu] Uninhabited (LTB Z) where
   uninhabited (MkDPair n prf) = absurd prf

toFin : {b : Nat} -> LTB b -> Fin b
fromFin : {b : Nat} -> Fin b -> LTB b

fromFinToFinLemma : {b : Nat} -> (n : LTB b) -> fromFin (toFin n) = n
fromFinToFinLemma {b = Z} k = absurd @{gugu}  k

Note because the implementation has a non-injective parameter, you may be forced to use the explicit passing (second) style sometimes because failing to resolve it.

[ahmadsalim]

@nicolabotta Note I added a test with your previous example code:
https://github.com/idris-lang/Idris-dev/blob/master/test/interfaces009/interfaces009.idr

[nicolabotta]

@ahmadsalim Many thanks!

[ahmadsalim]

Sure, you are most welcome 😄