[Haskell-cafe] Question on inductive type-families

[Sylvain Henry]

Hi,

Suppose I have the following type family:

type family Index (n :: Nat) (l :: [k]) = (r :: k) where
    Index 0 (x ': _ ) = x
    Index n (_ ': xs) = Index (n-1) xs

I'm using it to define a Variant type:

data V2 (vs :: [k]) where
    V2 :: forall vs (n :: Nat). KnownNat n => Proxy n -> Index n vs -> V2 vs

Now I want to match on the Variant retrieving either the head or the 
tail (another Variant):

splitV2 :: forall v vs. V2 (v:vs) -> Either v (V2 vs)
splitV2 = \case
    V2 (n1 :: Proxy n) v -> case sameNat n1 (Proxy @0) of
          Just Refl -> Left v
          Nothing   -> Right (V2 (Proxy @(n-1)) v)

It fails to typecheck with:

Couldn't match type ‘Index n (v : vs)’ with ‘Index (n - 1) vs’
Expected type: Index (n - 1) vs
Actual type: Index n vs1
NB: ‘Index’ is a non-injective type family


Is there a way to make this work?


This is highly speculative as I'm not very familiar with type-checking: 
would it be sound to make the inductive Index family "weakly" injective? 
I.e. somehow produce a typing rule for the type family:

   forall n n' x xs xs'.
     Solving: Index n (x ': xs) ~ Index (n'-1) xs'
     Is equivalent to solving: if n /= 0 then (n ~ n', xs ~ xs') else (x 
~ Index (n'-1) xs')

Here we could know that "n /= 0" thanks to the match on "sameNat n1 
(Proxy @0)".

("weakly" because we have some form of injectivity on the shape of the 
list but not on its contents)

Any pointer on this kind of stuff in research papers, Coq, Agda, etc. ?

Thanks,
Sylvain