GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-01-09T16:33:21Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24315Reduction stack overflow when using "coerce"2024-01-09T16:33:21ZSebastian GrafReduction stack overflow when using "coerce"Here's an interesting program that tries to `coerce` an operation to operate on a newtype:
```hs
module T24315 where
import Data.Coerce
type Heap τ = Int -> Maybe (τ ())
newtype ProcessM τ a = ProcessM (Heap (ProcessM τ) -> τ (a, Heap...Here's an interesting program that tries to `coerce` an operation to operate on a newtype:
```hs
module T24315 where
import Data.Coerce
type Heap τ = Int -> Maybe (τ ())
newtype ProcessM τ a = ProcessM (Heap (ProcessM τ) -> τ (a, Heap (ProcessM τ)))
newtype NewProcessM τ a = NewProcessM (ProcessM τ a)
runM :: ProcessM τ a -> τ (a, Heap (ProcessM τ))
runM (ProcessM f) = f (const Nothing)
runM2 :: NewProcessM τ a -> τ (a, Heap (NewProcessM τ))
runM2 = coerce runM
```
GHC 9.4 and GHC 9.9 report an error on that `coerce`:
```
test.hs:14:9: error: [GHC-40404]
• Reduction stack overflow; size = 201
When simplifying the following type: ProcessM τ ()
• In the expression: coerce runM
In an equation for ‘runM2’: runM2 = coerce runM
Suggested fix:
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
|
14 | runM2 = coerce runM
| ^^^^^^
```
I would not have expected this error message; in fact I would have expected that the coercion Just Works (it does not, for good reason below). Though admittedly, this is a gnarly type.
End of bug report.
---
Further diagnosis:
When I change `ProcessM` to a datatype, I'm getting a much nicer error:
```
test.hs:14:9: error: [GHC-18872]
• Couldn't match representation of type: τ (a, Heap (ProcessM τ))
with that of: τ (a, Heap (NewProcessM τ))
arising from a use of ‘coerce’
NB: We cannot know what roles the parameters to ‘τ’ have;
we must assume that the role is nominal
• In the expression: coerce runM
In an equation for ‘runM2’: runM2 = coerce runM
• Relevant bindings include
runM2 :: NewProcessM τ a -> τ (a, Heap (NewProcessM τ))
(bound at test.hs:14:1)
|
14 | runM2 = coerce runM
|
```
Aha, so I need to add a role annotation.
```hs
type role ProcessM representational nominal
```
But this is rejected for a different reason
```
test.hs:9:1: error: [GHC-29178]
• Role mismatch on variable τ:
Annotation says representational but role nominal is required
• while checking a role annotation for ‘ProcessM’
|
9 | type role ProcessM representational nominal
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
That is probably due to the Fixpoint; fair enough. I'd still expect the original program to emit a useful error.https://gitlab.haskell.org/ghc/ghc/-/issues/22644Derive coercions through data constructors2023-01-03T21:16:28ZShea Levyshea@shealevy.comDerive coercions through data constructors<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appr...<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appropriate for a GitLab feature request, include GHC API/plugin
innovations, new low-impact compiler flags, or other similar additions to GHC.
-->
## 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):
```haskell
{-# 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
```https://gitlab.haskell.org/ghc/ghc/-/issues/20937type-checking of `coerce` depends on which newtype constructors are imported2022-01-18T15:12:12ZSebastian Graftype-checking of `coerce` depends on which newtype constructors are importedConsider
```hs
module M where
newtype M m a = MkM (m a)
```
```hs
module Test where
import M (M)
import Data.Coerce
import Data.Functor.Identity
f :: M IO Int -> M IO (Identity Int)
f x = coerce x
```
`Test` won't compile in GHC 8.10...Consider
```hs
module M where
newtype M m a = MkM (m a)
```
```hs
module Test where
import M (M)
import Data.Coerce
import Data.Functor.Identity
f :: M IO Int -> M IO (Identity Int)
f x = coerce x
```
`Test` won't compile in GHC 8.10, 9.0 (haven't tried HEAD yet).
But if I also import the newtype constructor `MkM`, it compiles, presumably because it can look at the definition of `M` to figure out that its use of `a` is representational *if* `IO`'s first type param has a representational role, which it can only do with the information avaialble at its use site.
Why do I need to import `MkM`? Can't GHC do this automatically for me? What if `M` didn't export `MkM`?
This came up in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7329#note_401587, where `EtaReaderT` wraps around `ReaderT` and now `EtaReader` has to export the `ReaderT` newtype constructor or otherwise has to force all use sites to import `Control.Monad.Trans.Reader`, which I'd say is an implementation detail.
Do note that *hiding* the implementation of `M` leads to a degradation in the ability to coerce it, even though doing so would be safe. (Of course the other side of the coin is that use sites might break if we change the implementation of `M` ...)
Is this expected behavior? I was *very* confused by what I thought would just have been a refactoring.
To be clear, I don't want the fact of whether or not I import an unused newtype constructor to influence type-checking. That means I could live with either
1. *Always* unfold newtype definitions, whether it is or can be imported or not. (I see problems, like "the other side of the coin" above.)
2. *Never* unfold newtype definitions to type-check `coerce`. The only means of reasoning about whether a coerce is permitted should be based on inferred or annotated roles.
I'd favor (2), but that would amount to a lot of back compat problems.
---
In order for (2) to be realistic, it seems we'd need higher-order role annotations to encode the necessary information, so that we no longer need to unfold definitions at use sites. E.g.,
```hs
type role IO :: representational
-- so the abstraction of IO in terms of roles is like `(\r -> r) :: Role -> Role`
newtype M m a = MkM (m a)
type role M \rm. representational (rm representational)
-- so the abstraction of M in terms of roles is like `(\rm ra -> worseRole (rm ra) ra) :: (Role -> Role) -> Role -> Role`
```
Then `M IO Int` would compute to `(\rm ra -> worseRole (rm ra) ra) (\r -> r) Representational => worseRole (id Repr.) Repr. => Representational`. *Very* roughly speaking (of course eventually we must relate the two types we coerce). I hope you get the idea.
I think these abstractions can be defined generically, over all kinds (and are overriden by user-defined role annotations).https://gitlab.haskell.org/ghc/ghc/-/issues/19936Odd GND failure/success2021-06-08T14:22:57ZDavid FeuerOdd GND failure/successThere's currently a discussion about whether to change the definition of `MonadTrans` to use `QuantifiedConstraints`:
```haskell
class (forall m. Monad m => Monad (t m)) => MonadTrans t where
lift :: m a -> t m a
```
I wondered if th...There's currently a discussion about whether to change the definition of `MonadTrans` to use `QuantifiedConstraints`:
```haskell
class (forall m. Monad m => Monad (t m)) => MonadTrans t where
lift :: m a -> t m a
```
I wondered if this works with GND. As it turns out, the answer is yes:
```haskell
newtype B t (m :: Type -> Type) a => B (t m a)
deriving (Functor, Applicative, Monad)
-- StandaloneDeriving just to be sure the constraints is
-- what I expect.
deriving instance MonadTrans t => MonadTrans (B t)
```
compiles just fine. But a conceptually very similar idea does not:
```haskell
class MonadTrans t where
lift :: m a -> t m a
liftMonad :: Monad m => Proxy (t m) -> (Monad (t m) => r) -> r
```
This one produces an error,
```
Lift.hs:9:42: error:
• Occurs check: cannot construct the infinite type: t ~ B t
arising from the coercion of the method ‘liftMonad’
from type ‘forall (m :: * -> *) r.
Monad m =>
Proxy (t m) -> (Monad (t m) => r) -> r’
to type ‘forall (m :: * -> *) r.
Monad m =>
Proxy (B t m) -> (Monad (B t m) => r) -> r’
• When deriving the instance for (MonadTrans (B t))
```
Why does one work and not the other? Is there a good reason for that, or should they both succeed or both fail?https://gitlab.haskell.org/ghc/ghc/-/issues/18306Importing a newtype constructor can break typechecking2023-12-15T08:24:04ZDavid FeuerImporting a newtype constructor can break typechecking## Summary
Having a newtype constructor in scope can cause a reduction stack overflow when the program would otherwise typecheck.
## Steps to reproduce
The following comes from [this StackOverflow answer](https://stackoverflow.com/a/62...## Summary
Having a newtype constructor in scope can cause a reduction stack overflow when the program would otherwise typecheck.
## Steps to reproduce
The following comes from [this StackOverflow answer](https://stackoverflow.com/a/62237504/1477667) by @kabuhr.
```haskell
-- HyperFunction.hs
module HyperFunction where
newtype Hyper a b = Hyper { invoke :: Hyper b a -> b }
-- HyperCoerce.hs
module HyperCoerce where
import HyperFunction (Hyper)
-- The next line breaks it
-- import HyperFunction (Hyper (..))
import Data.Coerce
(#.) :: (Coercible c b) => q b c -> Hyper a b -> Hyper a c
(#.) _ = coerce
```
Compiling this as is works. Adding the commented line gives a reduction stack overflow.
## Expected behavior
The modules compile.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/18148ConstrainedClassMethods can trigger un-actionable redundant constraint warnin...2020-05-22T23:35:24ZKoz RossConstrainedClassMethods can trigger un-actionable redundant constraint warnings together with GND## Summary
If you use ``GeneralizedNewtypeDeriving`` (or indeed, ``DerivingVia``) to derive an instance of a type class whose methods have constraints that aren't in the type class head, it is possible to trigger redundant constraint wa...## Summary
If you use ``GeneralizedNewtypeDeriving`` (or indeed, ``DerivingVia``) to derive an instance of a type class whose methods have constraints that aren't in the type class head, it is possible to trigger redundant constraint warnings if the generated code would cause the constraints to be satisfied by whatever the type variables are set to. See the example given in 'steps to reproduce' for a demonstration. These warnings can't be actioned - the only option currently is to disable redundant constraint warnings completely.
## Steps to reproduce
Attempt to compile the following code with ``-Wredundant-constraints`` enabled:
```haskell
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
module Baz where
class Foo a where
bar :: (Num a) => a -> a
bar = (+ 1)
instance Foo Int
newtype Quux a = Quux a
deriving newtype instance Foo (Quux Int)
```
This will emit a redundant constraint warning, as ``Int`` is already an instance of ``Num``.
## Expected behavior
Should compile, emitting no warnings.
## Environment
* GHC version used: 8.10.1
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/17167Role annotations on classes require module-wide IncoherentInstances2020-01-23T19:43:04ZAdam GundryRole annotations on classes require module-wide IncoherentInstancesPer #8773, specifying a non-nominal role for a class parameter requires `IncoherentInstances`:
```hs
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE IncoherentInstances #-}
class C c
type role C phantom
```
For instances, the `IncoherentI...Per #8773, specifying a non-nominal role for a class parameter requires `IncoherentInstances`:
```hs
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE IncoherentInstances #-}
class C c
type role C phantom
```
For instances, the `IncoherentInstances` module-wide `LANGUAGE` pragma has been deprecated in favour of per-instance `{-# INCOHERENT #-}` pragmas. However, there doesn't appear to be an equivalent for `type role` on classes. This is awkward because I do not want the instances of `C` to be marked as incoherent, and hence they cannot be defined in the same module as `C`.
I think it would make sense to be able to use `{-# INCOHERENT #-}` after `type role`, so that it would be accepted without module-wide `IncoherentInstances`.https://gitlab.haskell.org/ghc/ghc/-/issues/15707More liberally kinded coercions for newtypes2019-07-07T18:03:21ZmniipMore liberally kinded coercions for newtypesConsider the infinite data family (possible thanks to #12369):
```hs
data family I :: k -> k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)...Consider the infinite data family (possible thanks to #12369):
```hs
data family I :: k -> k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of eta-contracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k -> *). a ~R I a
forall (a :: k -> l -> *). a ~R I a
forall (a :: k -> l -> m -> *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*-kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x -> I a x
i1 = coerce
...
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15441Data type with phantoms using TypeInType isn't coercible2019-07-07T18:04:53ZglittersharkData type with phantoms using TypeInType isn't coercibleI'm \*pretty\* sure this is a problem with TypeInType in particular. I'd expect the following to compile:
```hs
{-# LANGUAGE GADTs, TypeInType, TypeApplications #-}
module Bug where
import Prelude
import Data.Coerce
import Data.Kind
d...I'm \*pretty\* sure this is a problem with TypeInType in particular. I'd expect the following to compile:
```hs
{-# LANGUAGE GADTs, TypeInType, TypeApplications #-}
module Bug where
import Prelude
import Data.Coerce
import Data.Kind
data Foo a = Foo
data Bar (a :: Type) (b :: Foo a) where
Bar :: Bar a 'Foo
x = coerce @(Bar Int 'Foo) @(Bar Bool 'Foo)
```
But it doesn't
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Data type with phantoms using TypeInType isn't coercible","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm *pretty* sure this is a problem with TypeInType in particular. I'd expect the following to compile:\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeInType, TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Prelude\r\nimport Data.Coerce\r\nimport Data.Kind\r\n\r\ndata Foo a = Foo\r\n\r\ndata Bar (a :: Type) (b :: Foo a) where\r\n Bar :: Bar a 'Foo\r\n\r\nx = coerce @(Bar Int 'Foo) @(Bar Bool 'Foo)\r\n}}}\r\n\r\nBut it doesn't","type_of_failure":"OtherFailure","blocking":[]} -->Research neededhttps://gitlab.haskell.org/ghc/ghc/-/issues/14694Incompleteness in the Coercible constraint solver2023-12-15T08:12:32ZIcelandjackIncompleteness in the Coercible constraint solver```
$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
Prelude> newtype WF f a = WF (f a)
Prelude> import Data.Coerce
Prelude Data.Coerce> :set -XFlexibleContexts
Prelude Data.Coerce> :t coerce ...```
$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
Prelude> newtype WF f a = WF (f a)
Prelude> import Data.Coerce
Prelude Data.Coerce> :set -XFlexibleContexts
Prelude Data.Coerce> :t coerce :: Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)
<interactive>:1:1: error:
• Couldn't match representation of type ‘cat1 a1 b1’
with that of ‘a1 -> WF f1 b1’
arising from a use of ‘coerce’
• In the expression:
coerce ::
Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)
```
I'm not sure if I've filed this before or if it's even a bug.
But we know that `Coercible (a -> f b) (a -> WF f b)` so why doesn't this work?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Can't coerce given assumptions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n$ ghci -ignore-dot-ghci\r\nGHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help\r\nPrelude> newtype WF f a = WF (f a)\r\nPrelude> import Data.Coerce\r\nPrelude Data.Coerce> :set -XFlexibleContexts \r\nPrelude Data.Coerce> :t coerce :: Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)\r\n\r\n<interactive>:1:1: error:\r\n • Couldn't match representation of type ‘cat1 a1 b1’\r\n with that of ‘a1 -> WF f1 b1’\r\n arising from a use of ‘coerce’\r\n • In the expression:\r\n coerce ::\r\n Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)\r\n}}}\r\n\r\nI'm not sure if I've filed this before or if it's even a bug.\r\n\r\nBut we know that `Coercible (a -> f b) (a -> WF f b)` so why doesn't this work?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14386GHC doesn't allow Coercion between partly-saturated type constructors2019-07-07T18:17:13ZIcelandjackGHC doesn't allow Coercion between partly-saturated type constructorsIf I define an "opposite category" `newtype Op cat a b = Op (cat b a)` then representationally it forms an involution: applying `Op` twice gives the same representation as not applying it at all
```
$ ... -ignore-dot-ghci
GHCi, version ...If I define an "opposite category" `newtype Op cat a b = Op (cat b a)` then representationally it forms an involution: applying `Op` twice gives the same representation as not applying it at all
```
$ ... -ignore-dot-ghci
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Coerce
Prelude Data.Coerce> import Data.Type.Coercion
Prelude Data.Coerce Data.Type.Coercion> newtype Op cat a b = Op (cat b a)
Prelude Data.Coerce Data.Type.Coercion> :t coerce :: Op (Op cat) a b -> cat a b
coerce :: Op (Op cat) a b -> cat a b :: Op (Op cat) a b -> cat a b
Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat) a b) (cat a b)
Coercion :: Coercion (Op (Op cat) a b) (cat a b)
:: Coercion (Op (Op cat) a b) (cat a b)
```
But these don't work:
```
Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat) a) (cat a)
<interactive>:1:1: error:
• Couldn't match representation of type ‘Op (Op cat1) a1’
with that of ‘cat1 a1’
arising from a use of ‘Coercion’
• In the expression: Coercion :: Coercion (Op (Op cat) a) (cat a)
Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat) cat
<interactive>:1:38: error:
parse error (possibly incorrect indentation or mismatched brackets)
Prelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat)) cat
<interactive>:1:1: error:
• Couldn't match representation of type ‘cat1’
with that of ‘Op (Op cat1)’
arising from a use of ‘Coercion’
‘cat1’ is a rigid type variable bound by
an expression type signature:
forall (cat1 :: * -> * -> *). Coercion (Op (Op cat1)) cat1
at <interactive>:1:13-38
• In the expression: Coercion :: Coercion (Op (Op cat)) cat
```
I'm wondering if this is intentional
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC doesn't allow Coercion between partly-saturated type constructors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["roles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I define an \"opposite category\" `newtype Op cat a b = Op (cat b a)` then representationally it forms an involution: applying `Op` twice gives the same representation as not applying it at all\r\n\r\n{{{\r\n$ ... -ignore-dot-ghci\r\nGHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import Data.Coerce\r\nPrelude Data.Coerce> import Data.Type.Coercion \r\nPrelude Data.Coerce Data.Type.Coercion> newtype Op cat a b = Op (cat b a)\r\nPrelude Data.Coerce Data.Type.Coercion> :t coerce :: Op (Op cat) a b -> cat a b\r\ncoerce :: Op (Op cat) a b -> cat a b :: Op (Op cat) a b -> cat a b\r\nPrelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat) a b) (cat a b)\r\nCoercion :: Coercion (Op (Op cat) a b) (cat a b)\r\n :: Coercion (Op (Op cat) a b) (cat a b)\r\n}}}\r\n\r\nBut these don't work:\r\n\r\n{{{\r\nPrelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat) a) (cat a)\r\n\r\n<interactive>:1:1: error:\r\n • Couldn't match representation of type ‘Op (Op cat1) a1’\r\n with that of ‘cat1 a1’\r\n arising from a use of ‘Coercion’\r\n • In the expression: Coercion :: Coercion (Op (Op cat) a) (cat a)\r\nPrelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat) cat\r\n\r\n<interactive>:1:38: error:\r\n parse error (possibly incorrect indentation or mismatched brackets)\r\nPrelude Data.Coerce Data.Type.Coercion> :t Coercion :: Coercion (Op (Op cat)) cat\r\n\r\n<interactive>:1:1: error:\r\n • Couldn't match representation of type ‘cat1’\r\n with that of ‘Op (Op cat1)’\r\n arising from a use of ‘Coercion’\r\n ‘cat1’ is a rigid type variable bound by\r\n an expression type signature:\r\n forall (cat1 :: * -> * -> *). Coercion (Op (Op cat1)) cat1\r\n at <interactive>:1:13-38\r\n • In the expression: Coercion :: Coercion (Op (Op cat)) cat\r\n}}}\r\n\r\nI'm wondering if this is intentional","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14362Allow: Coercing (a:~:b) to (b:~:a)2019-07-07T18:17:19ZIcelandjackAllow: Coercing (a:~:b) to (b:~:a)Is there \*any\* sensible way to enable coercing [(:\~:)](https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type-Equality.html#t::-126-:) swapping its arguments
```hs
coerce :: a:~:b -> b:~:a
```
Same for [Coercion](https://h...Is there \*any\* sensible way to enable coercing [(:\~:)](https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type-Equality.html#t::-126-:) swapping its arguments
```hs
coerce :: a:~:b -> b:~:a
```
Same for [Coercion](https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type-Coercion.html#t:Coercion)
```hs
coerce :: Coercion a b -> Coercion b a
```
Thanks!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.2.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Allow: Coercing (a:~:b) to (b:~:a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["roles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Is there *any* sensible way to enable coercing [https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type-Equality.html#t::-126-: (:~:)] swapping its arguments\r\n\r\n{{{#!hs\r\ncoerce :: a:~:b -> b:~:a\r\n}}}\r\n\r\nSame for [https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type-Coercion.html#t:Coercion Coercion]\r\n\r\n{{{#!hs\r\ncoerce :: Coercion a b -> Coercion b a\r\n}}}\r\n\r\nThanks!","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14292Coercing between constraints of newtypes2019-07-07T18:17:35ZIcelandjackCoercing between constraints of newtypesThis doesn't work
```hs
{-# Language ConstraintKinds #-}
{-# Language GADTs #-}
import Data.Coerce
newtype USD = USD Int
data Dict c where
Dict :: c => Dict c
num :: Dict (Num Int) -> Dict (Num USD)
num = coerce
```
but this does...This doesn't work
```hs
{-# Language ConstraintKinds #-}
{-# Language GADTs #-}
import Data.Coerce
newtype USD = USD Int
data Dict c where
Dict :: c => Dict c
num :: Dict (Num Int) -> Dict (Num USD)
num = coerce
```
but this does
```hs
data NUM a = NUM (a -> a -> a)
num' :: NUM Int -> NUM USD
num' = coerce
```
is this a fundamental limitation?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.2.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Coercing between constraints of newtypes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"This doesn't work\r\n\r\n{{{#!hs\r\n{-# Language ConstraintKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Coerce\r\n\r\nnewtype USD = USD Int\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\nnum :: Dict (Num Int) -> Dict (Num USD)\r\nnum = coerce\r\n}}}\r\n\r\nbut this does\r\n\r\n{{{#!hs\r\ndata NUM a = NUM (a -> a -> a)\r\n\r\nnum' :: NUM Int -> NUM USD\r\nnum' = coerce\r\n}}}\r\n\r\nis this a fundamental limitation?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13358Role ranges (allow decomposition on newtypes)2019-07-07T18:22:17ZEdward Z. YangRole ranges (allow decomposition on newtypes)Extracted from #13140.
Today, there is a strange asymmetry between data types, for which the decomposition rule holds (if `T A ~R T B` then `A ~ρ B`, where ρ is the role of the type), and newtypes, for which the decomposition rule is un...Extracted from #13140.
Today, there is a strange asymmetry between data types, for which the decomposition rule holds (if `T A ~R T B` then `A ~ρ B`, where ρ is the role of the type), and newtypes, for which the decomposition rule is unsound.
I believe the root cause of this problem is the fact that we only maintain a single role per type parameter, while in fact what we need is a role \*range\* (i.e., and lower and upper role bound) to specify what inferences can be made about a type. Here's how it works.
Every type parameter is ascribed a role range, specifying the possible roles by which the type parameter might possibly be used. For example, if I write `data T a = MkT a`, `a` is used exactly at representational role, but we could also say that a \*might\* be used nominally, giving the role range nominal-representational.
The lower bound (nominal is lowest in subroling) specifies at what role the application rule is valid: if I say that the role is at least nominal, then I must provide `a ~N b` evidence to show that `T a ~R T b`. The upper bound (phantom is highest) specifies at what role the decomposition rule is valid. If I say that the role is at most phantom, I learn nothing from decomposition; but if I say the role is at most representational, when `T A ~R T B`, I learn `A ~R B`. Clearly, the role range nominal-phantom permits the most implementations, but gives the client the least information about equalities.
How do we tell if a role range is compatible with a type? The lower bound (what we call a role today) is computed by propagating roles through, but allowing substitution of roles as per the subroling relationship `N <= R <= P`. To compute the upper bound, we do exactly the same rules, but with the opposite subroling relation: `P <= R <= N`.
Some examples:
```
type role T representational..representational
newtype T a = MkT a
-- T a ~R T b implies a ~R b
type role T nominal..representational -- NB: nominal..nominal illegal!
newtype T a = MkT a
-- T a ~R T b implies a ~R b, BUT
-- a ~R b is insufficient to prove T a ~R T b (you need a ~N b)
type role T nominal..phantom -- NB: nominal..representational illegal!
newtype T a = MkT Int
-- T a ~R T b implies a ~P b (i.e. we don't learn anything)
-- a ~N b implies T a ~R T b
```
Richard wonders if we could use this to solve the "recursive newtype unwrapping" problem. Unfortunately, because our solver is guess-free, we must also maintain the most precise role for every type constructor. See #13140\##13358https://gitlab.haskell.org/ghc/ghc/-/issues/9118Can't eta-reduce representational coercions2021-07-30T14:34:57ZRichard Eisenbergrae@richarde.devCan't eta-reduce representational coercionsWhen I say
```
import Data.Type.Coercion
import Data.Coerce
import Data.Proxy
eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g
eta2 _ = Coercion
```
I get
```
Could not coerce from ‘f’ to ‘g’
because ‘f’ and ‘g’ are...When I say
```
import Data.Type.Coercion
import Data.Coerce
import Data.Proxy
eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g
eta2 _ = Coercion
```
I get
```
Could not coerce from ‘f’ to ‘g’
because ‘f’ and ‘g’ are different types.
arising from a use of ‘Coercion’
from the context (Coercible (f a) (g a))
bound by the type signature for
eta2 :: Coercible (f a) (g a) => Proxy a -> Coercion f g
at /Users/rae/temp/Roles.hs:5:9-56
In the expression: Coercion
In an equation for ‘eta2’: eta2 _ = Coercion
```
Unlike the case for #9117, this one is *not* expressible in Core. (At least, I don't see a way to do it.) So, to do this, we would have to update Core and then update the constraint solver. I *do* think this would be type safe. But, I also think it's reasonable to wait for someone with a real use case to shout before doing this. The only use case I have is to be able to do this:
```
-- says that a's parameter is representational
class Rep (a :: k1 -> k2) where
co :: Coercible x y => Coercible (a x) (a x)
instance Rep f => Rep (Compose f) where ...
```https://gitlab.haskell.org/ghc/ghc/-/issues/9112support for deriving Vector/MVector instances2019-07-07T18:41:52Zjwlatosupport for deriving Vector/MVector instancesSince ghc-7.8, the following is no longer possible:
```
-- simplified example taken from the vector package
class MVectorClass (v :: * -> * -> *) a where
basicLength :: v s a -> Int
data family MVector s a
data instance MVector s ...Since ghc-7.8, the following is no longer possible:
```
-- simplified example taken from the vector package
class MVectorClass (v :: * -> * -> *) a where
basicLength :: v s a -> Int
data family MVector s a
data instance MVector s Int -- implementation not important
newtype Age = Age Int deriving (MVectorClass MVector) -- rejected
```
Following from discussion in #8177, to enable this ghc would need to support data families with representational matching, such that `MVector s Int` and `MVector s Age` are representationally equal.
This has broken some code that previously worked, however as there are some workarounds I'm not sure how important it is.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.8.2 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"data families with representational matching","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Since ghc-7.8, the following is no longer possible:\r\n\r\n{{{\r\n-- simplified example taken from the vector package\r\nclass MVectorClass (v :: * -> * -> *) a where\r\n basicLength :: v s a -> Int\r\n\r\ndata family MVector s a\r\n\r\ndata instance MVector s Int -- implementation not important\r\n\r\nnewtype Age = Age Int deriving (MVectorClass MVector) -- rejected\r\n}}}\r\n\r\nFollowing from discussion in #8177, to enable this ghc would need to support data families with representational matching, such that `MVector s Int` and `MVector s Age` are representationally equal.\r\n\r\nThis has broken some code that previously worked, however as there are some workarounds I'm not sure how important it is.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/8177Roles for type families2023-03-03T14:56:11ZSimon Peyton JonesRoles for type familiesNow that we have [roles](roles), it might be helpful to be able to give a role signature for a data/type family.
At the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus
```
data fam...Now that we have [roles](roles), it might be helpful to be able to give a role signature for a data/type family.
At the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus
```
data family D a -- Parameter conservatively assumed to be N
class C a where
op :: D a -> a
instance C Int where ....
newtype N a = MkN a deriving( C ) -- Rejected
```
The generalised-newtype-deriving clause `deriving( C )` is rejected because `D` might use its parameter at role `N` thus:
```
data instance D [b] = MkD (F b) -- F is a type function
```
It would be strictly more expressive if we could
- **Declare** the roles of D's arguments (as we can declare their kinds). E.g.
```
data family D a@R
```
- **Check** that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance:
```
data instance D [b] = MkD (F b) -- F is a type function
```
I think there is no technical difficulty here. Just a question of doing it.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Roles for type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Now that we have [wiki:Roles roles], it might be helpful to be able to give a role signature for a data/type family.\r\n\r\nAt the moment, data/type family constructors have all parameters conservatively assigned to be role `N`. Thus\r\n{{{\r\ndata family D a -- Parameter conservatively assumed to be N\r\n\r\nclass C a where\r\n op :: D a -> a\r\n\r\ninstance C Int where ....\r\n\r\nnewtype N a = MkN a deriving( C ) -- Rejected\r\n}}}\r\nThe generalised-newtype-deriving clause `deriving( C )` is rejected because `D` might use its parameter at role `N` thus:\r\n{{{\r\ndata instance D [b] = MkD (F b) -- F is a type function\r\n}}}\r\nIt would be strictly more expressive if we could\r\n * '''Declare''' the roles of D's arguments (as we can declare their kinds). E.g.\r\n{{{\r\ndata family D a@R\r\n}}}\r\n * '''Check''' that each family instance obeys that role signature. E.g. given the preceding role signature, reject this instance:\r\n{{{\r\ndata instance D [b] = MkD (F b) -- F is a type function\r\n}}}\r\n\r\nI think there is no technical difficulty here. Just a question of doing it.","type_of_failure":"OtherFailure","blocking":[]} -->⊥Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev