`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.

Good thinking, But this gets quite verbose for `union` (where `MySet` occurs multiple times in the type) and is not possible at all for `fromList`. — Sebastian Graf, Sep 04 '17 at 11:54
I think this might be considerable a bug in GHC, and certainly worth a ticket. Or talk to Richard in Oxford :-) — Joachim Breitner, Sep 04 '17 at 13:31
@JoachimBreitner, I suspect this would be rather hard to fix. See my answer. Of course, you and Richard both know much more than I do. — dfeuer, Sep 05 '17 at 07:40

dfeuer · Accepted Answer · 2017-09-05T09:27:17.610

2

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.

edited Sep 05 '17 at 09:27

answered Sep 05 '17 at 07:16

dfeuer

48,079
5
63
167

That sounds kind-of like what my gut told me, but I wasn't sure. Thanks! Using `-XTypeApplications` is rather tedious, but it works: https://github.com/sgraf812/pomaps/blob/6d077d3413c3fcc0de05955c2d6b9bd82c085a85/library/Data/POSet/Internal.hs – Sebastian Graf Sep 06 '17 at 09:01
Btw., I think the third and fourth `Coercible`s are switched. Not that it changes anything about the idea. – Sebastian Graf Sep 06 '17 at 09:08
1

@SebastianGraf, if you're wrapping a whole module, you may find it easier to use full type signatures than type applications. `foo = coerce (M.foo :: theoldthing this that) :: forall this that. thenewthing this that)`. More copy/paste that way, with less thinking about which type arguments go where. – dfeuer Sep 06 '17 at 13:08

score 1 · Answer 2 · answered Sep 05 '17 at 17:21

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 (,) ())

NB: the OP is explicit that they are aware of the TypeApplications solution, but I think it's 'simple enough' - so this answer is essentially "no, there is no more elegant way". But this seems largely opinion based, so instead I phrase the answer itself as a (simple!) method which can be used to mechanically write such code without thinking hard about how to do so. — user2407038, Sep 05 '17 at 21:59
`:set -fprint-explicit-foralls` sounds like what I had reached for if I had known it when implementing https://github.com/sgraf812/pomaps/blob/6d077d3413c3fcc0de05955c2d6b9bd82c085a85/library/Data/POSet/Internal.hs. Thanks for your tips, but I think the other post is a more direct answer to the question. — Sebastian Graf, Sep 06 '17 at 09:05

`coerce` and instantiation of type variables

2 Answers2