inferred type doesn't type-check (using type families)
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:
>>> > 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
>>> > 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
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>
More information about the Glasgow-haskell-users