GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:38:39Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/9879Panic with partial type signatures2019-07-07T18:38:39ZKrzysztof GogolewskiPanic with partial type signaturesAttempting to check kind of type hole `_` in GHCi or putting it in a TH quotation causes a panic `rnHsTyKi HsWildcardTy`:
```
:kind _
let x = [t|_|]
```
<details><summary>Trac metadata</summary>
| Trac field | Value ...Attempting to check kind of type hole `_` in GHCi or putting it in a TH quotation causes a panic `rnHsTyKi HsWildcardTy`:
```
:kind _
let x = [t|_|]
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.9 |
| Type | Bug |
| 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":"Panic with partial type signatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.9","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Attempting to check kind of type hole `_` in GHCi or putting it in a TH quotation causes a panic `rnHsTyKi HsWildcardTy`:\r\n\r\n{{{\r\n:kind _\r\n\r\nlet x = [t|_|]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1thomaswthomaswhttps://gitlab.haskell.org/ghc/ghc/-/issues/9318Type error reported in wrong place with repeated type family expressions2019-07-07T18:40:54ZRichard Eisenbergrae@richarde.devType error reported in wrong place with repeated type family expressionsWhen I say
```
{-# LANGUAGE TypeFamilies #-}
type family F x
type instance F Int = Bool
foo :: F Int -> ()
foo True = ()
bar :: F Int -> ()
bar 'x' = ()
```
I get
```
/Users/rae/temp/Bug.hs:7:5:
Couldn't match type ‘Char’ with ...When I say
```
{-# LANGUAGE TypeFamilies #-}
type family F x
type instance F Int = Bool
foo :: F Int -> ()
foo True = ()
bar :: F Int -> ()
bar 'x' = ()
```
I get
```
/Users/rae/temp/Bug.hs:7:5:
Couldn't match type ‘Char’ with ‘Bool’
Expected type: F Int
Actual type: Bool
In the pattern: True
In an equation for ‘foo’: foo True = ()
/Users/rae/temp/Bug.hs:10:5:
Couldn't match type ‘Bool’ with ‘Char’
Expected type: F Int
Actual type: Char
In the pattern: 'x'
In an equation for ‘bar’: bar 'x' = ()
```
The second error is most certainly correct, but the first one is most certainly not. Note that the first error is reported on the definition of `foo`, which should type-check. Also, the "Couldn't match ..." bit doesn't correspond at all with the expected/actual bit. And, the expected/actual bit shows two types that are in fact equal.
This behavior can be seen in HEAD (as of Jul. 2), 7.8.3, and 7.8.2. This is a regression from 7.6.3, where this behavior does not appear.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | Bug |
| 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":"Type error reported in wrong place with repeated type family expressions","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family F x\r\ntype instance F Int = Bool\r\n\r\nfoo :: F Int -> ()\r\nfoo True = ()\r\n\r\nbar :: F Int -> ()\r\nbar 'x' = ()\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n/Users/rae/temp/Bug.hs:7:5:\r\n Couldn't match type ‘Char’ with ‘Bool’\r\n Expected type: F Int\r\n Actual type: Bool\r\n In the pattern: True\r\n In an equation for ‘foo’: foo True = ()\r\n\r\n/Users/rae/temp/Bug.hs:10:5:\r\n Couldn't match type ‘Bool’ with ‘Char’\r\n Expected type: F Int\r\n Actual type: Char\r\n In the pattern: 'x'\r\n In an equation for ‘bar’: bar 'x' = ()\r\n}}}\r\n\r\nThe second error is most certainly correct, but the first one is most certainly not. Note that the first error is reported on the definition of `foo`, which should type-check. Also, the \"Couldn't match ...\" bit doesn't correspond at all with the expected/actual bit. And, the expected/actual bit shows two types that are in fact equal.\r\n\r\nThis behavior can be seen in HEAD (as of Jul. 2), 7.8.3, and 7.8.2. This is a regression from 7.6.3, where this behavior does not appear.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/10078tcPluginStop of a type checker plugin is not called if an error occurs2019-07-07T18:37:39ZjbrackertcPluginStop of a type checker plugin is not called if an error occursWhen a module using a type checker plugin produces a compiler error the clean up function `tcPluginStop` of the plugin is not called.
I am not sure if this is intended, but according to the description of the wiki page (Plugins/TypeChec...When a module using a type checker plugin produces a compiler error the clean up function `tcPluginStop` of the plugin is not called.
I am not sure if this is intended, but according to the description of the wiki page (Plugins/TypeChecker) this should always be called.
### Test plugin
`MyPlugin.hs`:
```hs
module MyPlugin
( plugin ) where
import Plugins
import TcRnTypes
import TcPluginM
plugin :: Plugin
plugin = defaultPlugin
{ tcPlugin = \clos -> Just $ TcPlugin
{ tcPluginInit = tcPluginIO $ putStrLn ">>> Plugin Init"
, tcPluginSolve = \_ _ _ _ -> do
tcPluginIO $ putStrLn ">>> Plugin Solve"
return $ TcPluginOk [] []
, tcPluginStop = \_ -> tcPluginIO $ putStrLn ">>> Plugin Stop"
}
}
```
### Minimal example (with type error)
`Main.hs`:
```hs
{-# OPTIONS_GHC -fplugin MyPlugin #-}
module Main where
main :: (Monad m) => m ()
main = do
return 1
```
Compiling this will lead to the following output:
```
$ ~/ghc/inplace/bin/ghc-stage2 --make -package ghc-7.11.20150209 -dynamic Main.hs
[2 of 2] Compiling Main ( Main.hs, Main.o )
>>> Plugin Init
>>> Plugin Solve
>>> Plugin Solve
>>> Plugin Solve
Main.hs:6:10:
Could not deduce (Num ()) arising from the literal ‘1’
from the context: Monad m
bound by the type signature for: main :: Monad m => m ()
at Main.hs:4:9-25
In the first argument of ‘return’, namely ‘1’
In a stmt of a 'do' block: return 1
In the expression: do { return 1 }
```
Which means `tcPluginStop` was _not_ called.
### Minimal example (without type error)
`Main.hs`:
```hs
{-# OPTIONS_GHC -fplugin MyPlugin #-}
module Main where
main :: (Monad m) => m ()
main = do
return ()
```
Compiling this will lead to the following output:
```
$ ~/ghc/inplace/bin/ghc-stage2 --make -package ghc-7.11.20150209 -dynamic Main.hs
[2 of 2] Compiling Main ( Main.hs, Main.o ) [MyPlugin changed]
>>> Plugin Init
>>> Plugin Solve
>>> Plugin Solve
>>> Plugin Stop
Linking Main ...
```
Which means `tcPluginStop` _was_ called.
### Possible solution
As far as I can see, the solution to this should be to change the plugin code at the bottom of `typechecker/TcRnDriver.hs` from
```hs
withTcPlugins :: HscEnv -> TcM a -> TcM a
withTcPlugins hsc_env m =
do plugins <- liftIO (loadTcPlugins hsc_env)
case plugins of
[] -> m -- Common fast case
_ -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins
res <- updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m
mapM_ runTcPluginM stops
return res
where
startPlugin (TcPlugin start solve stop) =
do s <- runTcPluginM start
return (solve s, stop s)
```
to
```hs
withTcPlugins :: HscEnv -> TcM a -> TcM a
withTcPlugins hsc_env m =
do plugins <- liftIO (loadTcPlugins hsc_env)
case plugins of
[] -> m -- Common fast case
_ -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins
eitherRes <- tryM $ do updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m
mapM_ runTcPluginM stops
case eitherRes of
Left e -> failM
Right res -> return res
where
startPlugin (TcPlugin start solve stop) =
do s <- runTcPluginM start
return (solve s, stop s)
```
.
I have tried this. It compiles and my minimal example delivers the correct result.
Are there any arguments against this change? If not, I would try to commit a patch for this problem sometime this weekend.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | adamgundry |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"tcPluginStop of a type checker plugin is not called if an error occurs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["adamgundry"],"type":"Bug","description":"When a module using a type checker plugin produces a compiler error the clean up function `tcPluginStop` of the plugin is not called.\r\n\r\nI am not sure if this is intended, but according to the description of the wiki page (Plugins/TypeChecker) this should always be called.\r\n\r\n=== Test plugin\r\n\r\n`MyPlugin.hs`:\r\n{{{#!hs\r\nmodule MyPlugin\r\n ( plugin ) where\r\n\r\nimport Plugins\r\nimport TcRnTypes\r\nimport TcPluginM\r\n\r\nplugin :: Plugin\r\nplugin = defaultPlugin \r\n { tcPlugin = \\clos -> Just $ TcPlugin \r\n { tcPluginInit = tcPluginIO $ putStrLn \">>> Plugin Init\"\r\n , tcPluginSolve = \\_ _ _ _ -> do\r\n tcPluginIO $ putStrLn \">>> Plugin Solve\"\r\n return $ TcPluginOk [] []\r\n , tcPluginStop = \\_ -> tcPluginIO $ putStrLn \">>> Plugin Stop\"\r\n }\r\n }\r\n}}}\r\n\r\n=== Minimal example (with type error)\r\n\r\n`Main.hs`:\r\n{{{#!hs\r\n{-# OPTIONS_GHC -fplugin MyPlugin #-}\r\nmodule Main where\r\n\r\nmain :: (Monad m) => m ()\r\nmain = do\r\n return 1\r\n}}}\r\n\r\nCompiling this will lead to the following output:\r\n{{{\r\n$ ~/ghc/inplace/bin/ghc-stage2 --make -package ghc-7.11.20150209 -dynamic Main.hs\r\n[2 of 2] Compiling Main ( Main.hs, Main.o )\r\n>>> Plugin Init\r\n>>> Plugin Solve\r\n>>> Plugin Solve\r\n>>> Plugin Solve\r\n\r\nMain.hs:6:10:\r\n Could not deduce (Num ()) arising from the literal ‘1’\r\n from the context: Monad m\r\n bound by the type signature for: main :: Monad m => m ()\r\n at Main.hs:4:9-25\r\n In the first argument of ‘return’, namely ‘1’\r\n In a stmt of a 'do' block: return 1\r\n In the expression: do { return 1 }\r\n}}}\r\nWhich means `tcPluginStop` was _not_ called.\r\n\r\n=== Minimal example (without type error)\r\n\r\n`Main.hs`:\r\n{{{#!hs\r\n{-# OPTIONS_GHC -fplugin MyPlugin #-}\r\nmodule Main where\r\n\r\nmain :: (Monad m) => m ()\r\nmain = do\r\n return ()\r\n}}}\r\n\r\nCompiling this will lead to the following output:\r\n{{{\r\n$ ~/ghc/inplace/bin/ghc-stage2 --make -package ghc-7.11.20150209 -dynamic Main.hs\r\n[2 of 2] Compiling Main ( Main.hs, Main.o ) [MyPlugin changed]\r\n>>> Plugin Init\r\n>>> Plugin Solve\r\n>>> Plugin Solve\r\n>>> Plugin Stop\r\nLinking Main ...\r\n}}}\r\nWhich means `tcPluginStop` _was_ called.\r\n\r\n=== Possible solution\r\n\r\nAs far as I can see, the solution to this should be to change the plugin code at the bottom of `typechecker/TcRnDriver.hs` from\r\n{{{#!hs\r\nwithTcPlugins :: HscEnv -> TcM a -> TcM a\r\nwithTcPlugins hsc_env m =\r\n do plugins <- liftIO (loadTcPlugins hsc_env)\r\n case plugins of\r\n [] -> m -- Common fast case\r\n _ -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins\r\n res <- updGblEnv (\\e -> e { tcg_tc_plugins = solvers }) m\r\n mapM_ runTcPluginM stops\r\n return res\r\n where\r\n startPlugin (TcPlugin start solve stop) =\r\n do s <- runTcPluginM start\r\n return (solve s, stop s)\r\n}}}\r\nto\r\n{{{#!hs\r\nwithTcPlugins :: HscEnv -> TcM a -> TcM a\r\nwithTcPlugins hsc_env m =\r\n do plugins <- liftIO (loadTcPlugins hsc_env)\r\n case plugins of\r\n [] -> m -- Common fast case\r\n _ -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins\r\n eitherRes <- tryM $ do updGblEnv (\\e -> e { tcg_tc_plugins = solvers }) m\r\n mapM_ runTcPluginM stops\r\n case eitherRes of\r\n Left e -> failM\r\n Right res -> return res\r\n where\r\n startPlugin (TcPlugin start solve stop) =\r\n do s <- runTcPluginM start\r\n return (solve s, stop s)\r\n}}}\r\n.\r\n\r\nI have tried this. It compiles and my minimal example delivers the correct result.\r\n\r\nAre there any arguments against this change? If not, I would try to commit a patch for this problem sometime this weekend.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1jbrackerjbrackerhttps://gitlab.haskell.org/ghc/ghc/-/issues/10072Panic: generalised wildcards in RULES2019-07-07T18:37:40ZthomaswPanic: generalised wildcards in RULESGeneralised wildcards (PartialTypeSignatures) in the binder type annotation of a RULE cause panics.
Minimal example:
```hs
module WildcardInRuleBndrSig where
{-# RULES
"map/empty" forall (f :: a -> _). map f [] = []
#-}
```
Output:
...Generalised wildcards (PartialTypeSignatures) in the binder type annotation of a RULE cause panics.
Minimal example:
```hs
module WildcardInRuleBndrSig where
{-# RULES
"map/empty" forall (f :: a -> _). map f [] = []
#-}
```
Output:
```
WildcardInRuleBndrSig.hs:3:31:ghc-stage1: panic! (the 'impossible' happened)
(GHC version 7.11.20150209 for x86_64-unknown-linux):
No skolem info: w__alY[sk]
```
When a wildcard is generalised over, the error message reporting the inferred type gives some extra info about the type variables occurring in the inferred type. This extra information is retrieved by looking up the skolem information (`getSkolemInfo`) for the type variables in the enclosing implications (`cec_encl`). The problem is that there are no enclosing implications in this case, hence the panic.
Note that with the flags `-XPartialTypeSignatures` and `-fno-warn-partial-type-signatures` enabled, there is no panic, as no error/warning message is constructed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1-rc2 |
| Type | Bug |
| 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":"Panic: generalised wildcards in RULES","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"thomasw"},"version":"7.10.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Generalised wildcards (PartialTypeSignatures) in the binder type annotation of a RULE cause panics.\r\n\r\nMinimal example:\r\n{{{#!hs\r\nmodule WildcardInRuleBndrSig where\r\n{-# RULES\r\n\"map/empty\" forall (f :: a -> _). map f [] = []\r\n #-}\r\n}}}\r\n\r\nOutput:\r\n{{{\r\nWildcardInRuleBndrSig.hs:3:31:ghc-stage1: panic! (the 'impossible' happened)\r\n (GHC version 7.11.20150209 for x86_64-unknown-linux):\r\n\tNo skolem info: w__alY[sk]\r\n}}}\r\n\r\n\r\nWhen a wildcard is generalised over, the error message reporting the inferred type gives some extra info about the type variables occurring in the inferred type. This extra information is retrieved by looking up the skolem information (`getSkolemInfo`) for the type variables in the enclosing implications (`cec_encl`). The problem is that there are no enclosing implications in this case, hence the panic.\r\n\r\nNote that with the flags `-XPartialTypeSignatures` and `-fno-warn-partial-type-signatures` enabled, there is no panic, as no error/warning message is constructed.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1thomaswthomaswhttps://gitlab.haskell.org/ghc/ghc/-/issues/9953Pattern synonyms don't work with GADTs2019-07-07T18:38:14ZSimon Peyton JonesPattern synonyms don't work with GADTsConsider this variant of test `T8968-1`:
```
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where
data X :: * -> * where
Y :: a -> X (Maybe a)
pattern C :: a -> X (Maybe a)
pattern C x = Y x
foo :: X t...Consider this variant of test `T8968-1`:
```
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
module ShouldCompile where
data X :: * -> * where
Y :: a -> X (Maybe a)
pattern C :: a -> X (Maybe a)
pattern C x = Y x
foo :: X t -> t
foo (C x) = Just x
```
- If we had `(Y x)` instead of `(C x)` in the LHS of `foo`, then this is an ordinary GADT program and typechecks fine.
- If we omit the pattern signature, it typechecks fine, and `:info C` says
```
pattern C :: t ~ Maybe a => a -> X t -- Defined in ‘ShouldCompile’
```
- But as written, it fails with
```
Foo.hs:11:6:
Couldn't match type ‘t’ with ‘Maybe a0’
‘t’ is a rigid type variable bound by
the type signature for: foo :: X t -> t at Foo.hs:10:8
Expected type: X t
Actual type: X (Maybe a0)
Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)
In the pattern: C x
In an equation for ‘foo’: foo (C x) = Just x
```
> Moreover, `:info C` says
```
pattern C :: a -> X (Maybe a) -- Defined at Foo.hs:8:9
```
Do you see the difference? In the former, the "prov_theta" equality constraint is explicit, but in the latter it's implicit.
The exact thing happens for `DataCons`. It's handled via the `dcEqSpec` field. Essentially `PatSyn` should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in `TcTyClsDecls.rejigConRes` (perhaps needs a better name).
This is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.8.4 |
| 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":"Pattern synonyms don't work with GADTs","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this variant of test `T8968-1`:\r\n{{{\r\n{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}\r\nmodule ShouldCompile where\r\n\r\ndata X :: * -> * where\r\n Y :: a -> X (Maybe a)\r\n\r\npattern C :: a -> X (Maybe a)\r\npattern C x = Y x\r\n\r\nfoo :: X t -> t\r\nfoo (C x) = Just x\r\n}}}\r\n * If we had `(Y x)` instead of `(C x)` in the LHS of `foo`, then this is an ordinary GADT program and typechecks fine. \r\n\r\n * If we omit the pattern signature, it typechecks fine, and `:info C` says\r\n{{{\r\npattern C :: t ~ Maybe a => a -> X t \t-- Defined in ‘ShouldCompile’\r\n}}}\r\n\r\n * But as written, it fails with\r\n{{{\r\nFoo.hs:11:6:\r\n Couldn't match type ‘t’ with ‘Maybe a0’\r\n ‘t’ is a rigid type variable bound by\r\n the type signature for: foo :: X t -> t at Foo.hs:10:8\r\n Expected type: X t\r\n Actual type: X (Maybe a0)\r\n Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)\r\n In the pattern: C x\r\n In an equation for ‘foo’: foo (C x) = Just x\r\n}}}\r\n Moreover, `:info C` says\r\n{{{\r\npattern C :: a -> X (Maybe a) \t-- Defined at Foo.hs:8:9\r\n}}}\r\n\r\nDo you see the difference? In the former, the \"prov_theta\" equality constraint is explicit, but in the latter it's implicit.\r\n\r\nThe exact thing happens for `DataCons`. It's handled via the `dcEqSpec` field. Essentially `PatSyn` should have a new field for the implicit equality constraints. And, just as for data consructors, we need to generate the equality constraints, and the existentials that are needed, when we process the signature. Use the code in `TcTyClsDecls.rejigConRes` (perhaps needs a better name).\r\n\r\nThis is all pretty serious. Without fixing it, GADT-style pattern signatures are all but useless.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Gergő ÉrdiGergő Érdihttps://gitlab.haskell.org/ghc/ghc/-/issues/9922Partial type signatures + extensions panic2019-07-07T18:38:26ZKrzysztof GogolewskiPartial type signatures + extensions panicPartial type signatures combined with the following GHC extensions cause a panic:
```hs
class C a where default f :: _ -- DefaultSignatures
instance Num Bool where negate :: _ -- InstanceSigs
deriving instance _ ...Partial type signatures combined with the following GHC extensions cause a panic:
```hs
class C a where default f :: _ -- DefaultSignatures
instance Num Bool where negate :: _ -- InstanceSigs
deriving instance _ -- StandaloneDeriving
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.9 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | thomasw |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Partial type signatures + extensions panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.9","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["thomasw"],"type":"Bug","description":"Partial type signatures combined with the following GHC extensions cause a panic:\r\n\r\n{{{#!hs\r\nclass C a where default f :: _ -- DefaultSignatures\r\n\r\ninstance Num Bool where negate :: _ -- InstanceSigs\r\n\r\nderiving instance _ -- StandaloneDeriving\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1thomaswthomaswhttps://gitlab.haskell.org/ghc/ghc/-/issues/9889Pattern synonym does not work in top-level pattern bind2019-07-07T18:38:37ZRichard Eisenbergrae@richarde.devPattern synonym does not work in top-level pattern bindWhen I say
```
{-# LANGUAGE PatternSynonyms #-}
pattern Id x = x
Id x = True
```
I get
```
Not in scope: data constructor ‘Id’
```
This happens with both 7.8.3 and HEAD.When I say
```
{-# LANGUAGE PatternSynonyms #-}
pattern Id x = x
Id x = True
```
I get
```
Not in scope: data constructor ‘Id’
```
This happens with both 7.8.3 and HEAD.7.10.1Gergő ÉrdiGergő Érdihttps://gitlab.haskell.org/ghc/ghc/-/issues/9783Pattern synonym matcher is unnecessarily strict on unboxed continuations2019-07-07T18:39:03ZGergő ÉrdiPattern synonym matcher is unnecessarily strict on unboxed continuationsAs discovered while investigating #9732, if you have something like
```
{-# LANGUAGE PatternSynonyms, MagicHash #-}
import GHC.Base
pattern P = True
f :: Bool -> Int#
f P = 42#
```
`f` is compiled into
```
Main.f :: GHC.Types.Bool -...As discovered while investigating #9732, if you have something like
```
{-# LANGUAGE PatternSynonyms, MagicHash #-}
import GHC.Base
pattern P = True
f :: Bool -> Int#
f P = 42#
```
`f` is compiled into
```
Main.f :: GHC.Types.Bool -> GHC.Prim.Int#
[LclIdX, Str=DmdType]
Main.f =
letrec {
f_apU :: GHC.Types.Bool -> GHC.Prim.Int#
[LclId, Str=DmdType]
f_apU =
\ (ds_dq1 :: GHC.Types.Bool) ->
break<2>()
let {
fail_dq2 :: GHC.Prim.Void# -> GHC.Prim.Int#
[LclId, Str=DmdType]
fail_dq2 =
\ (ds_dq3 [OS=OneShot] :: GHC.Prim.Void#) ->
Control.Exception.Base.patError
@ GHC.Prim.Int# "unboxed.hs:7:1-9|function f"# } in
case fail_dq2 GHC.Prim.void# of wild_00 { __DEFAULT ->
(case break<1>() 42 of wild_00 { __DEFAULT ->
Main.$mP @ GHC.Prim.Int# ds_dq1 wild_00
})
wild_00
}; } in
f_apU
```
Note how `fail_dq2` is applied on `void#` _before_ the pattern match, meaning the following expression:
```
I# (f True)
```
will fail with
```
*** Exception: unboxed.hs:7:1-9: Non-exhaustive patterns in function f
```
This is because the the type of `P`'s matcher, instantiated for its use in `f`, is
```
$mP :: Bool -> Int# -> Int# -> Int#
```
so of course it is strict both on the success and the failure continuation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | Bug |
| 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":"Pattern synonym matcher is unnecessarily strict on unboxed continuations","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":"Bug","description":"As discovered while investigating #9732, if you have something like\r\n\r\n{{{\r\n{-# LANGUAGE PatternSynonyms, MagicHash #-}\r\nimport GHC.Base\r\n\r\npattern P = True\r\n\r\nf :: Bool -> Int#\r\nf P = 42#\r\n}}}\r\n\r\n`f` is compiled into\r\n\r\n{{{\r\nMain.f :: GHC.Types.Bool -> GHC.Prim.Int#\r\n[LclIdX, Str=DmdType]\r\nMain.f =\r\n letrec {\r\n f_apU :: GHC.Types.Bool -> GHC.Prim.Int#\r\n [LclId, Str=DmdType]\r\n f_apU =\r\n \\ (ds_dq1 :: GHC.Types.Bool) ->\r\n break<2>()\r\n let {\r\n fail_dq2 :: GHC.Prim.Void# -> GHC.Prim.Int#\r\n [LclId, Str=DmdType]\r\n fail_dq2 =\r\n \\ (ds_dq3 [OS=OneShot] :: GHC.Prim.Void#) ->\r\n Control.Exception.Base.patError\r\n @ GHC.Prim.Int# \"unboxed.hs:7:1-9|function f\"# } in\r\n case fail_dq2 GHC.Prim.void# of wild_00 { __DEFAULT ->\r\n (case break<1>() 42 of wild_00 { __DEFAULT ->\r\n Main.$mP @ GHC.Prim.Int# ds_dq1 wild_00\r\n })\r\n wild_00\r\n }; } in\r\n f_apU\r\n}}}\r\n\r\nNote how `fail_dq2` is applied on `void#` _before_ the pattern match, meaning the following expression:\r\n\r\n{{{\r\nI# (f True)\r\n}}}\r\n\r\nwill fail with\r\n\r\n{{{\r\n*** Exception: unboxed.hs:7:1-9: Non-exhaustive patterns in function f\r\n}}}\r\n\r\nThis is because the the type of `P`'s matcher, instantiated for its use in `f`, is\r\n\r\n{{{\r\n$mP :: Bool -> Int# -> Int# -> Int#\r\n}}}\r\n\r\nso of course it is strict both on the success and the failure continuation.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Gergő ÉrdiGergő Érdihttps://gitlab.haskell.org/ghc/ghc/-/issues/9739GHC 7.8 chokes on recursive classes2019-07-07T18:39:15ZbitonicGHC 7.8 chokes on recursive classesType checking this makes GHC 7.8.3 loop:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
module Foo where
class Class3 a => Class1 a where
class Class2 t a where
class2 :: (Class3 t) => a -> m
class (Class1 t, Class2 t t) => Class3 t ...Type checking this makes GHC 7.8.3 loop:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
module Foo where
class Class3 a => Class1 a where
class Class2 t a where
class2 :: (Class3 t) => a -> m
class (Class1 t, Class2 t t) => Class3 t where
```
Does not happen in 7.6.3.
I think it's something to do with the `Class3` constraint appearing in `class2`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | Bug |
| 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":"GHC 7.8 chokes on recursive classes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Type checking this makes GHC 7.8.3 loop:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\nmodule Foo where\r\n\r\nclass Class3 a => Class1 a where\r\n\r\nclass Class2 t a where\r\n class2 :: (Class3 t) => a -> m\r\n\r\nclass (Class1 t, Class2 t t) => Class3 t where\r\n}}}\r\n\r\nDoes not happen in 7.6.3.\r\n\r\nI think it's something to do with the `Class3` constraint appearing in `class2`.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/9605Misleading error message with forgotten "do"2019-07-07T18:39:51ZowstMisleading error message with forgotten "do"In the following (simplified) code, I forgot to add the do keyword, when doing some refactoring. This caused GHC to give a strange error message that said approximately
"The function F is applied to two arguments, but its type T has only...In the following (simplified) code, I forgot to add the do keyword, when doing some refactoring. This caused GHC to give a strange error message that said approximately
"The function F is applied to two arguments, but its type T has only two"... which is odd!
```hs
import Control.Monad.RWS ( evalRWS, RWS )
import Control.Monad.Writer.Class ( tell )
main = print $ evalRWS (go 1) () ()
go :: Int -> RWS () [String] () ()
go i = --Oops, forgot a do here
return (show i) >>= (\l -> tell [l])
-- go $ i + 1
go i
```
Strangely, replacing the "go i" line with the commented-out line above it gives a sensible error message, the "Possible cause: \`\\l -\> tell \[l\]' is applied to too many arguments" message, which is correct, and would've pointed me straight to the problem.
The invalid error message, which appears to be the same using GHC 7.6.3 and 7.8.3, is:
```
NFA.hs:8:25:
Couldn't match type ‘String
-> Control.Monad.Trans.RWS.Lazy.RWST
() [String] () Data.Functor.Identity.Identity ()’
with ‘()’
Expected type: Int
-> String
-> Control.Monad.Trans.RWS.Lazy.RWST
() [String] () Data.Functor.Identity.Identity ()
Actual type: Int -> ()
The function ‘\ l -> tell [l]’ is applied to two arguments,
but its type ‘(Int -> RWS () [String] () ()) -> Int -> ()’
has only two
In the second argument of ‘(>>=)’, namely ‘(\ l -> tell [l]) go i’
In the expression: return (show i) >>= (\ l -> tell [l]) go i
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.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":"Misleading error message with forgotten \"do\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the following (simplified) code, I forgot to add the do keyword, when doing some refactoring. This caused GHC to give a strange error message that said approximately\r\n\"The function F is applied to two arguments, but its type T has only two\"... which is odd!\r\n\r\n{{{#!hs\r\nimport Control.Monad.RWS ( evalRWS, RWS )\r\nimport Control.Monad.Writer.Class ( tell )\r\n\r\nmain = print $ evalRWS (go 1) () ()\r\n\r\ngo :: Int -> RWS () [String] () ()\r\ngo i = --Oops, forgot a do here\r\n return (show i) >>= (\\l -> tell [l])\r\n -- go $ i + 1\r\n go i\r\n}}}\r\n\r\nStrangely, replacing the \"go i\" line with the commented-out line above it gives a sensible error message, the \"Possible cause: `\\l -> tell [l]' is applied to too many arguments\" message, which is correct, and would've pointed me straight to the problem. \r\n\r\nThe invalid error message, which appears to be the same using GHC 7.6.3 and 7.8.3, is:\r\n\r\n{{{\r\nNFA.hs:8:25:\r\n Couldn't match type ‘String\r\n -> Control.Monad.Trans.RWS.Lazy.RWST\r\n () [String] () Data.Functor.Identity.Identity ()’\r\n with ‘()’\r\n Expected type: Int\r\n -> String\r\n -> Control.Monad.Trans.RWS.Lazy.RWST\r\n () [String] () Data.Functor.Identity.Identity ()\r\n Actual type: Int -> ()\r\n The function ‘\\ l -> tell [l]’ is applied to two arguments,\r\n but its type ‘(Int -> RWS () [String] () ()) -> Int -> ()’\r\n has only two\r\n In the second argument of ‘(>>=)’, namely ‘(\\ l -> tell [l]) go i’\r\n In the expression: return (show i) >>= (\\ l -> tell [l]) go i\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1YurasYurashttps://gitlab.haskell.org/ghc/ghc/-/issues/9582Associated Type Synonyms do not unfold in InstanceSigs2020-12-02T21:56:59Zandreas.abelAssociated Type Synonyms do not unfold in InstanceSigs```hs
{-# LANGUAGE InstanceSigs, TypeFamilies #-}
class C a where
type T a
m :: T a
instance C Int where
type T Int = String
m :: String
m = "bla"
-- Method signature does not match class; it should be m :: T Int
-- In th...```hs
{-# LANGUAGE InstanceSigs, TypeFamilies #-}
class C a where
type T a
m :: T a
instance C Int where
type T Int = String
m :: String
m = "bla"
-- Method signature does not match class; it should be m :: T Int
-- In the instance declaration for ‘C Int’
```
As `T Int` is a synonym of `String`, `m :: String` should be a valid type signature alternative to `m :: T Int`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | Bug |
| 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":"Associated Type Synonyms do not unfold in InstanceSigs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":["InstanceSigs","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# LANGUAGE InstanceSigs, TypeFamilies #-}\r\n\r\nclass C a where\r\n type T a\r\n m :: T a\r\n\r\ninstance C Int where\r\n type T Int = String\r\n m :: String\r\n m = \"bla\"\r\n\r\n-- Method signature does not match class; it should be m :: T Int\r\n-- In the instance declaration for ‘C Int’\r\n}}}\r\n\r\nAs {{{T Int}}} is a synonym of {{{String}}}, {{{m :: String}}} should be a valid type signature alternative to {{{m :: T Int}}}","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/9323Confusing type error behaviour2019-07-07T18:40:53ZSimon Peyton JonesConfusing type error behaviourCompile this example with GHC 7.8.3.
```
module Foo where
broken :: [Int]
broken = ()
ambiguous :: a -> String
ambiguous _ = show 0
```
You get
```
Foo.hs:4:10:
Couldn't match expected type ‘[Int]’ with actual type ‘()’
In t...Compile this example with GHC 7.8.3.
```
module Foo where
broken :: [Int]
broken = ()
ambiguous :: a -> String
ambiguous _ = show 0
```
You get
```
Foo.hs:4:10:
Couldn't match expected type ‘[Int]’ with actual type ‘()’
In the expression: ()
In an equation for ‘broken’: broken = ()
Foo.hs:7:15:
No instance for (Show a0) arising from a use of ‘show’
The type variable ‘a0’ is ambiguous
```
(and a similar ambiguous `(Num a0)` error).
**But if you comment out `broken`, the program compiles**, using the defaulting rules to choose `a0` = `Integer`.
This is obviously wrong.
Reported by Evan Laforge.7.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/9201GHC unexpectedly refines explicit kind signatures2019-07-07T18:41:24ZEdward KmettGHC unexpectedly refines explicit kind signaturesThe following program should be rejected by the type checker:
```
{-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses #-}
class MonoidalCCC (f :: x -> y) (d :: y -> y -> *) | f -> d where
ret :: d a (f a)
```
Inste...The following program should be rejected by the type checker:
```
{-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses #-}
class MonoidalCCC (f :: x -> y) (d :: y -> y -> *) | f -> d where
ret :: d a (f a)
```
Instead it is accepted, but the kind variables specified above are 'corrected' during typechecking to:
```
>>> :browse
class MonoidalCCC (f :: x -> x) (d :: x -> x -> *) | f -> d where
ret :: d a (f a)
```
This may be similar in root cause to issue #9200, but there a valid program is rejected, and here an invalid program is accepted, so the fixes may be quite different.
It seems these kind variables are just being allowed to unify rather than being checked for subsumption.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | ekmett |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC unexpectedly refines explicit kind signatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["ekmett"],"type":"Bug","description":"The following program should be rejected by the type checker:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses #-}\r\n\r\nclass MonoidalCCC (f :: x -> y) (d :: y -> y -> *) | f -> d where\r\n ret :: d a (f a)\r\n}}}\r\n\r\nInstead it is accepted, but the kind variables specified above are 'corrected' during typechecking to:\r\n\r\n{{{\r\n>>> :browse\r\nclass MonoidalCCC (f :: x -> x) (d :: x -> x -> *) | f -> d where\r\n ret :: d a (f a)\r\n}}}\r\n\r\nThis may be similar in root cause to issue #9200, but there a valid program is rejected, and here an invalid program is accepted, so the fixes may be quite different.\r\n\r\nIt seems these kind variables are just being allowed to unify rather than being checked for subsumption.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/9200Milner-Mycroft failure at the kind level2019-07-07T18:41:24ZEdward KmettMilner-Mycroft failure at the kind levelThis is a reduction of a problem that occurs in real code.
```
{-# LANGUAGE PolyKinds #-}
class D a => C (f :: k) a
class C () a => D a
```
Typechecking complains:
```
The first argument of ‘C’ should have kind ‘k’,
but ‘()’...This is a reduction of a problem that occurs in real code.
```
{-# LANGUAGE PolyKinds #-}
class D a => C (f :: k) a
class C () a => D a
```
Typechecking complains:
```
The first argument of ‘C’ should have kind ‘k’,
but ‘()’ has kind ‘*’
In the class declaration for ‘D’
```
This program should be accepted, but we're not generalizing enough.
A slightly less reduced version of the problem arises in practice in:
```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
import Control.Category
class (Category c, Category d, Category e) => Profunctor
(p :: x -> y -> z)
(c :: x -> x -> *)
(d :: y -> y -> *)
(e :: z -> z -> *)
| p -> c d e
-- lens-style isomorphism families in an arbitrary category
type Iso (c :: i -> i -> *) (s :: i) (a :: i) = forall (p :: i -> i -> *).
Profunctor p c c (->) => p a a -> p s s
class Category e => Cartesian (e :: z -> z -> *) where
type P e :: z -> z -> z
associate :: Iso e (P e (P e a b) c) (P e a (P e b c))
```
This typechecks, but if I replace the line
```
class (Category c, Category d, Category e) => Profunctor
```
with
```
class (Category c, Category d, Cartesian e) => Profunctor
```
to say that you can only enrich a category over a monoidal category (using `Cartesian` in the approximation here), then it fails because a more baroque version of the same kind of cycle as the minimal example above as Profunctor references Cartesian which references an Iso which mentions a Profunctor.
I'm supplying explicit kind variables in the signature of the class, so we should be able to use those like we do with function signatures a universe down. =/
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | ekmett |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Milner-Mycroft failure at the kind level","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["ekmett"],"type":"Bug","description":"This is a reduction of a problem that occurs in real code.\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds #-}\r\nclass D a => C (f :: k) a\r\nclass C () a => D a\r\n}}}\r\n\r\nTypechecking complains:\r\n\r\n{{{\r\n The first argument of ‘C’ should have kind ‘k’,\r\n but ‘()’ has kind ‘*’\r\n In the class declaration for ‘D’\r\n}}}\r\n\r\nThis program should be accepted, but we're not generalizing enough.\r\n\r\nA slightly less reduced version of the problem arises in practice in:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n\r\nimport Control.Category\r\n\r\nclass (Category c, Category d, Category e) => Profunctor\r\n (p :: x -> y -> z)\r\n (c :: x -> x -> *)\r\n (d :: y -> y -> *)\r\n (e :: z -> z -> *)\r\n | p -> c d e\r\n\r\n-- lens-style isomorphism families in an arbitrary category\r\ntype Iso (c :: i -> i -> *) (s :: i) (a :: i) = forall (p :: i -> i -> *). \r\n Profunctor p c c (->) => p a a -> p s s\r\n\r\nclass Category e => Cartesian (e :: z -> z -> *) where\r\n type P e :: z -> z -> z\r\n associate :: Iso e (P e (P e a b) c) (P e a (P e b c))\r\n}}}\r\n\r\nThis typechecks, but if I replace the line\r\n\r\n{{{\r\nclass (Category c, Category d, Category e) => Profunctor\r\n}}}\r\n\r\nwith \r\n\r\n{{{\r\nclass (Category c, Category d, Cartesian e) => Profunctor\r\n}}}\r\n\r\nto say that you can only enrich a category over a monoidal category (using `Cartesian` in the approximation here), then it fails because a more baroque version of the same kind of cycle as the minimal example above as Profunctor references Cartesian which references an Iso which mentions a Profunctor.\r\n\r\nI'm supplying explicit kind variables in the signature of the class, so we should be able to use those like we do with function signatures a universe down. =/","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/8968Pattern synonyms and GADTs2019-07-07T18:42:30ZAndres LöhPattern synonyms and GADTsI think this one is different from #8966, but feel free to close one as duplicate if it turns out to be the same problem.
The following program (using GADTs and pattern synonyms, but not kind polymorphism or data kinds) fails to check w...I think this one is different from #8966, but feel free to close one as duplicate if it turns out to be the same problem.
The following program (using GADTs and pattern synonyms, but not kind polymorphism or data kinds) fails to check with ghc-7.8.1-rc2, but I think it should:
```
{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
data X :: (* -> *) -> * -> * where
Y :: f Int -> X f Int
pattern C x = Y (Just x)
```
The error I get is the following:
```
PatKind.hs:6:18:
Couldn't match type ‘t’ with ‘Maybe’
‘t’ is untouchable
inside the constraints (t1 ~ Int)
bound by a pattern with constructor
Y :: forall (f :: * -> *). f Int -> X f Int,
in a pattern synonym declaration
at PatKind.hs:6:15-24
‘t’ is a rigid type variable bound by
the inferred type of
C :: X t t1
x :: Int
at PatKind.hs:1:1
Expected type: t Int
Actual type: Maybe Int
In the pattern: Just x
In the pattern: Y (Just x)
PatKind.hs:6:18:
Could not deduce (t ~ Maybe)
from the context (t1 ~ Int)
bound by the type signature for
(Main.$WC) :: t1 ~ Int => Int -> X t t1
at PatKind.hs:6:9
‘t’ is a rigid type variable bound by
the type signature for (Main.$WC) :: t1 ~ Int => Int -> X t t1
at PatKind.hs:1:1
Expected type: t Int
Actual type: Maybe Int
Relevant bindings include
($WC) :: Int -> X t t1 (bound at PatKind.hs:6:9)
In the first argument of ‘Y’, namely ‘(Just x)’
In the expression: Y (Just x)
```
Note that I'd be perfectly happy to provide a type signature for the pattern synonym, but I don't know of any syntax I could use. The Wiki page at https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms mentions I might be able to write
```
pattern C :: Int -> X Maybe Int
```
but this triggers a parse error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.1-rc2 |
| Type | Bug |
| 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":"Pattern synonyms and GADTs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I think this one is different from #8966, but feel free to close one as duplicate if it turns out to be the same problem.\r\n\r\nThe following program (using GADTs and pattern synonyms, but not kind polymorphism or data kinds) fails to check with ghc-7.8.1-rc2, but I think it should:\r\n{{{\r\n{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}\r\n\r\ndata X :: (* -> *) -> * -> * where\r\n Y :: f Int -> X f Int\r\n\r\npattern C x = Y (Just x)\r\n}}}\r\nThe error I get is the following:\r\n{{{\r\nPatKind.hs:6:18:\r\n Couldn't match type ‘t’ with ‘Maybe’\r\n ‘t’ is untouchable\r\n inside the constraints (t1 ~ Int)\r\n bound by a pattern with constructor\r\n Y :: forall (f :: * -> *). f Int -> X f Int,\r\n in a pattern synonym declaration\r\n at PatKind.hs:6:15-24\r\n ‘t’ is a rigid type variable bound by\r\n the inferred type of\r\n C :: X t t1\r\n x :: Int\r\n at PatKind.hs:1:1\r\n Expected type: t Int\r\n Actual type: Maybe Int\r\n In the pattern: Just x\r\n In the pattern: Y (Just x)\r\n\r\nPatKind.hs:6:18:\r\n Could not deduce (t ~ Maybe)\r\n from the context (t1 ~ Int)\r\n bound by the type signature for\r\n (Main.$WC) :: t1 ~ Int => Int -> X t t1\r\n at PatKind.hs:6:9\r\n ‘t’ is a rigid type variable bound by\r\n the type signature for (Main.$WC) :: t1 ~ Int => Int -> X t t1\r\n at PatKind.hs:1:1\r\n Expected type: t Int\r\n Actual type: Maybe Int\r\n Relevant bindings include\r\n ($WC) :: Int -> X t t1 (bound at PatKind.hs:6:9)\r\n In the first argument of ‘Y’, namely ‘(Just x)’\r\n In the expression: Y (Just x)\r\n}}}\r\n\r\nNote that I'd be perfectly happy to provide a type signature for the pattern synonym, but I don't know of any syntax I could use. The Wiki page at https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms mentions I might be able to write\r\n{{{\r\npattern C :: Int -> X Maybe Int\r\n}}}\r\nbut this triggers a parse error.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Gergő ÉrdiGergő Érdihttps://gitlab.haskell.org/ghc/ghc/-/issues/8778Typeable TypeNats2019-07-07T18:43:30ZdmccleanTypeable TypeNatsIt would be useful (the case I have at hand is for some scenarios involving checking of physical dimensions) to be able to combine the Data.Dynamic story with the GHC.TypeLits story.
A Typeable instance for every Nat is the sticking poi...It would be useful (the case I have at hand is for some scenarios involving checking of physical dimensions) to be able to combine the Data.Dynamic story with the GHC.TypeLits story.
A Typeable instance for every Nat is the sticking point.
(I do not know if this is even theoretically possible.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.1-rc1 |
| 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":"Typeable TypeNats","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"⊥","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It would be useful (the case I have at hand is for some scenarios involving checking of physical dimensions) to be able to combine the Data.Dynamic story with the GHC.TypeLits story.\r\n\r\nA Typeable instance for every Nat is the sticking point.\r\n\r\n(I do not know if this is even theoretically possible.)","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/8584Pattern synonym type signatures2019-07-07T18:44:22ZGergő ÉrdiPattern synonym type signaturesCurrently, the only way to specify a type signature for a pattern synonym is by adding type annotations to the right-hand side, like this:
```
{-# LANGUAGE PatternSynonyms, ScopedTypeVariables #-}
pattern Single x = ([x] :: [Int])
```
...Currently, the only way to specify a type signature for a pattern synonym is by adding type annotations to the right-hand side, like this:
```
{-# LANGUAGE PatternSynonyms, ScopedTypeVariables #-}
pattern Single x = ([x] :: [Int])
```
Bespoke syntax for adding type signatures for pattern synonyms would probably be useful.
Link to [PatternSynonyms](pattern-synonyms) for pattern synonym signatures for specification.7.10.1Gergő ÉrdiGergő Érdihttps://gitlab.haskell.org/ghc/ghc/-/issues/8044"Inaccessible code" error reported in wrong place2020-08-14T09:52:35ZRichard Eisenbergrae@richarde.dev"Inaccessible code" error reported in wrong placeHere is my file `Bug.hs`:
```
{-# LANGUAGE GADTs, TypeFamilies #-}
module Bug where
data X a where
XInt :: X Int
XBool :: X Bool
XChar :: X Char
type family Frob a where
Frob Int = Int
Frob x = Char
frob :: X a -> X (Fro...Here is my file `Bug.hs`:
```
{-# LANGUAGE GADTs, TypeFamilies #-}
module Bug where
data X a where
XInt :: X Int
XBool :: X Bool
XChar :: X Char
type family Frob a where
Frob Int = Int
Frob x = Char
frob :: X a -> X (Frob a)
frob XInt = XInt
frob _ = XChar
```
Compiling this file produces the error
```
Bug.hs:15:6:
Couldn't match type ‛Int’ with ‛Char’
Inaccessible code in
a pattern with constructor XInt :: X Int, in an equation for ‛frob’
In the pattern: XInt
In an equation for ‛frob’: frob XInt = XInt
```
The line/column number single out the pattern `XInt` in the first clause of the function `frob`. But, the real problem (as I see it), is the right-hand side of the *second* clause of `frob`. Indeed, when I comment out the second line of the function, the error goes away, even though it was reported on the first line.
I do not believe that this error is caused by closed type families, per se, because I have run across it without them, just in code that was too hard to pare down enough to make a bug report out of.
This was tested on 7.7.20130702.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| Type | Bug |
| 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":"\"Inaccessible code\" error reported in wrong place","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is my file `Bug.hs`:\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, TypeFamilies #-}\r\n\r\nmodule Bug where\r\n\r\ndata X a where\r\n XInt :: X Int\r\n XBool :: X Bool\r\n XChar :: X Char\r\n\r\ntype family Frob a where\r\n Frob Int = Int\r\n Frob x = Char\r\n\r\nfrob :: X a -> X (Frob a)\r\nfrob XInt = XInt\r\nfrob _ = XChar\r\n}}}\r\n\r\nCompiling this file produces the error\r\n\r\n{{{\r\nBug.hs:15:6:\r\n Couldn't match type ‛Int’ with ‛Char’\r\n Inaccessible code in\r\n a pattern with constructor XInt :: X Int, in an equation for ‛frob’\r\n In the pattern: XInt\r\n In an equation for ‛frob’: frob XInt = XInt\r\n}}}\r\n\r\nThe line/column number single out the pattern `XInt` in the first clause of the function `frob`. But, the real problem (as I see it), is the right-hand side of the ''second'' clause of `frob`. Indeed, when I comment out the second line of the function, the error goes away, even though it was reported on the first line.\r\n\r\nI do not believe that this error is caused by closed type families, per se, because I have run across it without them, just in code that was too hard to pare down enough to make a bug report out of.\r\n\r\nThis was tested on 7.7.20130702.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/7730:info and polykinds2019-07-07T18:48:23ZKrzysztof Gogolewski:info and polykinds```
ghci -XPolyKinds
Prelude> data A x y
Prelude> :i A
data A k k x y -- Defined at <interactive>:3:6
```
The two `k` might be different. It should be either `A k l x y` or - without kind variables - `A x y`.
<details><summary>Trac m...```
ghci -XPolyKinds
Prelude> data A x y
Prelude> :i A
data A k k x y -- Defined at <interactive>:3:6
```
The two `k` might be different. It should be either `A k l x y` or - without kind variables - `A x y`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.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":":info and polykinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\nghci -XPolyKinds\r\n\r\nPrelude> data A x y\r\nPrelude> :i A\r\ndata A k k x y \t-- Defined at <interactive>:3:6\r\n}}}\r\n\r\nThe two `k` might be different. It should be either {{{A k l x y}}} or - without kind variables - {{{A x y}}}.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1archblobarchblobhttps://gitlab.haskell.org/ghc/ghc/-/issues/7643Kind application error2019-07-07T18:48:52ZgmainlandKind application errorCompiling the attached program with -dcore-lint fails. This failure is a reduced version of code taken from the primitive package, version 0.5.0.1.
To see the failure:
```
ghc -dcore-lint --make Main.hs
```
The failure does not occur ...Compiling the attached program with -dcore-lint fails. This failure is a reduced version of code taken from the primitive package, version 0.5.0.1.
To see the failure:
```
ghc -dcore-lint --make Main.hs
```
The failure does not occur with GHC 7.4.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.6.1 |
| Type | Bug |
| 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":"Kind application error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling the attached program with -dcore-lint fails. This failure is a reduced version of code taken from the primitive package, version 0.5.0.1.\r\n\r\nTo see the failure:\r\n\r\n{{{\r\nghc -dcore-lint --make Main.hs\r\n}}}\r\n\r\nThe failure does not occur with GHC 7.4.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1Simon Peyton JonesSimon Peyton Jones