Advice on type families and non-injectivity?

[Conal Elliott]

Hi Iavor,

Thanks for the remarks.

so there is really no way for GHC to figure out what is the intended value
> for `a`.
>

Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation `(forall a. F a) ==
(forall a'. F a')`?

-- Conal


On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki
<iavor.diatchki at gmail.com>wrote:

> Hello Conal,
>
> The issue with your example is that it is ambiguous, so GHC can't figure
> out how to instantiate the use of `foo`.   It might be easier to see why
> this is if you write it in this form:
>
> > foo :: (F a ~ b) => b
> > foo = ...
>
> Now, we can see that only `b` appears on the RHS of the `=>`, so there is
> really no way for GHC to figure out what is the intended value for `a`.
>  Replacing `a` with a concrete type (such as `Bool`) eliminates the
> problem, because now GHC does not need to come up with a value for `a`.
> Another way to eliminate the ambiguity would be if `F` was injective---then
> we'd know that `b` uniquely determines `a` so again there would be no
> ambiguity.
>
> If `F` is not injective, however, the only workaround would be to write
> the type in such a way that the function arguments appear in the signature
> directly (e.g., something like 'a -> F a' would be ok).
>
> -Iavor
>
>
>
>
>
>
>
>
> On Sun, Jan 13, 2013 at 11:10 AM, 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
>>
>>
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130113/bd650861/attachment.htm>