inferred type doesn't type-check (using type families)

[Roland Zumkeller-2]

Hi,

Compiling

> class WithT a where
>   type T a

> f :: T a -> a -> T a
> f = undefined

> g x = f x 42

with -XTypeFamilies -fwarn-missing-signatures gives:

             Inferred type: g :: forall a. (Num a) => T a -> T a

Adding

> g :: Num a => T a -> T a

results in:

    Couldn't match expected type `T a' against inferred type `T a1'
    In the first argument of `f', namely `x'

Is the inferred type not the right one? Is g typeable?

Best,

Roland

--
http://alacave.net/~roland/
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Daniel Fischer-4]

Am Dienstag 03 November 2009 19:28:55 schrieb Roland Zumkeller:

> Hi,
>
> Compiling
>
> > class WithT a where
> >   type T a
> >
> > f :: T a -> a -> T a
> > f = undefined
> >
> > g x = f x 42
>
> with -XTypeFamilies -fwarn-missing-signatures gives:
>
>              Inferred type: g :: forall a. (Num a) => T a -> T a
>
> Adding
>
> > g :: Num a => T a -> T a
>
> results in:
>
>     Couldn't match expected type `T a' against inferred type `T a1'
>     In the first argument of `f', namely `x'
>
> Is the inferred type not the right one? Is g typeable?

The type function T isn't injective (or, it isn't guaranteed to be), so there's no way to
determine which type a to use for 42.

>
> Best,
>
> Roland

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Max Bolingbroke-2]

2009/11/3 Daniel Fischer <daniel.is.fischer@...>:

> Am Dienstag 03 November 2009 19:28:55 schrieb Roland Zumkeller:
>> Hi,
>>
>> Compiling
>>
>> > class WithT a where
>> >   type T a
>> >
>> > f :: T a -> a -> T a
>> > f = undefined
>> >
>> > g x = f x 42
>>
>> with -XTypeFamilies -fwarn-missing-signatures gives:
>>
>>              Inferred type: g :: forall a. (Num a) => T a -> T a
>>
>> Adding
>>
>> > g :: Num a => T a -> T a
>>
>> results in:
>>
>>     Couldn't match expected type `T a' against inferred type `T a1'
>>     In the first argument of `f', namely `x'
>>
>> Is the inferred type not the right one? Is g typeable?
>
> The type function T isn't injective (or, it isn't guaranteed to be), so there's no way to
> determine which type a to use for 42.

I think (untested) that in this particular case you can get around the
problem using scoped type variables:

> g :: forall a. Num a => T a -> T a
> g x = f x (42 :: a)

In fact, this seems to be the general pattern for fixing problems like
this with type families: add extra "witness" arguments which GHC can
use to unify type variables that are "hidden" inside type family
applications.

Cheers,
Max
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[David Menendez-2]

On Tue, Nov 3, 2009 at 3:20 PM, Max Bolingbroke
<batterseapower@...> wrote:

> 2009/11/3 Daniel Fischer <daniel.is.fischer@...>:
>> Am Dienstag 03 November 2009 19:28:55 schrieb Roland Zumkeller:
>>> Hi,
>>>
>>> Compiling
>>>
>>> > class WithT a where
>>> >   type T a
>>> >
>>> > f :: T a -> a -> T a
>>> > f = undefined
>>> >
>>> > g x = f x 42
>>>
>>> with -XTypeFamilies -fwarn-missing-signatures gives:
>>>
>>>              Inferred type: g :: forall a. (Num a) => T a -> T a
>>>
>>> Adding
>>>
>>> > g :: Num a => T a -> T a
>>>
>>> results in:
>>>
>>>     Couldn't match expected type `T a' against inferred type `T a1'
>>>     In the first argument of `f', namely `x'
>>>
>>> Is the inferred type not the right one? Is g typeable?
>>
>> The type function T isn't injective (or, it isn't guaranteed to be), so there's no way to
>> determine which type a to use for 42.
>
> I think (untested) that in this particular case you can get around the
> problem using scoped type variables:
>
>> g :: forall a. Num a => T a -> T a
>> g x = f x (42 :: a)

GHC accepts this, but arguably shouldn't as there's no way to call g.
Neither the argument to g nor the context of g has enough information
to specify a, so there's no way to know what's intended.

> In fact, this seems to be the general pattern for fixing problems like
> this with type families: add extra "witness" arguments which GHC can
> use to unify type variables that are "hidden" inside type family
> applications.

This is true. You can use a dummy argument to force the choice of a,
and if the dummy isn't used it gets removed in optimization.

data Proxy a  -- no values, so should always be removable during optimization

g :: forall a. Num a => Proxy a -> T a -> T a
g _ x = f x (42 :: a)   -- works fine

--
Dave Menendez <dave@...>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Simon Peyton-Jones]

| I think (untested) that in this particular case you can get around the
| problem using scoped type variables:
|
| > g :: forall a. Num a => T a -> T a
| > g x = f x (42 :: a)
|
| In fact, this seems to be the general pattern for fixing problems like
| this with type families: add extra "witness" arguments which GHC can
| use to unify type variables that are "hidden" inside type family
| applications.

But in this case all you've done is to make g have an ambiguous type.

I've drafted a FAQ about this at
        http://haskell.org/haskellwiki/GHC/Type_families#Frequently_asked_questions

Please, everyone, edit and extend.

Simon
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@...
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users