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

[David Menendez]

On Tue, Nov 3, 2009 at 3:20 PM, Max Bolingbroke
<batterseapower at hotmail.com> wrote:
> 2009/11/3 Daniel Fischer <daniel.is.fischer at web.de>:
>> 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 at zednenem.com>
<http://www.eyrie.org/~zednenem/>