Hi Sylvain, The problem is that in the case where `n1` is not equal to `0`, this unequality is not made available as a constraint solver (whereas in the case where they are equal, the `Refl` constructor makes the corresponding equality constraint available). In fact, there is no built-in "unequality constraint" that acts as a counterpart to `~` (it does not seem quite straightforward how that would even work), but there is one way to encode it as a boolean type family `((n == 0) ~ 'False)`. That requires changing type families to pattern-match on `n == 0` instead of `n` directly, and possibly additional gymnastics to reflect the comparison at term-level: type Index n l = IndexIf (n == 0) n l type family IndexIf (b :: Bool) (n :: Nat) (l :: [k]) :: k where IndexIf 'False n (x ': _ ) = x IndexIf 'True n (_ ': xs) = Index (n - 1) xs Cheers, Li-yao On 8/21/19 9:09 AM, Sylvain Henry wrote:
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
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.