Skip to content

Derive coercions through data constructors

Motivation

Enable MonadTransControl's StT to be Type -> Type (and a Functor) without full higher-order roles.

See https://github.com/basvandijk/monad-control/pull/64 for an implementation currently unacceptable given the current rules, and https://github.com/basvandijk/monad-control/issues/39 for reasons why this would be useful.

Proposal

The idea is to modify the coercion instance search in 2 ways, which in principle can be added independently:

  1. Coercions are generated at the search site based on the relevant data constructors with any parameter specifications at the search site substituted
  2. Coercions incorporate the constraint context of the constructor, including any constraints implied by modification 1.

I'm not sure I'm using the best terminology for this, consider this example (which also indicates how this is different from higher-order roles):

{-# LANGUAGE QuantifiedConstraints #-}
module Test where

import Data.Coerce

newtype IdentityNT f a = IdentityNT (f a)

data IdentityData f a = IdentityData (f a)

data IdentityIO a = IdentityIO (IO a)

data IdentityEx f a = (forall x y. Coercible x y => Coercible (f x) (f y)) => IdentityEx (f a)

data IsRepresentational f = (forall x y. Coercible x y => Coercible (f x) (f y)) => IsRepresentational

-- Works because Coercible (IdentityNT IO) IO...
ntIO :: IsRepresentational (IdentityNT IO)
ntIO = IsRepresentational

-- Works because Coercible (IdentityNT f) f...
ntRep :: (forall x y. Coercible x y => Coercible (f x) (f y)) => IsRepresentational (IdentityNT f)
ntRep = IsRepresentational

{- None of the changes suggested here can make this work, needs higher-order roles and a role signature
ntBad :: IsRepresentational (IdentityNT f)
ntBad = IsRepresentational
-}

-- Works because inferred role
io :: IsRepresentational IdentityIO
io = IsRepresentational

-- Would be enabled by modification 1, the ctor becomes IdentityData (IO a). "Morally" equivalent to IdentityIO
dataIO :: IsRepresentational (IdentityData IO)
dataIO = IsRepresentational

-- Would be enabled by modification 1 + 2, the ctor becomes (forall x y. Coercible x y => Coercible (f x) (f y)) => IdentityData (f a). "Morally" equivalent to IdentityEx
dataRep :: (forall x y. Coercible x y => Coercible (f x) (f y)) => IsRepresentational (IdentityData f)
dataRep = IsRepresentational

{- None of the changes suggested here can make this work, needs higher-order roles and a role signature
dataBad :: IsRepresentational (IdentityData f)
dataBad = IsRepresentational
-}

-- Would be enabled by modification 2
ex :: IsRepresentational (IdentityEx f)
ex = IsRepresentational
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information