Its partial inverse, "thickening" has the spec
thicken i i = Nothing thicken i (thin i j) = Just j
thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n) thicken Fz Fz = Nothing thicken Fz (Fs j) = Just j thicken (Fs i) Fz = Just Fz thicken (Fs i) (Fs j) = fmap Fs (thicken i j)
[...]
So you really need a safety check there. Another way to do it, crudely but avoiding the run time numbers, is this
thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n) thicken Fz Fz = Nothing thicken Fz (Fs j) = Just j thicken (Fs Fz) Fz = Just Fz thicken (Fs Fz) (Fs j) = fmap Fs (thicken Fz j) thicken (Fs (Fs i)) Fz = Just Fz thicken (Fs (Fs i)) (Fs j) = fmap Fs (thicken (Fs i) j)
Isn't the problem simply that in the former 'thicken', the compiler can not guarantee that the case thicken (Fs i) Fz = Just Fz does never show up when we have 'thicken :: Fin (S Z) -> ...'? I mean the subtle point about Fin is that 'Fz' is the "only" inhabitant of 'Fin (S Z)'. At least, this is what Epigram can deduce. But due to _|_, every constructor that is declared may appear in the form of Fs _|_ That's why only the latter 'thicken' can be correct. Regards, apfelmus