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 Iceland_jack

Keywords: Roles QuantifiedContexts added

comment:2 Changed 2 years ago by RyanGlScott

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:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}

import Data.Coerce
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Kind

(<%<) :: (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

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 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 and id2F", 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:

{-# LANGUAGE TypeOperators #-}

import Data.Functor.Compose
import Data.Functor.Identity
import Data.Type.Coercion

works :: Identity a `Coercion` Compose Identity Identity a
works = Coercion

fails :: Identity `Coercion` Compose Identity Identity
fails = Coercion

But this time, I can reproduce the error you reported for this program. The error is right on the mark—you can't coerce between Identity and Compose Identity Identity because they're not representationally equal. Full stop. Try as you might, there's no way to derive a Coercible 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 that Identity is representationally equal to Compose Identity Identity. But to my knowledge, there's no reasoning principle which states that f a ~R g a implies f ~R g.

comment:3 Changed 2 years ago by adamse

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
   |        ^^^^^
Last edited 2 years ago by adamse (previous) (diff)

comment:4 Changed 2 years ago by RyanGlScott

Good catch. I've opened #14323 for this.

comment:5 in reply to:  2 Changed 2 years ago by Iceland_jack

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 that Identity is representationally equal to Compose Identity Identity.

Yes that's right

But to my knowledge, there's no reasoning principle which states that f a ~R g a implies f ~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 Types.. maybe it is used to assist the constraint solver in ways I don't get

Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:6 in reply to:  2 Changed 23 months ago by RyanGlScott

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 implies f ~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 as

data 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 for MaybeT, this requires Coercible MyIO IO to hold. Therefore, for a newtype declaration as the one above, GHC will η-reduce the unwrapping rule to say Coercible IO MyIO instead of Coercible (IO a) (MyIO a). Using symmetry, this allows us to solve Coercible (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 RyanGlScott

See also #14386, which shows another example of an unwrapping rule that fails to eta-reduce.

comment:8 Changed 23 months ago by goldfire

Yet another thing that representational equality can't do, but perhaps could if it were better.

comment:9 Changed 20 months ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:10 Changed 16 months ago by Ben Gamari <ben@…>

In 7df5896/ghc:

Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers
Note: See TracTickets for help on using tickets.