refactor Uninhabited implementation for Elem types #3412
Conversation
libs/base/Data/List/Elem.idr
Outdated
| @@ -19,11 +19,11 @@ data Elem : a -> List a -> Type where | |||
| There : Elem x xs -> Elem x (y :: xs) | |||
|
|
|||
| export | |||
| Uninhabited (Here = There e) where | |||
| Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs} e) where | |||
There was a problem hiding this comment.
If you're going fully heterogeneous, why not have two different xs on each sides?
There was a problem hiding this comment.
good point. xs are now different
There was a problem hiding this comment.
Since xs are now different maybe we should add something like that?
Either (Not (x = x')) (Not xs = xs') => Uninhabited (Here {x} {xs} = Here {x = x'} {xs = xs'}) where
Basically, if x or xs are different, Here and There will be different as well.
There was a problem hiding this comment.
Either (Not (x = x')) (Not xs = xs') => Uninhabited (Here {x} {xs} = Here {x = x'} {xs = xs'})
I think this can be proven for any Biinjective, not only for this particular one
There was a problem hiding this comment.
This might be more of a stylistic choice, I'm not sure, but I would personally prefer if at least one of the test code files used the explicit syntax for which equality was being used (i.e. === or ~=~), just so we have something clearly showing the different ones - since that was what caused the original confusion on the discord - as well as testing the magic elaboration of = to the hopefully correct equality : )
CHANGELOG_NEXT.md
Outdated
| @@ -227,6 +227,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO | |||
|
|
|||
| * Added `Data.IORef.atomically` for the chez backend. | |||
|
|
|||
| * Refactor `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`. | |||
There was a problem hiding this comment.
Would you mind adding a brief sentence explaining why / explaining what the refactor achieves?
I added tests for all combinations |
Description
Refactor
Uninhabitedimplementation forData.List.Elem,Data.List1.Elem,Data.SnocList.ElemandData.Vect.Elemso it can be used for homogeneous and heterogeneous equality.