Couldn't match type ‘HandlerSite m0’ with ‘HandlerSite m’ when "modifying" field with same value

Question

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?

Answer 1

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 ms, 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.)