inferred type doesn't type-check (using type families)
David Menendez
dave at zednenem.com
Tue Nov 3 20:38:41 EST 2009
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/>
More information about the Glasgow-haskell-users
mailing list