[Haskell-cafe] Advice on type families and non-injectivity?

[Conal Elliott]

Thanks, Jake! This suggestion helped a lot.  -- Conal


On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur <jake.mcarthur at gmail.com>wrote:

> I have a trick that loses a little convenience, but may still be more
> convenient than data families.
>
> {-# LANGUAGE TypeFamilies #-}
>
> import Data.Tagged
>
> type family F a
>
> foo :: Tagged a (F a)
> foo = Tagged undefined
>
> bar :: Tagged a (F a)
> bar = foo
>
>
> This allows you to use the same newtype wrapper consistently, regardless
> of what the type instance actually is; one of the inconveniences of data
> families is the need to use different constructors for different types.
>
>
> On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott <conal at conal.net> wrote:
>
>> I sometimes run into trouble with lack of injectivity for type families.
>> I'm trying to understand what's at the heart of these difficulties and
>> whether I can avoid them. Also, whether some of the obstacles could be
>> overcome with simple improvements to GHC.
>>
>> Here's a simple example:
>>
>> > {-# LANGUAGE TypeFamilies #-}
>> >
>> > type family F a
>> >
>> > foo :: F a
>> > foo = undefined
>> >
>> > bar :: F a
>> > bar = foo
>>
>> The error message:
>>
>>     Couldn't match type `F a' with `F a1'
>>     NB: `F' is a type function, and may not be injective
>>     In the expression: foo
>>     In an equation for `bar': bar = foo
>>
>> A terser (but perhaps subtler) example producing the same error:
>>
>> > baz :: F a
>> > baz = baz
>>
>> Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>>
>> Does the difficulty here have to do with trying to *infer* the type and
>> then compare with the given one? Or is there an issue even with type
>> *checking* in such cases?
>>
>> Other insights welcome, as well as suggested work-arounds.
>>
>> I know about (injective) data families but don't want to lose the
>> convenience of type synonym families.
>>
>> Thanks,  -- Conal
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130114/cf96af01/attachment.htm>