`coerce` and instantiation of type variables

Question

Consider the following GHCi session:

>:set -XTypeApplications
>import Data.Map.Strict
>import GHC.Exts
>newtype MySet a = MySet (Map a ())
>let member' :: Ord a => a -> MySet a -> Bool; member' = coerce member

<interactive>:21:57: error:
    * Couldn't match representation of type `a0' with that of `()'
        arising from a use of `coerce'
    * In the expression: coerce member
      In an equation for member': member' = coerce member
>let member' :: Ord a => a -> MySet a -> Bool; member' = coerce (member @_ @())

I have a hunch of what's going on here: The type-checker needs to satisfy Coercible (Ord a => a -> Map a b -> Bool) (Ord a => a -> MySet a -> Bool) and isn't able to instantiate b in this constraint to ().

Is there a more elegant way than to do this with -XTypeApplications?

Edit: I'm especially looking for solutions that deal with many occurences of MySet a in the type, for example union :: Ord a => MySet a -> MySet a -> MySet a.

Answer 1

member :: Ord a => a -> Map a b -> Bool
member' :: Ord a => a -> MySet a -> Bool

GHC needs to accept

Coercible (Map a b) (MySet a)

It sees that

Coercible (MySet a) (Map a ())

which leaves it needing

Coercible (Map a ()) (Map a b)

which leads to

Coercible () b

But what is b? It's ambiguous. In this case, it doesn't matter what b is, because by parametricity, member can't possibly care. So it would be perfectly reasonable to choose b ~ () and resolve the coercion trivially. But GHC generally doesn't perform such a parametricity analysis in type inference. I suspect it might be tricky to change that. Most especially, any time the type inference "guesses", there's a risk it might guess wrong and block up inference somewhere else. It's a big can of worms.

As for your problem, I don't have a good solution. When you have several functions with similar patterns, you can abstract them out, but you'll still face significant annoyance.

Answer 2

The solution with TypeApplications is quite straightforward:

{-# LANGUAGE TypeApplications #-}

import Data.Coerce
import qualified Data.Map as M

newtype Set a = Set (M.Map a ())

member :: Ord a => a -> Set a -> Bool
member = coerce (M.member @_ @())

union :: Ord a => Set a -> Set a -> Set a
union = coerce (M.union @_ @())

Note that some functions will require more or less wildcards, e.g.

smap :: (Ord b) => (a -> b) -> Set a -> Set b
smap = coerce (M.mapKeys @_ @_ @())

To determine how exactly you must specify the type applications (aside from trial and error), use

>:set -fprint-explicit-foralls
>:i M.mapKeys
M.mapKeys ::
  forall k2 k1 a. Ord k2 => (k1 -> k2) -> M.Map k1 a -> M.Map k2 a

The variable order you get from :i is the same one used by TypeApplications.

Note that you can't use coerce for fromList - it isn't a limitation, it just doesn't make sense:

fromList :: Ord a => [a] -> Set a
fromList = coerce (M.fromList @_ @())

This gives the error

* Couldn't match representation of type `a' with that of `(a, ())'

The best you can do here is probably

fromList :: Ord a => [a] -> Set a
fromList = coerce (M.fromList @_ @()) . map (flip (,) ())