Opened 2 years ago
Last modified 16 months ago
#14317 new feature request
Solve Coercible constraints over type constructors
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | Roles, QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #14386 | Differential Rev(s): | |
Wiki Page: |
Description
The core question is, could fails
type check?
import Data.Type.Coercion works :: Identity a `Coercion` Compose Identity Identity a works = Coercion -- • Couldn't match representation of type ‘Identity’ -- with that of ‘Compose Identity Identity’ -- arising from a use of ‘Coercion’ -- • In the expression: -- Coercion :: Identity `Coercion` Compose Identity Identity fails :: Identity `Coercion` Compose Identity Identity fails = Coercion
This arises from playing with Traversable: A Remix.
Given coerce :: Compose Identity Identity ~> Identity
I wanted to capture that id1
and id2
are actually the same arrow (up to representation)
(<%<) :: (Functor f, Functor g) => (b -> g c) -> (a -> f b) -> (a -> Compose f g c) g <%< f = Compose . fmap g . f id1 :: a -> Identity a id1 = Identity id2 :: a -> Compose Identity Identity a id2 = Identity <%< Identity
So I define
data F :: (k -> Type) -> (Type -> k -> Type) where MkF :: Coercible f f' => (a -> f' b) -> F f a b id1F :: Coercible Identity f => F f a a id1F = MkF id1 id2F :: Coercible (Compose Identity Identity) f => F f b b id2F = MkF id2
but we can not unify the types of id1F
and id2F
. Does this require quantified class constraints? I'm not sure where they would go
Change History (10)
comment:1 Changed 2 years ago by
Keywords: | Roles QuantifiedContexts added |
---|
comment:2 follow-ups: 5 6 Changed 2 years ago by
comment:3 Changed 2 years ago by
Slightly on a tangent but: this program typechecks in 8.0.2 but fails in 8.2.1
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} import Data.Coerce newtype (f ... g) a = C (f (g a)) newtype I a = I a data F f a b where MkF :: Coercible (f b) (f' b) => (a -> f' b) -> F f a b id1 :: a -> I a id1 = I id1F :: Coercible b (f b) => F f b b id1F = MkF I
/Users/adam/src/doodles/co.hs:17:8: error: • Could not deduce: Coercible b (f b) arising from a use of ‘MkF’ from the context: Coercible b (f b) bound by the type signature for: id1F :: forall b (f :: * -> *). Coercible b (f b) => F f b b at /Users/adam/src/doodles/co.hs:16:1-36 ‘b’ is a rigid type variable bound by the type signature for: id1F :: forall b (f :: * -> *). Coercible b (f b) => F f b b at /Users/adam/src/doodles/co.hs:16:1-36 • In the expression: MkF I In an equation for ‘id1F’: id1F = MkF I • Relevant bindings include id1F :: F f b b (bound at /Users/adam/src/doodles/co.hs:17:1) | 17 | id1F = MkF I | ^^^^^
comment:5 Changed 2 years ago by
My goal was to specialize id1F
, id2F
to
id1F :: F (Compose Identity Identity) a a id2F :: F Identity a a
such that F f
can be made a Category
(less useful than I originally thought). This works with Adam's code (on 8.0.1)
data F' f a b where MkF' :: Coercible (f b) (f' b) => (a -> f' b) -> F' f a b id1F :: Coercible (f a) a => F' f a a id1F = MkF' Identity a :: F' Identity a a a = id1F b :: F' (Compose Identity Identity) a a b = id1F
which cannot be made into a Category
because the representation of a
leaks into the signature.
Replying to RyanGlScott:
I think you might be inclined to believe that because
Identity a
is representationally equal to(Compose Identity Identity) a
, that GHC can conclude thatIdentity
is representationally equal toCompose Identity Identity
.
Yes that's right
But to my knowledge, there's no reasoning principle which states that
f a ~R g a
impliesf ~R g
.
Can there not be some kind of pseudo rule?
instance (forall xx. f xx `Coercible` g xx) => Coercible f g
I don't understand uses for polykinded Coercible
newtype EITHER a b = E (Either a b) newtype USD = USD Int x :: Coercion EITHER Either x = Coercion y :: Coercion (EITHER USD) (Either Int) y = Coercion
coerce
and coerceWith
only work with Type
s.. maybe it is used to assist the constraint solver in ways I don't get
comment:6 Changed 23 months ago by
It turns out that my earlier comment:
Replying to RyanGlScott:
But to my knowledge, there's no reasoning principle which states that
f a ~R g a
impliesf ~R g
.
Is a bit misleading. I've re-read the Safe Zero-cost Coercions for Haskell paper recently, and it turns out that Section 2.8 (Supporting higher-order polymorphism) pertains to this very topic:
So far, we have only seen
Coercible
applied to types of kind*
, but that is not sufficient to support all coercions that we might want. For example, consider a monad transformer such asdata MaybeT m a = MaybeT (m (Maybe a))and a newtype that wraps another monad, e.g.
newtype MyIO a = MyIO (IO a)It is reasonable to expect that
Coercible (MaybeT MyIO a) (MaybeT IO a)
can be derived. Using the lifting rule forMaybeT
, this requiresCoercible MyIO IO
to hold. Therefore, for anewtype
declaration as the one above, GHC will η-reduce the unwrapping rule to sayCoercible IO MyIO
instead ofCoercible (IO a) (MyIO a)
. Using symmetry, this allows us to solveCoercible (MaybeT MyIO a) (MaybeT IO a)
.
Alas, that is the only discussion of eta-reducing unwrapping rules that I can find in the entire paper, as it doesn't appear to be brought up again at any point. But this would definitely explain why you can construct a Coercion (EITHER USD) (Either Int)
with relative ease.
Now it is clear to me why you still can't derive Coercible Identity (Compose Identity Identity)
from Coercible (Identity a) (Compose Identity Identity a)
. The reason is because you'd have to be able to η-reduce this unwrapping rule:
Coercible (Compose f g a) (f (g a))
But there is no way to η-reduce the a
from f (g a)
, so GHC evidently does not attempt this. So I'm inclined to label this as not-a-bug.
comment:7 Changed 23 months ago by
Related Tickets: | → #14386 |
---|
See also #14386, which shows another example of an unwrapping rule that fails to eta-reduce.
comment:8 Changed 23 months ago by
Yet another thing that representational equality can't do, but perhaps could if it were better.
comment:9 Changed 20 months ago by
Keywords: | QuantifiedConstraints added; QuantifiedContexts removed |
---|
You're asking about two different (incomplete) programs, so I'm forced to guess at what your intention was. I'll tackle them in reverse order.
For the second program, I'm guessing this is what you meant? I had to add some imports and language extensions to make this go through:
But importantly, this program does typecheck! So I'm not sure what bug you're alluding to here. (You mention "we can not unify the types of
id1F
andid2F
", but I'm not sure what is meant by that statement.)For the first program, I also needed to add some imports and language extensions:
But this time, I can reproduce the error you reported for this program. The error is right on the mark—you can't
coerce
betweenIdentity
andCompose Identity Identity
because they're not representationally equal. Full stop. Try as you might, there's no way to derive aCoercible Identity (Compose Identity Identity)
constraint.I think you might be inclined to believe that because
Identity a
is representationally equal to(Compose Identity Identity) a
, that GHC can conclude thatIdentity
is representationally equal toCompose Identity Identity
. But to my knowledge, there's no reasoning principle which states thatf a ~R g a
impliesf ~R g
.