haskelltypeclasscoercionphantom-types

Coercion of typeclass instances with phantom parameter

I have

{-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Coerce
import Data.Kind

newtype IFix f i = IFix { unIFix :: f (IFix f) i }

class IFunctor (f :: (i -> Type) -> i -> Type) where
  imap :: (forall i'. a i' -> b i') -> (forall i'. f a i' -> f b i')

f :: IFunctor f => forall i. IFix f i -> IFix f i
f = undefined

g :: IFunctor f => forall i. IFix f i -> IFix f i
g = IFix . imap f . unIFix

h :: IFunctor f => forall i. IFix f i -> IFix f i
h = coerce . imap f . coerce

i :: IFunctor f => forall i. IFix f i -> IFix f i
i = coerce (imap f)

where IFix is a type-level fixpoint of indexed type constructors, i is the index (a phantom parameter), IFunctor is the class of such indexed type constructors that are actually functors, f is just a random function, g, h, i try to propagate f under the IFix wrapper. A side note: this is a simplified example and I actually often run into similar problems in other settings where manual rewrapping becames a bit tedious (for one I would like to avoid mapping the unwrap-rewrap function over lists or other structures).

input:18:5: error:
    • Couldn't match representation of type ‘f (IFix f) i’
                               with that of ‘f0 (IFix f1) i0’
        arising from a use of ‘coerce’
   |
18 | h = coerce . imap f . coerce
   |     ^^^^^^

input:21:5: error:
    • Couldn't match representation of type ‘f (IFix f) i’
                               with that of ‘f2 (IFix f3) i1’
        arising from a use of ‘coerce’
   |
21 | i = coerce (imap f)
   |     ^^^^^^^^^^^^^^^

and honestly I am not really surprised, but since I do not see under the hood of coercions I wonder, is there a way to modify my definitions, so that coerce can be applied? I tried RoleAnnotations but

  1. type role IFix nominal phantom is invalid
  2. I have no idea how to require type roles for the type class (and I fear there is no way, since the doc mentions typeclasses assume parameters to be nominal)

So my question is, is there a way to make coerce work in this setting and if not, are there any deep reasons why not or is it just the limitation of the current role inference implementation. My naive view leads me to believe a typeclass could impose constraints on roles of arguments and instances would have to satisfy the constraint. Is there maybe a good source on some useful coercion tricks?

Solution

  • Actually, g and h don't typecheck because the type of imap f is ambiguous.

    imap :: IFunctor f => (a ~> b) -> (f a ~> f b)

    For example, in h, imap f gets inferred the following type, with free unification variables ?f0, ?f1, ?i0:

    h = coerce . (imap f :: ?f0 (IFix ?f1) ?i0 -> ?f0 (IFix ?f1) ?i0) . coerce

    Usually the context allows us to instantiate these variables, but here the context is:

    coerce . _ . coerce

    note the type of coerce :: Coercible a b => a -> b, which entirely decouples the input and output types, as far as type inference is concerned.

    We can use the extension ScopedTypeVariables to annotate imap f:

    h :: forall f i. IFunctor f => IFix f i -> IFix f i
h = coerce . (imap f :: f (IFix f) i -> f (IFix f) i) . coerce

    or specialize coerce to restrict its shape:

    type E a = a -> a

i :: IFunctor f => IFix f i -> IFix f i
i = (coerce :: E (f (IFix f) i) -> E (IFix f i)) (imap f)

    coerce on its own is too general, so it's common to have to add such annotations. It might be worth having a library of common specializations.