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:
- Coercions are generated at the search site based on the relevant data constructors with any parameter specifications at the search site substituted
- 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