Add more coercion rules

[treeowl]

mapMonotonic coerce = coerce and mapKeysMonotonic coerce = coerce, or so.

[jberryman]

This would be nice. I came here to ask for a Set.coerce but I don't know which is better.

It's a very unsatisfying situation, because ideally we could just use coerce and GHC would throw an error in the rare case that we didn't just derive Ord somewhere, and so we could get something that's safer than mapMonotonic for this use-case.

[treeowl]

@jberryman, we can offer these rules while maintaining a "standard Haskell" API. For coercing, we'd want

setCoercion :: Coercible a b => Coercion (Set a) (Set b)
-- and/or
quantCo :: ((forall a b. Coercible a b => Coercible (Set a) (Set b)) => r) -> r

Unfortunately, the nasty way type roles work for data means we need unsafeCoerce for the former and also mean I have no idea how if at all to implement the latter. Will you be at Haskell DC on Wednesday?

[jberryman]

Yeah assumed, but wasn't totally sure if this was guaranteed to be safe (at least as safe as mapMonotonic):

setCoerce :: Coercible a b => Coercion (Set a) (Set b)
setCoerce = unsafeCoerce

(And my first comment was a little jumbled; if it wasn't clear I meant that it's a bit of a shame that setCoerce can't be made to be safer than mapMonotonic coerce.)

Will you be at Haskell DC on Wednesday?

No, but I'd love to come up for one sometime if I can. Just subscribed to the meetup group.

[dmwit]

@jberryman What goes wrong with the safe version, as in

setCoercion :: Coercible a b => Coercion (Set a) (Set b)
setCoercion = Coercion

(defined within a module that has access to Set's constructors, of course)?

[leftaroundabout]

@jberryman that's definitely not safe. Consider

newtype DInt = D {getDInt :: Int} deriving (Eq)
instance Ord DInt where D x < D y = y<x

Then coerce is not monotonic, and thus unsafeCoercing the maps would give a corrupted data structure.

But I'm not sure if that goes off on a tangent WRT to the question you meant to discuss here.

[treeowl]

@jberryman What goes wrong with the safe version, as in

setCoercion :: Coercible a b => Coercion (Set a) (Set b)
setCoercion = Coercion

(defined within a module that has access to Set's constructors, of course)?

@dmwit, the type checker will reject that thanks to the nominal role. The zero-cost coercion designers took a freebie that wasn't really so free. They liked the idea of

F's parameter has a representational role |-
  Coercible (F a) (F b) => Coercible a b

F's parameter has a nominal role |-
  Coercible (F a) (F b) => a ~ b

These can't work for newtypes, because it's just so obviously useful to be able to coerce them wildly when their constructors are in scope. But they figured they'd enforce the rule that data inherently and unconditionally has the role given in the role signature, giving them what they wanted. But that means we can't safely coerce nominal data even in the defining module.

[leftaroundabout]

Right, and the reason nominal data can't be safely coerced is precisely that it would allow mayhem like non-monotonic coerce destroying a set tree's invariant.

[treeowl]

(If it's not obvious already, I think that they were wrong to take that "freebie" and that it should be removed. It's not actually very useful and it gets in the way of a variety of potential good things.)

[treeowl]

(Alternatively, there could be a "soft" role signature and a "hard" role signature, where only the latter enables the backwards reasoning.)