I'm pretty sure this is a bug. My code works if I put a type
signature on your second example.
*TFInjectivity :t testX'
testX' :: (P a ~ B (L a), X' a) = a - B (L a)
*TFInjectivity :t testX' (\(A _) - B __) :: B (HCons a HNil)
testX' (\(A _) - B __) :: B (HCons a HNil) :: B (HCons a HNil)
Hello,
On Tue, May 18, 2010 at 04:47:50PM -0700, Dan Weston wrote:
Unifying those two types by hand, I get:
P (A t - B a)
~ P (B a)
Maybe the problem is that type families (and associated types, their
class cousins) are not injective: P x ~ P y does not imply that x ~ y.
Hello all,
for the past few hours I've been struggling to express a certain idea using
type families and I really can't get it to typecheck. It all works fine using
functional dependencies, but it could be more readable with TFs. From those
papers about TFs I got this feeling that they should be
Unifying those two types by hand, I get:
P (A t - B a)
~ P (B a)
Maybe the problem is that type families (and associated types, their
class cousins) are not injective: P x ~ P y does not imply that x ~ y.
Maybe you need a data type (with appropriate wrapping and unwrapping) to
ensure
