GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:03:25Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15694GHC panic from pattern synonym, "Type-correct unfilled coercion hole"2019-07-07T18:03:25ZIcelandjackGHC panic from pattern synonym, "Type-correct unfilled coercion hole"```hs
{-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, KindSignatures, GADTs #-}
import Data.Kind
import Data.Type.Equality
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(...```hs
{-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, KindSignatures, GADTs #-}
import Data.Kind
import Data.Type.Equality
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
pattern ASSO :: () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks) (ks1 :: Type) k1 (a2 :: k1) (ctx1 :: Ctx ks1) a3. (kind ~ (k -> ks), a ~~ f, b ~~ (a1 :&: ctx), ks ~ (k1 -> ks1), ctx ~~ (a2 :&: E), ks1 ~ Type, f a1 a2 ~~ a3) => a3 -> ApplyT kind a b
pattern ASSO a = AS (AS (AO a))
```
```
$ ghci -ignore-dot-ghci 465.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 465.hs, interpreted )
WARNING: file compiler/types/TyCoRep.hs, line 2378
in_scope InScope {kind_a1Cw a_a1Cx b_a1Cy ks_a1Cz k_a1CA f_a1CB
a1_a1CC ctx_a1CD ks1_a1CE k1_a1CF a2_a1CG ctx1_a1CH a3_a1CI
k0_a1F8}
tenv [a1Cw :-> kind_a1Cw[sk:0], a1Cx :-> a_a1Cx[sk:0],
a1Cy :-> b_a1Cy[sk:0], a1Cz :-> ks_a1Cz[sk:0],
a1CA :-> k_a1CA[sk:0], a1CB :-> f_a1CB[sk:0],
a1CC :-> a1_a1CC[sk:0], a1CD :-> ctx_a1CD[sk:0],
a1CE :-> ks1_a1CE[sk:0], a1CF :-> k1_a1CF[sk:0],
a1CG :-> a2_a1CG[sk:0], a1CH :-> ctx1_a1CH[sk:0],
a1CI :-> a3_a1CI[sk:0]]
cenv []
tys [kind_a1Cw[sk:1] ~ (k_a1CA[sk:2] -> ks_a1Cz[sk:2]),
a_a1Cx[sk:1] ~~ f_a1CB[sk:2],
b_a1Cy[sk:1] ~~ (a1_a1CC[sk:2] ':&: ctx_a1CD[sk:2]),
ks_a1Cz[sk:2] ~ (k1_a1CF[sk:2] -> ks1_a1CE[sk:2]),
ctx_a1CD[sk:2] ~~ (a2_a1CG[sk:2] ':&: 'E), ks1_a1CE[sk:2] ~ *,
(f_a1CB[sk:2] a1_a1CC[sk:2] |> {co_a1Fc}) a2_a1CG[sk:2]
~~ a3_a1CI[sk:2]]
cos []
needInScope [a1F8 :-> k0_a1F8[sk:2], a1Fc :-> co_a1Fc]
WARNING: file compiler/types/TyCoRep.hs, line 2378
in_scope InScope {kind_a1Cw a_a1Cx b_a1Cy k0_a1HA ks_a1HB k_a1HC
f_a1HD a1_a1HE ctx_a1HF ks1_a1HG k1_a1HH a2_a1HI ctx1_a1HJ a3_a1HK}
tenv [a1Cz :-> ks_a1HB[tau:4], a1CA :-> k_a1HC[tau:4],
a1CB :-> f_a1HD[tau:4], a1CC :-> a1_a1HE[tau:4],
a1CD :-> ctx_a1HF[tau:4], a1CE :-> ks1_a1HG[tau:4],
a1CF :-> k1_a1HH[tau:4], a1CG :-> a2_a1HI[tau:4],
a1CH :-> ctx1_a1HJ[tau:4], a1CI :-> a3_a1HK[tau:4],
a1F8 :-> k0_a1HA[tau:4]]
cenv []
tys [kind_a1Cw[sk:0] ~ (k_a1CA[sk:0] -> ks_a1Cz[sk:0]),
a_a1Cx[sk:0] ~~ f_a1CB[sk:0],
b_a1Cy[sk:0] ~~ (a1_a1CC[sk:0] ':&: ctx_a1CD[sk:0]),
ks_a1Cz[sk:0] ~ (k1_a1CF[sk:0] -> ks1_a1CE[sk:0]),
ctx_a1CD[sk:0] ~~ (a2_a1CG[sk:0] ':&: 'E), ks1_a1CE[sk:0] ~ *,
(f_a1CB[sk:0] a1_a1CC[sk:0] |> {co_a1Fc}) a2_a1CG[sk:0]
~~ a3_a1CI[sk:0]]
cos []
needInScope [a1Cw :-> kind_a1Cw[sk:0], a1Cx :-> a_a1Cx[sk:0],
a1Cy :-> b_a1Cy[sk:0], a1Fc :-> co_a1Fc]
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180828 for x86_64-unknown-linux):
ASSERT failed!
Type-correct unfilled coercion hole {co_a1Fc}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1716:99 in ghc:TcHsSyn
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15693Abstracting out pattern into a pattern synonym fails with scary error2019-07-07T18:03:25ZIcelandjackAbstracting out pattern into a pattern synonym fails with scary errorThis **works**
```hs
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: k...This **works**
```hs
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
foo :: ApplyT(Type -> Type -> Type) Either a -> ()
foo (ASSO (Left a)) = ()
pattern ASSO a = AS (AS (AO a))
```
but then you might think, let's give a name (pattern synonym) to `ASSO (Left a)`
This **fails**
```hs
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
pattern ASSO a = AS (AS (AO a))
pattern ASSOLeft a = ASSO (Left a)
```
```
$ ghci -ignore-dot-ghci 464.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/464.hs, interpreted )
hs/464.hs:16:22: error:
• Couldn't match type ‘k1’ with ‘*’
‘k1’ is a rigid type variable bound by
the signature for pattern synonym ‘ASSOLeft’
at hs/464.hs:16:1-34
Expected type: ApplyT kind a b
Actual type: ApplyT (* -> * -> *) Either (a1 ':&: (a20 ':&: 'E))
• In the expression: ASSO (Left a)
In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)
|
16 | pattern ASSOLeft a = ASSO (Left a)
| ^^^^^^^^^^^^^
hs/464.hs:16:28: error:
• Could not deduce: k1 ~ *
from the context: (kind ~ (k -> ks), a ~~ f, b ~~ (a2 ':&: ctx),
ks ~ (k1 -> ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,
f1 a3 ~~ a4, ctx1 ~~ 'E)
bound by a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
-> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 -> ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:22-34
‘k1’ is a rigid type variable bound by
a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx
ks) ks1 k1 (f1 :: k1
-> ks1) (a2 :: k1) (ctx1 :: Ctx
ks1) a3.
(kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1),
f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,
ctx1 ~~ 'E) =>
a3 -> ApplyT kind a b,
in a pattern synonym declaration
at hs/464.hs:16:22-34
When matching types
a3 :: k1
b0 :: *
Expected type: a4
Actual type: Either a1 b0
• In the pattern: Left a
In the pattern: ASSO (Left a)
In the declaration for pattern synonym ‘ASSOLeft’
|
16 | pattern ASSOLeft a = ASSO (Left a)
| ^^^^^^
Failed, no modules loaded.
Prelude>
```
----
Can I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| 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":"Abstracting out pattern into a pattern synonym fails with scary error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This '''works'''\r\n\r\n{{{#!hs\r\n{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type -> Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a -> Ctx(as) -> Ctx(a -> as)\r\n\r\ndata ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where\r\n AO :: a -> ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n -> ApplyT(k -> ks) f (a:&:ctx)\r\n\r\nfoo :: ApplyT(Type -> Type -> Type) Either a -> ()\r\nfoo (ASSO (Left a)) = ()\r\n\r\npattern ASSO a = AS (AS (AO a))\r\n}}}\r\n\r\nbut then you might think, let's give a name (pattern synonym) to `ASSO (Left a)`\r\n\r\nThis '''fails'''\r\n{{{#!hs\r\n{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type -> Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a -> Ctx(as) -> Ctx(a -> as)\r\n\r\ndata ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where\r\n AO :: a -> ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n -> ApplyT(k -> ks) f (a:&:ctx)\r\n\r\npattern ASSO a = AS (AS (AO a))\r\n\r\npattern ASSOLeft a = ASSO (Left a)\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 464.hs\r\nGHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/464.hs, interpreted )\r\n\r\nhs/464.hs:16:22: error:\r\n • Couldn't match type ‘k1’ with ‘*’\r\n ‘k1’ is a rigid type variable bound by\r\n the signature for pattern synonym ‘ASSOLeft’\r\n at hs/464.hs:16:1-34\r\n Expected type: ApplyT kind a b\r\n Actual type: ApplyT (* -> * -> *) Either (a1 ':&: (a20 ':&: 'E))\r\n • In the expression: ASSO (Left a)\r\n In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a)\r\n |\r\n16 | pattern ASSOLeft a = ASSO (Left a)\r\n | ^^^^^^^^^^^^^\r\n\r\nhs/464.hs:16:28: error:\r\n • Could not deduce: k1 ~ *\r\n from the context: (kind ~ (k -> ks), a ~~ f, b ~~ (a2 ':&: ctx),\r\n ks ~ (k1 -> ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *,\r\n f1 a3 ~~ a4, ctx1 ~~ 'E)\r\n bound by a pattern with pattern synonym:\r\n ASSO :: forall kind (a :: kind) (b :: Ctx kind).\r\n () =>\r\n forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx\r\n ks) ks1 k1 (f1 :: k1\r\n -> ks1) (a2 :: k1) (ctx1 :: Ctx\r\n ks1) a3.\r\n (kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1),\r\n f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,\r\n ctx1 ~~ 'E) =>\r\n a3 -> ApplyT kind a b,\r\n in a pattern synonym declaration\r\n at hs/464.hs:16:22-34\r\n ‘k1’ is a rigid type variable bound by\r\n a pattern with pattern synonym:\r\n ASSO :: forall kind (a :: kind) (b :: Ctx kind).\r\n () =>\r\n forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx\r\n ks) ks1 k1 (f1 :: k1\r\n -> ks1) (a2 :: k1) (ctx1 :: Ctx\r\n ks1) a3.\r\n (kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1),\r\n f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3,\r\n ctx1 ~~ 'E) =>\r\n a3 -> ApplyT kind a b,\r\n in a pattern synonym declaration\r\n at hs/464.hs:16:22-34\r\n When matching types\r\n a3 :: k1\r\n b0 :: *\r\n Expected type: a4\r\n Actual type: Either a1 b0\r\n • In the pattern: Left a\r\n In the pattern: ASSO (Left a)\r\n In the declaration for pattern synonym ‘ASSOLeft’\r\n |\r\n16 | pattern ASSOLeft a = ASSO (Left a)\r\n | ^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\n----\r\n\r\nCan I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14747DisambiguateRecordFields fails for PatternSynonyms2019-07-07T18:15:46ZAdam GundryDisambiguateRecordFields fails for PatternSynonymsConsider:
```hs
{-# LANGUAGE PatternSynonyms #-}
module A where
pattern S{x} = [x]
```
```hs
{-# LANGUAGE PatternSynonyms, DisambiguateRecordFields #-}
module B where
import A
pattern T{x} = [x]
e = S { x = 42 }
```
Compiling mo...Consider:
```hs
{-# LANGUAGE PatternSynonyms #-}
module A where
pattern S{x} = [x]
```
```hs
{-# LANGUAGE PatternSynonyms, DisambiguateRecordFields #-}
module B where
import A
pattern T{x} = [x]
e = S { x = 42 }
```
Compiling module B fails with `Ambiguous occurrence ‘x’` in the definition of `e`. In principle, `DisambiguateRecordFields` should select the field belonging to the `S` "data constructor". However, the current implementation of this works by identifying the parent type constructor, which doesn't exist for a pattern synonym.
This continues to fail if `T` is replaced by a data type with a field `x`. If `S` is replaced by a data type, however, it starts working.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #11283 |
| Blocking | |
| CC | mpickering |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"DisambiguateRecordFields fails for PatternSynonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[11283],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":["mpickering"],"type":"Bug","description":"Consider:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PatternSynonyms #-}\r\n\r\nmodule A where\r\n\r\npattern S{x} = [x]\r\n}}}\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PatternSynonyms, DisambiguateRecordFields #-}\r\n\r\nmodule B where\r\n\r\nimport A\r\n\r\npattern T{x} = [x]\r\n\r\ne = S { x = 42 }\r\n}}}\r\n\r\nCompiling module B fails with `Ambiguous occurrence ‘x’` in the definition of `e`. In principle, `DisambiguateRecordFields` should select the field belonging to the `S` \"data constructor\". However, the current implementation of this works by identifying the parent type constructor, which doesn't exist for a pattern synonym.\r\n\r\nThis continues to fail if `T` is replaced by a data type with a field `x`. If `S` is replaced by a data type, however, it starts working.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc/-/issues/9793Some as-patterns could be accepted in pattern synonyms2019-07-07T18:39:01ZGergő ÉrdiSome as-patterns could be accepted in pattern synonymsCurrently all as-patterns are rejected in pattern synonym definitions, to avoid situations like
```
pattern P x y <- x@(y:_)
```
since there's no valid reason to be able to then write something like
```
f [True] False = ...
```
this ...Currently all as-patterns are rejected in pattern synonym definitions, to avoid situations like
```
pattern P x y <- x@(y:_)
```
since there's no valid reason to be able to then write something like
```
f [True] False = ...
```
this would just lead to confusion.
However, I think we could accept as-patterns where the body of the as-pattern doesn't contain any variable bindings that are accessible via the pattern synonym. In other words, this should be OK:
```
pattern P x <- x@(y:_)
```
since it's exactly equivalent to
```
pattern P x <- x@(_:_)
```
which I don't think is as confusing as the other example.
I haven't really made up my mind yet if these should be bidirectional; but they certainly could be, by just ignoring the body of the as-pattern in the wrapper; so the following two would be equivalent:
```
pattern P1 x = [x@(y:_)]
pattern P2 x <- [x@(y:_)]
where
P2 x = [x]
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Some as-patterns could be accepted in pattern synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"cactus"},"version":"7.8.3","keywords":["pattern","synonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Currently all as-patterns are rejected in pattern synonym definitions, to avoid situations like\r\n\r\n\r\n{{{\r\npattern P x y <- x@(y:_)\r\n}}}\r\n\r\nsince there's no valid reason to be able to then write something like\r\n\r\n{{{\r\nf [True] False = ...\r\n}}}\r\n\r\nthis would just lead to confusion.\r\n\r\nHowever, I think we could accept as-patterns where the body of the as-pattern doesn't contain any variable bindings that are accessible via the pattern synonym. In other words, this should be OK:\r\n\r\n{{{\r\npattern P x <- x@(y:_)\r\n}}}\r\n\r\nsince it's exactly equivalent to\r\n\r\n{{{\r\npattern P x <- x@(_:_)\r\n}}}\r\n\r\nwhich I don't think is as confusing as the other example.\r\n\r\nI haven't really made up my mind yet if these should be bidirectional; but they certainly could be, by just ignoring the body of the as-pattern in the wrapper; so the following two would be equivalent:\r\n\r\n{{{\r\npattern P1 x = [x@(y:_)]\r\npattern P2 x <- [x@(y:_)]\r\n where\r\n P2 x = [x]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Gergő ÉrdiGergő Érdi