#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles, | QuantifiedContexts Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs {-# 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: {{{#!hs {-# 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles, | QuantifiedContexts Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Good catch. I've opened #14323 for this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles, | QuantifiedContexts Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): It turns out that my earlier comment: Replying to [comment:2 RyanGlScott]:

But to my knowledge, there's no reasoning principle which states that `f a ~R g a` implies `f ~R g`.

So far, we have only seen `Coercible` applied to types of kind `*`, but

Is a bit misleading. I've re-read the [http://www.seas.upenn.edu/~sweirich/papers/coercible-JFP.pdf 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: that is not sufficient to support all coercions that we might want. For example, consider a monad transformer such as

{{{#!hs data MaybeT m a = MaybeT (m (Maybe a)) }}}

and a newtype that wraps another monad, e.g.

{{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles, | QuantifiedContexts 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Yet another thing that representational equality can't do, but perhaps could if it were better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles, | QuantifiedConstraints 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: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"7df589608abb178efd6499ee705ba4eebd0cf0d1/ghc" 7df5896/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="7df589608abb178efd6499ee705ba4eebd0cf0d1" 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler