Pattern matching breaks injective type families
{-# LANGUAGE TypeFamilyDependencies, TypeOperators, DataKinds, GADTs, TypeApplications #-}
data HList xs where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x:xs)
type family ListId xs = ys | ys -> xs
where
ListId '[] = '[]
ListId (x:xs) = (x : ListId xs)
f :: HList (ListId ts) -> ()
f a =
case a of
HNil -> ()
-- z@(HCons _ _) -> f z -- uncomment to break
z -> f z
While z -> f z
works, pattern matching on HCons
breaks it:
A.hs:16:24: error:
• Could not deduce: ListId xs ~ xs1
from the context: ListId ts ~ (x : xs1)
bound by a pattern with constructor:
HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
in a case alternative
at A.hs:16:8-16
‘xs1’ is a rigid type variable bound by
a pattern with constructor:
HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
in a case alternative
at A.hs:16:8-16
Expected type: HList (ListId (x : xs))
Actual type: HList (ListId ts)
• In the first argument of ‘f’, namely ‘z’
In the expression: f z
In a case alternative: z@(HCons _ _) -> f z
|
16 | z@(HCons _ _) -> f z
| ^