I'm working on a Yesod app and wanted to have an alternative textField
with a modified fieldView
. To start, I tried this:
textField
:: ( Monad m
, RenderMessage (HandlerSite m) FormMessage
)
=> Field m Text
textField = I.textField
{ fieldView = fieldView I.textField
}
As far as I can see, this textField
should be identical to I.textField
. However, I get the following error:
Foo.hs:37:19: error:
• Couldn't match type ‘HandlerSite m0’ with ‘HandlerSite m’
Expected type: FieldViewFunc m Text
Actual type: FieldViewFunc m0 Text
NB: ‘HandlerSite’ is a type function, and may not be injective
The type variable ‘m0’ is ambiguous
• In the ‘fieldView’ field of a record
In the expression: I.textField {fieldView = fieldView I.textField}
In an equation for ‘textField’:
textField = I.textField {fieldView = fieldView I.textField}
• Relevant bindings include
textField :: Field m Text
(bound at Foo.hs:36:1)
Interestingly, this alternative way of writing this works just fine:
textField
:: ( Monad m
, RenderMessage (HandlerSite m) FormMessage
)
=> Field m Text
textField = f
{ fieldView = fieldView
}
where
f@Field {..} = I.textField
Is the problem in using fieldView
as a function? I'm quite stumped right now. I tried using ScopedTypeVariables
to link m
to m0
, but it didn't work and I don't see why it would even be needed. What's stopping m
from matching with m0
?
EDIT: I just tried:
textField
:: ( Monad m
, RenderMessage (HandlerSite m) FormMessage
)
=> Field m Text
textField = I.textField
{ fieldView = fieldView
}
where
Field {..} = I.textField
And it failed, so I guess the problem is related with mentioning I.textField
twice. This is weird. It's not like I.textField
is a type-class member with multiple definitions to select from, and, even if it were, I don't see what's stopping ghc from deducing that m
and m0
are the same.... ok HandlerSite
is a type family, so I guess from the type checker's point of view it could lead to different instances of RenderMessage
and so different definitions of code that's somehow linked to I.textField
. I think I'm starting to see the light.
EDIT 2: I thought I could link them like this:
textField
:: ( Monad m
, RenderMessage (HandlerSite m) FormMessage
)
=> Field m Text
textField = (I.textField :: Field m Text)
{ fieldView = fieldView (I.textField :: Field m Text)
}
with ScopedTypeVariables
on, but apparently not.
EDIT 3: Following the logic, this works:
textField
:: ( Monad m
, RenderMessage (HandlerSite m) FormMessage
)
=> Field m Text
textField = f
{ fieldView = fieldView f
}
where
f = I.textField
So I guess this has something to do with top-level vs local bindings?
And it failed, so I guess the problem is related with mentioning I.textField twice. This is weird.
Actually, this is quite common when type families are involved. Let me show the issue in a simpler case. Suppose we have a type family as follows
type family F a
type instance F Int = String
type instance F Bool = String
Note how F Int
and F Bool
are actually the same type, i.e. String
. This is possible since F
can be a non-injective function.
Now, if we have at hand the following function
foo :: F a -> SomeResultType
we discover that we can not, in general, call it as
foo "some string"
Why? Well, the compiler can not determine what type to use for a
: it could be Int
or Bool
, since both would make F a
to be String
. The call is ambiguous, so it raises a type error.
Even worse, if we used twice that call in our code, e.g.
bar (foo "string") (foo "string")
it would be even possible to choose a = Int
for the first call, and a = Bool
for the second call!
Moreover, consider what would happen if we have a polymorphic value which can produce any F a
.
x :: forall a . F a
Then, we might be tempted to call foo x
. After all, foo
takes F a
and x
can produce F a
for any a
. It looks fine, but it is once again ambiguous. Indeed, what should be chosen for a
? Many choices apply. We might try to fix this with a type signature
foo (x :: F Int)
but this is completely equivalent to any of
foo (x :: String)
foo (x :: F Bool)
so it does really choose the type a
!
In your code, a similar problem happens. Let's dissect the type error:
Couldn't match type ‘HandlerSite m0’ with ‘HandlerSite m’
Expected type: FieldViewFunc m Text
Actual type: FieldViewFunc m0 Text
NB: ‘HandlerSite’ is a type function, and may not be injective
This is telling us that at some point we need to specify a FieldViewFunc m Text
. This type involves a type family HandlerSite m
, which due to non-injectivity, could be the same type as HandlerSite m0
for some other monad m0
.
Now, I.textField
can produce a value "for any m
". Hence, using it is somehow similar to using foo x
above. Your code is more peculiar, since if we use the "same" call to I.textField
, the compiler is able to infer that we indeed want the "right" m
. Here, "same" call means defining some identifier like your f
to I.textField
, and use f
twice. Instead, making two calls to I.textField
allows GHC to choose two distinct m
s, one for each call, and ambiguity arises.
If you are confused, don't worry -- it is a bit tricky to understand, especially on a relatively real-world framework like Yesod.
How to solve this? There are many ways, but in my opinion, the best, modern way to resolve such ambiguities is to turn on the TypeApplications
extension (beyond ScopedTypeVariables
) and then specify that we really want to choose m
as the outer m
, as follows:
textField :: forall m .
( Monad m
, RenderMessage (HandlerSite m) FormMessage
)
=> Field m Text
textField = I.textField @ m
{ fieldView = fieldView (I.textField @ m)
}
The @ m
syntax is used to choose the type, overriding the type inference engine. It has a similar effect as writing a type annotation in many cases, but works even in "ambiguous" cases where type annotations do not. For instance foo (x @ Int)
would have worked in the simpler example above.
(I'm not familiar with Yesod so the above might not work if I.textField
is also parametrized by other type variables, in which case we need more @ type
applications e.g. I.textField @type @type2 ...
one of which is @m
.)