GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:59:12Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/4395T1735(ghci) failing with core-lint error2019-07-07T18:59:12ZSimon MarlowT1735(ghci) failing with core-lint errorexcerpt from the error message:
```
GHCi, version 7.1.20101013: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ....excerpt from the error message:
```
GHCi, version 7.1.20101013: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
[1 of 6] Compiling T1735_Help.Context ( T1735_Help/Context.hs, interpreted )
[2 of 6] Compiling T1735_Help.State ( T1735_Help/State.hs, interpreted )
[3 of 6] Compiling T1735_Help.Basics ( T1735_Help/Basics.hs, interpreted )
[4 of 6] Compiling T1735_Help.Instances ( T1735_Help/Instances.hs, interpreted )
[5 of 6] Compiling T1735_Help.Xml ( T1735_Help/Xml.hs, interpreted )
*** Core Lint errors : in result of Tidy Core ***
{-# LINE 122 "T1735_Help/Xml.hs #-}:
[RHS of T1735_Help.Xml.typeNotValue :: forall a_a1NJ.
T1735_Help.Xml.Xml a_a1NJ =>
a_a1NJ -> a_a1NJ]
Demand type has 2 arguments, rhs has 1 arguments, T1735_Help.Xml.typeNotValue
Binder's strictness signature: DmdType TTb
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"T1735(ghci) failing with core-lint error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"excerpt from the error message:\r\n\r\n{{{\r\nGHCi, version 7.1.20101013: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\nLoading package ffi-1.0 ... linking ... done.\r\n[1 of 6] Compiling T1735_Help.Context ( T1735_Help/Context.hs, interpreted )\r\n[2 of 6] Compiling T1735_Help.State ( T1735_Help/State.hs, interpreted )\r\n[3 of 6] Compiling T1735_Help.Basics ( T1735_Help/Basics.hs, interpreted )\r\n[4 of 6] Compiling T1735_Help.Instances ( T1735_Help/Instances.hs, interpreted )\r\n[5 of 6] Compiling T1735_Help.Xml ( T1735_Help/Xml.hs, interpreted )\r\n*** Core Lint errors : in result of Tidy Core ***\r\n{-# LINE 122 \"T1735_Help/Xml.hs #-}:\r\n [RHS of T1735_Help.Xml.typeNotValue :: forall a_a1NJ.\r\n T1735_Help.Xml.Xml a_a1NJ =>\r\n a_a1NJ -> a_a1NJ]\r\n Demand type has 2 arguments, rhs has 1 arguments, T1735_Help.Xml.typeNotValue\r\n Binder's strictness signature: DmdType TTb\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.0.1Ian Lynagh <igloo@earth.li>Ian Lynagh <igloo@earth.li>https://gitlab.haskell.org/ghc/ghc/-/issues/4394IPRun failure2021-11-02T09:27:32ZSimon MarlowIPRun failuretypecheck/should_run/IPRun is currently failing all ways:
```
=====> IPRun(normal) 1973 of 2622 [0, 24, 0]
cd ./typecheck/should_run && '/64playpen/simonmar/nightly/HEAD-cam-04-unx/x86_64-unknown-linux/inplace/bin/ghc-stage2' -fforce-re...typecheck/should_run/IPRun is currently failing all ways:
```
=====> IPRun(normal) 1973 of 2622 [0, 24, 0]
cd ./typecheck/should_run && '/64playpen/simonmar/nightly/HEAD-cam-04-unx/x86_64-unknown-linux/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-conf -rtsopts -o IPRun IPRun.hs >IPRun.comp.stderr 2>&1
Compile failed (status 256) errors were:
[1 of 1] Compiling Main ( IPRun.hs, IPRun.o )
IPRun.hs:13:18:
Ambiguous type variable `a' in the constraint:
(Num a) arising from the literal `5'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: 5
In the expression: let ?x = 5 in \ () -> ?x
In an equation for `f2': f2 () = let ?x = 5 in \ () -> ?x
IPRun.hs:24:13:
Ambiguous type variable `a1' in the constraint:
(Show a1) arising from a use of `print'
Probable fix: add a type signature that fixes these type variable(s)
In a stmt of a 'do' expression: print (f2 () ())
In the expression:
do { print (f0 ());
print (f1 ());
print (f2 () ());
print (f3 ()) }
In the expression:
let ?x = 0
in
do { print (f0 ());
print (f1 ());
print (f2 () ());
.... }
*** unexpected failure for IPRun(normal)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"IPRun failure","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"typecheck/should_run/IPRun is currently failing all ways:\r\n\r\n{{{\r\n=====> IPRun(normal) 1973 of 2622 [0, 24, 0]\r\ncd ./typecheck/should_run && '/64playpen/simonmar/nightly/HEAD-cam-04-unx/x86_64-unknown-linux/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-conf -rtsopts -o IPRun IPRun.hs >IPRun.comp.stderr 2>&1\r\nCompile failed (status 256) errors were:\r\n[1 of 1] Compiling Main ( IPRun.hs, IPRun.o )\r\n\r\nIPRun.hs:13:18:\r\n Ambiguous type variable `a' in the constraint:\r\n (Num a) arising from the literal `5'\r\n Probable fix: add a type signature that fixes these type variable(s)\r\n In the expression: 5\r\n In the expression: let ?x = 5 in \\ () -> ?x\r\n In an equation for `f2': f2 () = let ?x = 5 in \\ () -> ?x\r\n\r\nIPRun.hs:24:13:\r\n Ambiguous type variable `a1' in the constraint:\r\n (Show a1) arising from a use of `print'\r\n Probable fix: add a type signature that fixes these type variable(s)\r\n In a stmt of a 'do' expression: print (f2 () ())\r\n In the expression:\r\n do { print (f0 ());\r\n print (f1 ());\r\n print (f2 () ());\r\n print (f3 ()) }\r\n In the expression:\r\n let ?x = 0\r\n in\r\n do { print (f0 ());\r\n print (f1 ());\r\n print (f2 () ());\r\n .... }\r\n\r\n*** unexpected failure for IPRun(normal)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/4392tcrun020 failure2019-07-07T18:59:13ZSimon Marlowtcrun020 failure```
tcrun020 is currently failing all ways:
=====> tcrun020(normal) 1947 of 2622 [0, 12, 0]
cd ./typecheck/should_run && '/64playpen/simonmar/nightly/HEAD-cam-04-unx/x86_64-unknown-linux/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lin...```
tcrun020 is currently failing all ways:
=====> tcrun020(normal) 1947 of 2622 [0, 12, 0]
cd ./typecheck/should_run && '/64playpen/simonmar/nightly/HEAD-cam-04-unx/x86_64-unknown-linux/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-conf -rtsopts -o tcrun020 tcrun020.hs >tcrun020.comp.stderr 2>&1
Compile failed (status 256) errors were:
[1 of 1] Compiling Main ( tcrun020.hs, tcrun020.o )
tcrun020.hs:15:21:
Illegal instance declaration for `C1 m Bool'
(All instance types must be of the form (T a1 ... an)
where a1 ... an are type *variables*,
and each type variable appears at most once in the instance head.
Use -XFlexibleInstances if you want to disable this.)
In the instance declaration for `C1 m Bool'
*** unexpected failure for tcrun020(normal)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"tcrun020 failure","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\ntcrun020 is currently failing all ways:\r\n\r\n=====> tcrun020(normal) 1947 of 2622 [0, 12, 0]\r\ncd ./typecheck/should_run && '/64playpen/simonmar/nightly/HEAD-cam-04-unx/x86_64-unknown-linux/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-conf -rtsopts -o tcrun020 tcrun020.hs >tcrun020.comp.stderr 2>&1\r\nCompile failed (status 256) errors were:\r\n[1 of 1] Compiling Main ( tcrun020.hs, tcrun020.o )\r\n\r\ntcrun020.hs:15:21:\r\n Illegal instance declaration for `C1 m Bool'\r\n (All instance types must be of the form (T a1 ... an)\r\n where a1 ... an are type *variables*,\r\n and each type variable appears at most once in the instance head.\r\n Use -XFlexibleInstances if you want to disable this.)\r\n In the instance declaration for `C1 m Bool'\r\n\r\n*** unexpected failure for tcrun020(normal)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/4385Type-level natural numbers2019-07-07T18:59:14ZIavor S. DiatchkiType-level natural numbersNatural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time ...Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, BlueSpec, Cryptol, Habit).
Existing features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!
Indeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).
Supporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:
- a standard implementation,
- a better notation,
- better error messages,
- a more efficient implementation,
- more complete support for numeric operations.
I have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:
```
http://code.galois.com/darcs/ghc-type-naturals/
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | |
| 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":"Type-level natural numbers","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"diatchki"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, BlueSpec, Cryptol, Habit).\r\n\r\nExisting features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!\r\n\r\nIndeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).\r\n\r\nSupporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:\r\n * a standard implementation,\r\n * a better notation,\r\n * better error messages,\r\n * a more efficient implementation,\r\n * more complete support for numeric operations.\r\n\r\nI have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:\r\n{{{\r\nhttp://code.galois.com/darcs/ghc-type-naturals/\r\n}}}\r\n\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/4364Template Haskell: Cycle in type synonym declarations2019-07-07T18:59:20ZIan Lynagh <igloo@earth.li>Template Haskell: Cycle in type synonym declarations`type-level-numbers-0.1` doesn't build with 7.0.1 RC 1. Here's the essence:
```
{-# LANGUAGE TemplateHaskell #-}
module Q where
data Z
type N0 = $( [t| Z |] )
type N1 = $( [t| Z |] )
```
```
$ ghc --make m.hs
[1 of 1] Compiling Q ...`type-level-numbers-0.1` doesn't build with 7.0.1 RC 1. Here's the essence:
```
{-# LANGUAGE TemplateHaskell #-}
module Q where
data Z
type N0 = $( [t| Z |] )
type N1 = $( [t| Z |] )
```
```
$ ghc --make m.hs
[1 of 1] Compiling Q ( m.hs, m.o )
m.hs:7:1:
Cycle in type synonym declarations:
m.hs:7:1-23: type N0 = $([t| Z |])
m.hs:8:1-23: type N1 = $([t| Z |])
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Template Haskell: Cycle in type synonym declarations","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"7.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"`type-level-numbers-0.1` doesn't build with 7.0.1 RC 1. Here's the essence:\r\n\r\n{{{\r\n{-# LANGUAGE TemplateHaskell #-}\r\nmodule Q where\r\n\r\ndata Z\r\n\r\ntype N0 = $( [t| Z |] )\r\ntype N1 = $( [t| Z |] )\r\n}}}\r\n\r\n{{{\r\n$ ghc --make m.hs\r\n[1 of 1] Compiling Q ( m.hs, m.o )\r\n\r\nm.hs:7:1:\r\n Cycle in type synonym declarations:\r\n m.hs:7:1-23: type N0 = $([t| Z |])\r\n m.hs:8:1-23: type N1 = $([t| Z |])\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.8.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/4361Typechecker regression2019-07-07T18:59:21ZIan Lynagh <igloo@earth.li>Typechecker regressionHere's the essence of the regression DoCon showed up, reported here:
http://www.haskell.org/pipermail/glasgow-haskell-bugs/2010-September/025511.html
```
{-# LANGUAGE FlexibleContexts #-}
module Pol3_ (moduloBasisx) where
class Commut...Here's the essence of the regression DoCon showed up, reported here:
http://www.haskell.org/pipermail/glasgow-haskell-bugs/2010-September/025511.html
```
{-# LANGUAGE FlexibleContexts #-}
module Pol3_ (moduloBasisx) where
class CommutativeRing a
class CommutativeRing a => LinSolvRing a
class LinSolvRing a => EuclideanRing a
instance EuclideanRing a => LinSolvRing (Pol a)
instance CommutativeRing a => CommutativeRing (Pol a)
data Pol a = MkPol
upLinSolvRing :: LinSolvRing a => a -> ()
upLinSolvRing = undefined
moduloBasisx :: (LinSolvRing (Pol a), CommutativeRing a) => Pol a -> ()
moduloBasisx p = let x = upLinSolvRing p
in ()
```
```
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 6.12.2
$ ghc --make Pol3_
[1 of 1] Compiling Pol3_ ( Pol3_.hs, Pol3_.o )
$
```
```
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.0.0.20100924
$ ghc --make Pol3_
[1 of 1] Compiling Pol3_ ( Pol3_.hs, Pol3_.o )
Pol3_.hs:19:26:
Could not deduce (EuclideanRing a)
from the context (LinSolvRing (Pol a), CommutativeRing a)
arising from a use of `upLinSolvRing'
Possible fix:
add (EuclideanRing a) to the context of
the type signature for `moduloBasisx'
In the expression: upLinSolvRing p
In an equation for `x': x = upLinSolvRing p
In the expression: let x = upLinSolvRing p in ()
$
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker regression","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"7.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's the essence of the regression DoCon showed up, reported here:\r\nhttp://www.haskell.org/pipermail/glasgow-haskell-bugs/2010-September/025511.html\r\n\r\n{{{\r\n{-# LANGUAGE FlexibleContexts #-}\r\n\r\nmodule Pol3_ (moduloBasisx) where\r\n\r\nclass CommutativeRing a\r\nclass CommutativeRing a => LinSolvRing a\r\nclass LinSolvRing a => EuclideanRing a\r\n\r\ninstance EuclideanRing a => LinSolvRing (Pol a)\r\ninstance CommutativeRing a => CommutativeRing (Pol a)\r\n\r\ndata Pol a = MkPol\r\n\r\nupLinSolvRing :: LinSolvRing a => a -> ()\r\nupLinSolvRing = undefined\r\n\r\nmoduloBasisx :: (LinSolvRing (Pol a), CommutativeRing a) => Pol a -> ()\r\nmoduloBasisx p = let x = upLinSolvRing p\r\n in ()\r\n}}}\r\n\r\n{{{\r\n$ ghc --version\r\nThe Glorious Glasgow Haskell Compilation System, version 6.12.2\r\n$ ghc --make Pol3_\r\n[1 of 1] Compiling Pol3_ ( Pol3_.hs, Pol3_.o )\r\n$\r\n}}}\r\n\r\n{{{\r\n$ ghc --version\r\nThe Glorious Glasgow Haskell Compilation System, version 7.0.0.20100924\r\n$ ghc --make Pol3_\r\n[1 of 1] Compiling Pol3_ ( Pol3_.hs, Pol3_.o )\r\n\r\nPol3_.hs:19:26:\r\n Could not deduce (EuclideanRing a)\r\n from the context (LinSolvRing (Pol a), CommutativeRing a)\r\n arising from a use of `upLinSolvRing'\r\n Possible fix:\r\n add (EuclideanRing a) to the context of\r\n the type signature for `moduloBasisx'\r\n In the expression: upLinSolvRing p\r\n In an equation for `x': x = upLinSolvRing p\r\n In the expression: let x = upLinSolvRing p in ()\r\n$\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/4358infinite loop on unification with a type family context2019-07-07T18:59:21Zpatrick_premontinfinite loop on unification with a type family contextThe following throws ghc (and ghci) in a loop (ghc-7.0.0.20100925 for i386-unknown-mingw32)
and it eventually aborts with "ghc.exe: out of memory".
```
> {-# LANGUAGE TypeFamilies, Rank2Types, FlexibleContexts #-}
> type family T a
> ...The following throws ghc (and ghci) in a loop (ghc-7.0.0.20100925 for i386-unknown-mingw32)
and it eventually aborts with "ghc.exe: out of memory".
```
> {-# LANGUAGE TypeFamilies, Rank2Types, FlexibleContexts #-}
> type family T a
> t2 :: forall a. ((T a ~ a) => a) -> a
> t2 = t
> t :: forall a. ((T a ~ a) => a) -> a
> t = undefined
```
Using ghc 6.12.1 we do not get a loop, but a puzzling error:
typeBug.lhs:9:7:
Couldn't match expected type `(T a ~ a) => a'
against inferred type `(T a \~ a) =\> a'
Expected type: (T a \~ a) =\> a
Inferred type: (T a \~ a) =\> a
In the expression: t
> In the definition of \`t2': t2 = t
I presume that the non-injectivity of type family T triggers the problem however
the following produces no errors in either version of the compiler.
```
> ok2 :: forall a. T a -> a
> ok2 = ok
> ok :: forall a. T a -> a
> ok = undefined
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.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":"infinite loop on unification with a type family context","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":["context","family","infinite","loop","type"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following throws ghc (and ghci) in a loop (ghc-7.0.0.20100925 for i386-unknown-mingw32)\r\nand it eventually aborts with \"ghc.exe: out of memory\".\r\n\r\n{{{\r\n\r\n> {-# LANGUAGE TypeFamilies, Rank2Types, FlexibleContexts #-}\r\n\r\n> type family T a\r\n\r\n> t2 :: forall a. ((T a ~ a) => a) -> a\r\n> t2 = t\r\n \r\n> t :: forall a. ((T a ~ a) => a) -> a\r\n> t = undefined\r\n\r\n}}}\r\n\r\nUsing ghc 6.12.1 we do not get a loop, but a puzzling error:\r\n\r\ntypeBug.lhs:9:7:\r\n Couldn't match expected type `(T a ~ a) => a'\r\n against inferred type `(T a ~ a) => a'\r\n Expected type: (T a ~ a) => a\r\n Inferred type: (T a ~ a) => a\r\n In the expression: t\r\n In the definition of `t2': t2 = t\r\n\r\nI presume that the non-injectivity of type family T triggers the problem however\r\nthe following produces no errors in either version of the compiler.\r\n\r\n{{{\r\n\r\n> ok2 :: forall a. T a -> a\r\n> ok2 = ok\r\n \r\n> ok :: forall a. T a -> a\r\n> ok = undefined\r\n\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4356type instance doesn't work when the type is (->)2019-07-07T18:59:22ZSjoerd Visschertype instance doesn't work when the type is (->)This doesn't work in 7.0.0.20100924.
It works fine in 6.12.3.
```
{-# LANGUAGE TypeFamilies #-}
type family T t :: * -> * -> *
type instance T Bool = (->)
f :: T Bool Bool Bool
f = not
```
This is the error:
```
Couldn't match typ...This doesn't work in 7.0.0.20100924.
It works fine in 6.12.3.
```
{-# LANGUAGE TypeFamilies #-}
type family T t :: * -> * -> *
type instance T Bool = (->)
f :: T Bool Bool Bool
f = not
```
This is the error:
```
Couldn't match type `T Bool' with `(->)'
Expected type: T Bool Bool Bool
Actual type: Bool -> Bool
In the expression: not
In an equation for `f': f = not
```7.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/4355Coud not deduce (Typeable a) from context (Typeable a, …)2019-07-07T18:59:22ZmaltemCoud not deduce (Typeable a) from context (Typeable a, …)Attached is a module containing code from XMonadContrib that does not type-check anymore with ghc 7.0.1 rc1. I tried to strip the code somewhat down; at least it only depends on base and mtl. Here's the (somewhat irritating) error messag...Attached is a module containing code from XMonadContrib that does not type-check anymore with ghc 7.0.1 rc1. I tried to strip the code somewhat down; at least it only depends on base and mtl. Here's the (somewhat irritating) error message:
```
tcBug.hs:50:30:
Could not deduce (Typeable a)
from the context (Typeable a, Show ts, HList ts a, LayoutClass l a)
arising from a use of `fromMessage'
Possible fix:
add (Typeable a) to the context of the instance declaration
In a stmt of a pattern guard for
an equation for `handleMessage':
Just (Toggle t) <- fromMessage m
In an equation for `handleMessage':
handleMessage mt m
| Just (Toggle t) <- fromMessage m,
i@(Just _) <- find (transformers mt) t
= case currLayout mt of {
EL l det
-> do { l' <- fromMaybe l
`fmap`
handleMessage l (SomeMessage ReleaseResources);
.... }
where
cur = (i == currIndex mt) }
| otherwise
= case currLayout mt of {
EL l det
-> fmap (fmap (\ x -> mt {currLayout = EL x det}))
$ handleMessage l m }
In the instance declaration for `LayoutClass (MultiToggle ts l) a'
tcBug.hs:51:25:
Could not deduce (HList ts a)
from the context (Typeable a,
Show ts,
HList ts a,
LayoutClass l a,
Transformer t a)
arising from a use of `find'
Possible fix:
add (HList ts a) to the context of
the data constructor `Toggle'
or the instance declaration
In a stmt of a pattern guard for
an equation for `handleMessage':
i@(Just _) <- find (transformers mt) t
In a stmt of a pattern guard for
an equation for `handleMessage':
Just (Toggle t) <- fromMessage m
In an equation for `handleMessage':
handleMessage mt m
| Just (Toggle t) <- fromMessage m,
i@(Just _) <- find (transformers mt) t
= case currLayout mt of {
EL l det
-> do { l' <- fromMaybe l
`fmap`
handleMessage l (SomeMessage ReleaseResources);
.... }
where
cur = (i == currIndex mt) }
| otherwise
= case currLayout mt of {
EL l det
-> fmap (fmap (\ x -> mt {currLayout = EL x det}))
$ handleMessage l m }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.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":"Coud not deduce (Typeable a) from context (Typeable a, …)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Attached is a module containing code from XMonadContrib that does not type-check anymore with ghc 7.0.1 rc1. I tried to strip the code somewhat down; at least it only depends on base and mtl. Here's the (somewhat irritating) error message:\r\n\r\n{{{\r\ntcBug.hs:50:30:\r\n Could not deduce (Typeable a)\r\n from the context (Typeable a, Show ts, HList ts a, LayoutClass l a)\r\n arising from a use of `fromMessage'\r\n Possible fix:\r\n add (Typeable a) to the context of the instance declaration\r\n In a stmt of a pattern guard for\r\n an equation for `handleMessage':\r\n Just (Toggle t) <- fromMessage m\r\n In an equation for `handleMessage':\r\n handleMessage mt m\r\n | Just (Toggle t) <- fromMessage m,\r\n i@(Just _) <- find (transformers mt) t\r\n = case currLayout mt of {\r\n EL l det\r\n -> do { l' <- fromMaybe l\r\n `fmap`\r\n handleMessage l (SomeMessage ReleaseResources);\r\n .... }\r\n where\r\n cur = (i == currIndex mt) }\r\n | otherwise\r\n = case currLayout mt of {\r\n EL l det\r\n -> fmap (fmap (\\ x -> mt {currLayout = EL x det}))\r\n $ handleMessage l m }\r\n In the instance declaration for `LayoutClass (MultiToggle ts l) a'\r\n\r\ntcBug.hs:51:25:\r\n Could not deduce (HList ts a)\r\n from the context (Typeable a,\r\n Show ts,\r\n HList ts a,\r\n LayoutClass l a,\r\n Transformer t a)\r\n arising from a use of `find'\r\n Possible fix:\r\n add (HList ts a) to the context of\r\n the data constructor `Toggle'\r\n or the instance declaration\r\n In a stmt of a pattern guard for\r\n an equation for `handleMessage':\r\n i@(Just _) <- find (transformers mt) t\r\n In a stmt of a pattern guard for\r\n an equation for `handleMessage':\r\n Just (Toggle t) <- fromMessage m\r\n In an equation for `handleMessage':\r\n handleMessage mt m\r\n | Just (Toggle t) <- fromMessage m,\r\n i@(Just _) <- find (transformers mt) t\r\n = case currLayout mt of {\r\n EL l det\r\n -> do { l' <- fromMaybe l\r\n `fmap`\r\n handleMessage l (SomeMessage ReleaseResources);\r\n .... }\r\n where\r\n cur = (i == currIndex mt) }\r\n | otherwise\r\n = case currLayout mt of {\r\n EL l det\r\n -> fmap (fmap (\\ x -> mt {currLayout = EL x det}))\r\n $ handleMessage l m }\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/4347Bug in unification of polymorphic and not-yet-polymorphic type2019-07-07T18:59:24ZdolioBug in unification of polymorphic and not-yet-polymorphic typeThe new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of `($)` where it...The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of `($)` where it would have to be instantiated impredicatively.
Initially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because:
```
const :: a -> (forall b. b) -> a
```
is accepted by the type checker. However, the simple:
```
id :: (forall a. a) -> (forall b. b)
```
is not, giving an error message:
```
Couldn't match type `b' with `forall a. a'
`b' is a rigid type variable bound by
an expression type signature at <interactive>:1:32
In the expression: id :: (forall a. a) -> (forall b. b)
```
This would seem to indicate that the type is being rewritten to:
```
forall b. (forall a. a) -> b
```
and then the `forall a. a` matched with the bare `b`. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.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":"Asymmetry of (impredicative) instantiation/higher rank types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of {{{($)}}} where it would have to be instantiated impredicatively.\r\n\r\nInitially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because:\r\n\r\n{{{\r\nconst :: a -> (forall b. b) -> a\r\n}}}\r\n\r\nis accepted by the type checker. However, the simple:\r\n\r\n{{{\r\nid :: (forall a. a) -> (forall b. b)\r\n}}}\r\n\r\nis not, giving an error message:\r\n\r\n{{{\r\n Couldn't match type `b' with `forall a. a'\r\n `b' is a rigid type variable bound by\r\n an expression type signature at <interactive>:1:32\r\n In the expression: id :: (forall a. a) -> (forall b. b)\r\n}}}\r\n\r\nThis would seem to indicate that the type is being rewritten to:\r\n\r\n{{{\r\nforall b. (forall a. a) -> b\r\n}}}\r\n\r\nand then the {{{forall a. a}}} matched with the bare {{{b}}}. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation.","type_of_failure":"OtherFailure","blocking":[]} -->7.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/4338weird discrepancies between TFs and FDs in GHC72019-07-07T18:59:28Zillissiusweird discrepancies between TFs and FDs in GHC7I'm trying to do some seemingly equivalent code with GHC7 as of 09/19, using !TypeFamilies on the one hand and !FunctionalDependencies on the other, and my experience is that the TFs version results in some really weird-ass error message...I'm trying to do some seemingly equivalent code with GHC7 as of 09/19, using !TypeFamilies on the one hand and !FunctionalDependencies on the other, and my experience is that the TFs version results in some really weird-ass error messages from the compiler -- and a hang in one case -- whereas the FDs version works just fine. I'm not sure about the errors, though they certainly seem bizarre, but I'm pretty sure the compiler hanging is a bug. (And I assume a hang is morally equivalent to a crash, so I'm marking this as such.)
Here's the version with TFs:
```
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleContexts #-}
class (There a ~ b, BackAgain b ~ a) => Foo a b where
type There a
type BackAgain b
there :: a -> b
back :: b -> a
tickle :: b -> b
instance Foo Char Int where
type There Char = Int
type BackAgain Int = Char
there = fromEnum
back = toEnum
tickle = (+1)
test :: (Foo a b) => a -> a
test = back . tickle . there
main :: IO ()
main = print $ test 'F'
```
and the one with FDs:
```
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class Bar a b | a -> b, b -> a where
there :: a -> b
back :: b -> a
tickle :: b -> b
instance Bar Char Int where
there = fromEnum
back = toEnum
tickle = (+1)
test :: (Bar a b) => a -> a
test = back . tickle . there
main :: IO ()
main = print $ test 'F'
```
Are these as functionally-equivalent as they seem, or are there some subtle differences I'm missing? (Is it possible there's some kind of configuration problem on my end?)
In any case, the result is that the TFs version gives me different errors depending on which type signatures I supply or omit, whereas the version with FDs compiles and works correctly in all cases.
The TFs version, if I supply both type signatures (as listed):
```
$ ghc Foo.hs
[1 of 1] Compiling Main ( Foo.hs, Foo.o )
Foo.hs:18:15:
Could not deduce (Foo (BackAgain (There a)) (There a))
from the context (Foo a b)
arising from a use of `tickle'
Possible fix:
add (Foo (BackAgain (There a)) (There a)) to the context of
the type signature for `test'
or add an instance declaration for
(Foo (BackAgain (There a)) (There a))
In the first argument of `(.)', namely `tickle'
In the second argument of `(.)', namely `tickle . there'
In the expression: back . tickle . there
Foo.hs:21:16:
Overlapping instances for Foo Char Int
arising from a use of `test'
Matching instances:
instance Foo Char Int -- Defined at Foo.hs:10:10-21
(The choice depends on the instantiation of `'
To pick the first instance above, use -XIncoherentInstances
when compiling the other instance declarations)
In the second argument of `($)', namely `test 'F''
In the expression: print $ test 'F'
In an equation for `main': main = print $ test 'F'
```
If I leave off the type signature for main, but not test:
```
$ ghc Foo.hs
[1 of 1] Compiling Main ( Foo.hs, Foo.o )
Foo.hs:18:15:
Could not deduce (Foo (BackAgain (There a)) (There a))
from the context (Foo a b)
arising from a use of `tickle'
Possible fix:
add (Foo (BackAgain (There a)) (There a)) to the context of
the type signature for `test'
or add an instance declaration for
(Foo (BackAgain (There a)) (There a))
In the first argument of `(.)', namely `tickle'
In the second argument of `(.)', namely `tickle . there'
In the expression: back . tickle . there
```
If I leave off the signature for test, regardless of whether I supply one for main:
```
$ ghc Foo.hs
[1 of 1] Compiling Main ( Foo.hs, Foo.o )
^C
-- a seemingly infinite loop
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.13 |
| 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":"weird discrepancies between TFs and FDs in GHC7","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.13","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm trying to do some seemingly equivalent code with GHC7 as of 09/19, using !TypeFamilies on the one hand and !FunctionalDependencies on the other, and my experience is that the TFs version results in some really weird-ass error messages from the compiler -- and a hang in one case -- whereas the FDs version works just fine. I'm not sure about the errors, though they certainly seem bizarre, but I'm pretty sure the compiler hanging is a bug. (And I assume a hang is morally equivalent to a crash, so I'm marking this as such.)\r\n\r\nHere's the version with TFs:\r\n\r\n{{{\r\n{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleContexts #-}\r\n\r\nclass (There a ~ b, BackAgain b ~ a) => Foo a b where\r\n type There a\r\n type BackAgain b\r\n there :: a -> b\r\n back :: b -> a\r\n tickle :: b -> b\r\n\r\ninstance Foo Char Int where\r\n type There Char = Int\r\n type BackAgain Int = Char\r\n there = fromEnum\r\n back = toEnum\r\n tickle = (+1)\r\n\r\ntest :: (Foo a b) => a -> a\r\ntest = back . tickle . there\r\n\r\nmain :: IO ()\r\nmain = print $ test 'F'\r\n}}}\r\n\r\n\r\nand the one with FDs:\r\n\r\n{{{\r\n{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}\r\n\r\nclass Bar a b | a -> b, b -> a where\r\n there :: a -> b\r\n back :: b -> a\r\n tickle :: b -> b\r\n\r\ninstance Bar Char Int where\r\n there = fromEnum\r\n back = toEnum\r\n tickle = (+1)\r\n\r\ntest :: (Bar a b) => a -> a\r\ntest = back . tickle . there\r\n\r\nmain :: IO ()\r\nmain = print $ test 'F'\r\n}}}\r\n\r\nAre these as functionally-equivalent as they seem, or are there some subtle differences I'm missing? (Is it possible there's some kind of configuration problem on my end?)\r\n\r\n\r\nIn any case, the result is that the TFs version gives me different errors depending on which type signatures I supply or omit, whereas the version with FDs compiles and works correctly in all cases.\r\n\r\nThe TFs version, if I supply both type signatures (as listed):\r\n\r\n{{{\r\n$ ghc Foo.hs \r\n[1 of 1] Compiling Main ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:18:15:\r\n Could not deduce (Foo (BackAgain (There a)) (There a))\r\n from the context (Foo a b)\r\n arising from a use of `tickle'\r\n Possible fix:\r\n add (Foo (BackAgain (There a)) (There a)) to the context of\r\n the type signature for `test'\r\n or add an instance declaration for\r\n (Foo (BackAgain (There a)) (There a))\r\n In the first argument of `(.)', namely `tickle'\r\n In the second argument of `(.)', namely `tickle . there'\r\n In the expression: back . tickle . there\r\n\r\nFoo.hs:21:16:\r\n Overlapping instances for Foo Char Int\r\n arising from a use of `test'\r\n Matching instances:\r\n instance Foo Char Int -- Defined at Foo.hs:10:10-21\r\n (The choice depends on the instantiation of `'\r\n To pick the first instance above, use -XIncoherentInstances\r\n when compiling the other instance declarations)\r\n In the second argument of `($)', namely `test 'F''\r\n In the expression: print $ test 'F'\r\n In an equation for `main': main = print $ test 'F'\r\n}}}\r\n\r\n\r\nIf I leave off the type signature for main, but not test:\r\n\r\n{{{\r\n$ ghc Foo.hs \r\n[1 of 1] Compiling Main ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:18:15:\r\n Could not deduce (Foo (BackAgain (There a)) (There a))\r\n from the context (Foo a b)\r\n arising from a use of `tickle'\r\n Possible fix:\r\n add (Foo (BackAgain (There a)) (There a)) to the context of\r\n the type signature for `test'\r\n or add an instance declaration for\r\n (Foo (BackAgain (There a)) (There a))\r\n In the first argument of `(.)', namely `tickle'\r\n In the second argument of `(.)', namely `tickle . there'\r\n In the expression: back . tickle . there\r\n}}}\r\n\r\nIf I leave off the signature for test, regardless of whether I supply one for main:\r\n\r\n{{{\r\n$ ghc Foo.hs \r\n[1 of 1] Compiling Main ( Foo.hs, Foo.o )\r\n^C\r\n-- a seemingly infinite loop\r\n}}}\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/4284Adding parentheses introduces type error2019-07-07T18:59:42ZjpbernardyAdding parentheses introduces type error```
{-# LANGUAGE RankNTypes #-}
module Test where
foo :: () -> forall b. b
foo = undefined
works = id foo
fails = (id) foo
-- works type checks, but fails fails with the following error
-- message:
--
-- Cannot match a monotype wi...```
{-# LANGUAGE RankNTypes #-}
module Test where
foo :: () -> forall b. b
foo = undefined
works = id foo
fails = (id) foo
-- works type checks, but fails fails with the following error
-- message:
--
-- Cannot match a monotype with `() -> forall b. b'
-- Probable cause: `foo' is applied to too few arguments
-- In the first argument of `(id)', namely `foo'
-- In the expression: (id) foo
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | nad |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Adding parentheses introduces type error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.3","keywords":["higher-rank","polymorphism"],"differentials":[],"test_case":"","architecture":"","cc":["nad"],"type":"Bug","description":"{{{\r\n{-# LANGUAGE RankNTypes #-}\r\n\r\nmodule Test where\r\n\r\nfoo :: () -> forall b. b\r\nfoo = undefined\r\n\r\nworks = id foo\r\n\r\nfails = (id) foo\r\n\r\n-- works type checks, but fails fails with the following error\r\n-- message:\r\n--\r\n-- Cannot match a monotype with `() -> forall b. b'\r\n-- Probable cause: `foo' is applied to too few arguments\r\n-- In the first argument of `(id)', namely `foo'\r\n-- In the expression: (id) foo\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4272Typechecker loop with type families2019-07-07T18:59:45ZGhost UserTypechecker loop with type familiesThe following code (which I think is ill-typed) causes GHC to hang, both on 6.12.1 and 6.13.20100616:
```
{-# LANGUAGE TypeFamilies, ScopedTypeVariables, FlexibleContexts #-}
module Crash where
class Family f where
terms :: f a -> a
...The following code (which I think is ill-typed) causes GHC to hang, both on 6.12.1 and 6.13.20100616:
```
{-# LANGUAGE TypeFamilies, ScopedTypeVariables, FlexibleContexts #-}
module Crash where
class Family f where
terms :: f a -> a
class Family (TermFamily a) => TermLike a where
type TermFamily a :: * -> *
laws :: forall a b. TermLike a => TermFamily a a -> b
laws t = prune t (terms (undefined :: TermFamily a a))
prune :: TermLike a => TermFamily a a -> TermFamily a a -> b
prune = undefined
```
The compiler still hangs if I remove the typeclass constraints (everything to the left of a =\>, I mean), but everything else seems to be necessary for the compiler to loop. Using -dshow-passes shows that it's the typechecker that loops.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.13 |
| 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":"Typechecker loop with type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.13","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code (which I think is ill-typed) causes GHC to hang, both on 6.12.1 and 6.13.20100616:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies, ScopedTypeVariables, FlexibleContexts #-}\r\nmodule Crash where\r\n\r\nclass Family f where\r\n terms :: f a -> a\r\n\r\nclass Family (TermFamily a) => TermLike a where\r\n type TermFamily a :: * -> *\r\n\r\nlaws :: forall a b. TermLike a => TermFamily a a -> b\r\nlaws t = prune t (terms (undefined :: TermFamily a a))\r\n\r\nprune :: TermLike a => TermFamily a a -> TermFamily a a -> b\r\nprune = undefined\r\n}}}\r\n\r\nThe compiler still hangs if I remove the typeclass constraints (everything to the left of a =>, I mean), but everything else seems to be necessary for the compiler to loop. Using -dshow-passes shows that it's the typechecker that loops.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4235deriving Enum fails for data instances2019-07-07T18:59:55Znestraderiving Enum fails for data instancesThe following sample module does not compile:
```
{-# LANGUAGE TypeFamilies #-}
module Foo where
data family Foo a
data instance Foo Int
= A | B
deriving (Enum)
```
GHC gives 5 error messages, all to line 8 (the deriving clause),...The following sample module does not compile:
```
{-# LANGUAGE TypeFamilies #-}
module Foo where
data family Foo a
data instance Foo Int
= A | B
deriving (Enum)
```
GHC gives 5 error messages, all to line 8 (the deriving clause), in terms of some internal representations of variables and types. I think that an error message should not be of this kind even if the code really contains an error. But here I even do not understand why the code should not be valid. In the case of deriving Eq, Ord, Bounded or Show for the same Foo Int, everything works fine; and also, old good instance declaration instead of deriving gives a normally working code. (Analogous errors are produced when deriving Ix.)
Here is the output of GHCi -v in the case of the above module (GHC gives a similar one):
```
Prelude> :l Foo
*** Chasing dependencies:
Chasing modules from:
Stable obj: []
Stable BCO: []
unload: retaining objs []
unload: retaining bcos []
Ready for upsweep []
Upsweep completely successful.
*** Deleting temp files:
Deleting:
*** Chasing dependencies:
Chasing modules from: *Foo.hs
Stable obj: []
Stable BCO: []
unload: retaining objs []
unload: retaining bcos []
Ready for upsweep
[NONREC
ModSummary {
ms_hs_date = Mon Aug 2 14:30:44 UTC 2010
ms_mod = main:Foo,
ms_imps = []
ms_srcimps = []
}]
compile: input file Foo.hs
*** Checking old interface for main:Foo:
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
*** Parser:
*** Renamer/typechecker:
Foo.hs:8:12:
Couldn't match expected type `Foo Int'
against inferred type `Foo.R:FooInt'
NB: `Foo' is a type function
In the expression: Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) 1)
In the expression:
if (==) Foo.$maxtag_R:FooInt (GHC.Types.I# a#) then
error
"succ{R:FooInt}: tried to take `succ' of last tag in enumeration"
else
Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) 1)
In a case alternative:
a#
-> if (==) Foo.$maxtag_R:FooInt (GHC.Types.I# a#) then
error
"succ{R:FooInt}: tried to take `succ' of last tag in enumeration"
else
Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) 1)
Foo.hs:8:12:
Couldn't match expected type `Foo Int'
against inferred type `Foo.R:FooInt'
NB: `Foo' is a type function
In the expression: Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) -1)
In the expression:
if (==) 0 (GHC.Types.I# a#) then
error
"pred{R:FooInt}: tried to take `pred' of first tag in enumeration"
else
Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) -1)
In a case alternative:
a#
-> if (==) 0 (GHC.Types.I# a#) then
error
"pred{R:FooInt}: tried to take `pred' of first tag in enumeration"
else
Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) -1)
Foo.hs:8:12:
Couldn't match expected type `Foo Int'
against inferred type `Foo.R:FooInt'
NB: `Foo' is a type function
In the expression: Foo.$tag2con_R:FooInt a
In the expression:
if (&&) ((>=) a 0) ((<=) a Foo.$maxtag_R:FooInt) then
Foo.$tag2con_R:FooInt a
else
error
((++)
"toEnum{R:FooInt}: tag ("
(showsPrec
0
a
((++)
") is outside of enumeration's range (0,"
(showsPrec 0 Foo.$maxtag_R:FooInt ")"))))
In the definition of `toEnum':
toEnum a = if (&&) ((>=) a 0) ((<=) a Foo.$maxtag_R:FooInt) then
Foo.$tag2con_R:FooInt a
else
error
((++)
"toEnum{R:FooInt}: tag ("
(showsPrec
0
a
((++)
") is outside of enumeration's range (0,"
(showsPrec 0 Foo.$maxtag_R:FooInt ")"))))
Foo.hs:8:12:
Couldn't match expected type `Foo Int'
against inferred type `Foo.R:FooInt'
NB: `Foo' is a type function
In the first argument of `map', namely `Foo.$tag2con_R:FooInt'
In the expression:
map
Foo.$tag2con_R:FooInt
(enumFromTo (GHC.Types.I# a#) Foo.$maxtag_R:FooInt)
In a case alternative:
a#
-> map
Foo.$tag2con_R:FooInt
(enumFromTo (GHC.Types.I# a#) Foo.$maxtag_R:FooInt)
Foo.hs:8:12:
Couldn't match expected type `Foo Int'
against inferred type `Foo.R:FooInt'
NB: `Foo' is a type function
In the first argument of `map', namely `Foo.$tag2con_R:FooInt'
In the expression:
map
Foo.$tag2con_R:FooInt
(enumFromThenTo
(GHC.Types.I# a#)
(GHC.Types.I# b#)
(if (>) (GHC.Types.I# a#) (GHC.Types.I# b#) then
0
else
Foo.$maxtag_R:FooInt))
In a case alternative:
b#
-> map
Foo.$tag2con_R:FooInt
(enumFromThenTo
(GHC.Types.I# a#)
(GHC.Types.I# b#)
(if (>) (GHC.Types.I# a#) (GHC.Types.I# b#) then
0
else
Foo.$maxtag_R:FooInt))
*** Deleting temp files:
Deleting:
Upsweep partially successful.
*** Deleting temp files:
Deleting:
Failed, modules loaded: none.
```
Making deriving stand-alone does not help (the error messages would be more or less similar). It seems that the automatically derived code for methods is buggy and does not type-check.
Using GADTs also does not help, but the feedback is different. In the case of GADTs, (stand-alone) deriving does not work for other type classes either. For example, if the module is
```
{-# LANGUAGE GADTs, StandaloneDeriving, FlexibleInstances #-}
module Foo where
data Foo a where
A :: Foo Int
B :: Foo Int
deriving instance (Eq (Foo Int))
```
then GHCi says the following:
```
Foo.hs:1:0:
GADT pattern match in non-rigid context for `A'
Probable solution: add a type signature for `Foo.$con2tag_Foo'
In the pattern: A
In the definition of `Foo.$con2tag_Foo': Foo.$con2tag_Foo A = 0#
```
Note the location of the error according to the message!
Anyway, after deleting the stand-alone deriving, GHCi is satisfied. By the way, :i A then gives:
```
data Foo a where
A :: (a ~ Int) => Foo Int
...
```
However, :t A gives:
```
A :: Foo Int
```
So, is the type system of GHC ambiguous? Why are the types given by :i and :t different?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.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":"deriving Enum fails for data instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.3","keywords":["GADTs","deriving,","families,","instance","type"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following sample module does not compile:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\ndata family Foo a\r\n\r\ndata instance Foo Int\r\n = A | B\r\n deriving (Enum)\r\n}}}\r\n\r\nGHC gives 5 error messages, all to line 8 (the deriving clause), in terms of some internal representations of variables and types. I think that an error message should not be of this kind even if the code really contains an error. But here I even do not understand why the code should not be valid. In the case of deriving Eq, Ord, Bounded or Show for the same Foo Int, everything works fine; and also, old good instance declaration instead of deriving gives a normally working code. (Analogous errors are produced when deriving Ix.)\r\n\r\nHere is the output of GHCi -v in the case of the above module (GHC gives a similar one):\r\n\r\n{{{\r\nPrelude> :l Foo\r\n*** Chasing dependencies:\r\nChasing modules from:\r\nStable obj: []\r\nStable BCO: []\r\nunload: retaining objs []\r\nunload: retaining bcos []\r\nReady for upsweep []\r\nUpsweep completely successful.\r\n*** Deleting temp files:\r\nDeleting:\r\n*** Chasing dependencies:\r\nChasing modules from: *Foo.hs\r\nStable obj: []\r\nStable BCO: []\r\nunload: retaining objs []\r\nunload: retaining bcos []\r\nReady for upsweep\r\n [NONREC\r\n ModSummary {\r\n ms_hs_date = Mon Aug 2 14:30:44 UTC 2010\r\n ms_mod = main:Foo,\r\n ms_imps = []\r\n ms_srcimps = []\r\n }]\r\ncompile: input file Foo.hs\r\n*** Checking old interface for main:Foo:\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n*** Parser:\r\n*** Renamer/typechecker:\r\n\r\nFoo.hs:8:12:\r\n Couldn't match expected type `Foo Int'\r\n against inferred type `Foo.R:FooInt'\r\n NB: `Foo' is a type function\r\n In the expression: Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) 1)\r\n In the expression:\r\n if (==) Foo.$maxtag_R:FooInt (GHC.Types.I# a#) then\r\n error\r\n \"succ{R:FooInt}: tried to take `succ' of last tag in enumeration\"\r\n else\r\n Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) 1)\r\n In a case alternative:\r\n a#\r\n -> if (==) Foo.$maxtag_R:FooInt (GHC.Types.I# a#) then\r\n error\r\n \"succ{R:FooInt}: tried to take `succ' of last tag in enumeration\"\r\n else\r\n Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) 1)\r\n\r\nFoo.hs:8:12:\r\n Couldn't match expected type `Foo Int'\r\n against inferred type `Foo.R:FooInt'\r\n NB: `Foo' is a type function\r\n In the expression: Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) -1)\r\n In the expression:\r\n if (==) 0 (GHC.Types.I# a#) then\r\n error\r\n \"pred{R:FooInt}: tried to take `pred' of first tag in enumeration\"\r\n else\r\n Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) -1)\r\n In a case alternative:\r\n a#\r\n -> if (==) 0 (GHC.Types.I# a#) then\r\n error\r\n \"pred{R:FooInt}: tried to take `pred' of first tag in enumeration\"\r\n else\r\n Foo.$tag2con_R:FooInt ((+) (GHC.Types.I# a#) -1)\r\n\r\nFoo.hs:8:12:\r\n Couldn't match expected type `Foo Int'\r\n against inferred type `Foo.R:FooInt'\r\n NB: `Foo' is a type function\r\n In the expression: Foo.$tag2con_R:FooInt a\r\n In the expression:\r\n if (&&) ((>=) a 0) ((<=) a Foo.$maxtag_R:FooInt) then\r\n Foo.$tag2con_R:FooInt a\r\n else\r\n error\r\n ((++)\r\n \"toEnum{R:FooInt}: tag (\"\r\n (showsPrec\r\n 0\r\n a\r\n ((++)\r\n \") is outside of enumeration's range (0,\"\r\n (showsPrec 0 Foo.$maxtag_R:FooInt \")\"))))\r\n In the definition of `toEnum':\r\n toEnum a = if (&&) ((>=) a 0) ((<=) a Foo.$maxtag_R:FooInt) then\r\n Foo.$tag2con_R:FooInt a\r\n else\r\n error\r\n ((++)\r\n \"toEnum{R:FooInt}: tag (\"\r\n (showsPrec\r\n 0\r\n a\r\n ((++)\r\n \") is outside of enumeration's range (0,\"\r\n (showsPrec 0 Foo.$maxtag_R:FooInt \")\"))))\r\n\r\nFoo.hs:8:12:\r\n Couldn't match expected type `Foo Int'\r\n against inferred type `Foo.R:FooInt'\r\n NB: `Foo' is a type function\r\n In the first argument of `map', namely `Foo.$tag2con_R:FooInt'\r\n In the expression:\r\n map\r\n Foo.$tag2con_R:FooInt\r\n (enumFromTo (GHC.Types.I# a#) Foo.$maxtag_R:FooInt)\r\n In a case alternative:\r\n a#\r\n -> map\r\n Foo.$tag2con_R:FooInt\r\n (enumFromTo (GHC.Types.I# a#) Foo.$maxtag_R:FooInt)\r\n\r\nFoo.hs:8:12:\r\n Couldn't match expected type `Foo Int'\r\n against inferred type `Foo.R:FooInt'\r\n NB: `Foo' is a type function\r\n In the first argument of `map', namely `Foo.$tag2con_R:FooInt'\r\n In the expression:\r\n map\r\n Foo.$tag2con_R:FooInt\r\n (enumFromThenTo\r\n (GHC.Types.I# a#)\r\n (GHC.Types.I# b#)\r\n (if (>) (GHC.Types.I# a#) (GHC.Types.I# b#) then\r\n 0\r\n else\r\n Foo.$maxtag_R:FooInt))\r\n In a case alternative:\r\n b#\r\n -> map\r\n Foo.$tag2con_R:FooInt\r\n (enumFromThenTo\r\n (GHC.Types.I# a#)\r\n (GHC.Types.I# b#)\r\n (if (>) (GHC.Types.I# a#) (GHC.Types.I# b#) then\r\n 0\r\n else\r\n Foo.$maxtag_R:FooInt))\r\n*** Deleting temp files:\r\nDeleting:\r\nUpsweep partially successful.\r\n*** Deleting temp files:\r\nDeleting:\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nMaking deriving stand-alone does not help (the error messages would be more or less similar). It seems that the automatically derived code for methods is buggy and does not type-check.\r\n\r\nUsing GADTs also does not help, but the feedback is different. In the case of GADTs, (stand-alone) deriving does not work for other type classes either. For example, if the module is \r\n\r\n{{{\r\n{-# LANGUAGE GADTs, StandaloneDeriving, FlexibleInstances #-}\r\nmodule Foo where\r\n\r\ndata Foo a where\r\n A :: Foo Int\r\n B :: Foo Int\r\n\r\nderiving instance (Eq (Foo Int))\r\n}}}\r\nthen GHCi says the following:\r\n\r\n{{{\r\nFoo.hs:1:0:\r\n GADT pattern match in non-rigid context for `A'\r\n Probable solution: add a type signature for `Foo.$con2tag_Foo'\r\n In the pattern: A\r\n In the definition of `Foo.$con2tag_Foo': Foo.$con2tag_Foo A = 0#\r\n}}}\r\n\r\nNote the location of the error according to the message! \r\nAnyway, after deleting the stand-alone deriving, GHCi is satisfied. By the way, :i A then gives:\r\n\r\n{{{\r\ndata Foo a where\r\n A :: (a ~ Int) => Foo Int\r\n ...\r\n}}}\r\n\r\nHowever, :t A gives:\r\n\r\n{{{\r\nA :: Foo Int\r\n}}}\r\n\r\nSo, is the type system of GHC ambiguous? Why are the types given by :i and :t different?\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4232Finish and merge new typechecker branch2019-07-07T18:59:56ZIan Lynagh <igloo@earth.li>Finish and merge new typechecker branchFinish and merge new typechecker branch
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.13 ...Finish and merge new typechecker branch
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.13 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Finish and merge new typechecker branch","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"6.13","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Finish and merge new typechecker branch","type_of_failure":"OtherFailure","blocking":[]} -->7.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/4226Lifting constraints is questionably correct for implicit parameters.2019-07-07T19:00:00ZdolioLifting constraints is questionably correct for implicit parameters.Greetings,
While fooling with implicit parameters today, I encountered an anomaly. Part of (I think) the justification of implicit parameters is that the types inform you of what they do. So, for instance:
```
(\() -> ?x) :: (?x :: Int...Greetings,
While fooling with implicit parameters today, I encountered an anomaly. Part of (I think) the justification of implicit parameters is that the types inform you of what they do. So, for instance:
```
(\() -> ?x) :: (?x :: Int) => () -> Int
```
depends on an implicit parameter, while:
```
(let ?x = 5 in \() -> ?x) :: () -> Int
```
does not. However, I discovered that the following:
```
(let ?x = 5 in \() -> ?x) :: () -> ((?x :: Int) => Int)
```
generates a function whose implicit parameter `?x` is actually unbound, so if we let that expression be `f`, then:
```
let ?x = 4 in f ()
```
yields 4. By contrast, if we give the type:
```
(let ?x = 5 in \() -> ?x) :: (?x :: Int) => () -> Int
```
the `?x` in the lambda expression *is* bound, and the implicit parameter constraint is spurious (like `5 :: (?x :: Int) => Int`). This happens for definitions in which types are given, so it does not seem like it is a case of the note on monomorphism in the implicit parameters documentation. For instance:
```
let f :: (?x :: Int) => () -> Int
f = let ?x = 5 in \() -> ?x
g :: () -> ((?x :: Int) => Int)
g = let ?x = 5 in \() -> ?x
in let ?x = 4
in (f (), g()) -- (5, 4)
```
This would arguably be fine, as the two have different types. However, GHC does not actually distinguish them. Asking the type of either will generate:
`(?x :: Int) => () -> Int`
Instead of the one with the higher-rank (so to speak) constraint.
I get this behavior using 6.12.1, but it seems unlikely that it would have changed in the 6.12 series.
Strictly speaking, I'm not sure I can call this a bug. Due to context weakening, there's probably no way to unambiguously clarify using types which values are genuinely dependent on implicit parameters, and which are not (similar to `ask` versus `local (const 5) ask` in `Reader`). However, it seems odd that the type annotations make a difference, yet are not subsequently distinguished. It's also conceivable that the `() -> ((?x :: Int) => Int)` behavior is unintentional. I am unsure which, if any, of these resolutions is appropriate.
So, instead, I'll call this a proposal, that we determine whether this is the intended behavior (feel free to promote to a bug if it is decided that something needs to be fixed, however). :)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.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":"Lifting constraints is questionably correct for implicit parameters.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":["implicit","parameters"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Greetings,\r\n\r\nWhile fooling with implicit parameters today, I encountered an anomaly. Part of (I think) the justification of implicit parameters is that the types inform you of what they do. So, for instance:\r\n\r\n{{{\r\n(\\() -> ?x) :: (?x :: Int) => () -> Int\r\n}}}\r\n\r\ndepends on an implicit parameter, while:\r\n\r\n{{{\r\n(let ?x = 5 in \\() -> ?x) :: () -> Int\r\n}}}\r\n\r\ndoes not. However, I discovered that the following:\r\n\r\n{{{\r\n(let ?x = 5 in \\() -> ?x) :: () -> ((?x :: Int) => Int)\r\n}}}\r\n\r\ngenerates a function whose implicit parameter {{{?x}}} is actually unbound, so if we let that expression be {{{f}}}, then:\r\n\r\n{{{\r\nlet ?x = 4 in f ()\r\n}}}\r\n\r\nyields 4. By contrast, if we give the type:\r\n{{{\r\n(let ?x = 5 in \\() -> ?x) :: (?x :: Int) => () -> Int\r\n}}}\r\n\r\nthe {{{?x}}} in the lambda expression ''is'' bound, and the implicit parameter constraint is spurious (like {{{5 :: (?x :: Int) => Int}}}). This happens for definitions in which types are given, so it does not seem like it is a case of the note on monomorphism in the implicit parameters documentation. For instance:\r\n\r\n{{{\r\nlet f :: (?x :: Int) => () -> Int\r\n f = let ?x = 5 in \\() -> ?x\r\n g :: () -> ((?x :: Int) => Int)\r\n g = let ?x = 5 in \\() -> ?x\r\n in let ?x = 4\r\n in (f (), g()) -- (5, 4)\r\n}}}\r\n\r\nThis would arguably be fine, as the two have different types. However, GHC does not actually distinguish them. Asking the type of either will generate:\r\n\r\n{{{(?x :: Int) => () -> Int}}}\r\n\r\nInstead of the one with the higher-rank (so to speak) constraint.\r\n\r\nI get this behavior using 6.12.1, but it seems unlikely that it would have changed in the 6.12 series.\r\n\r\nStrictly speaking, I'm not sure I can call this a bug. Due to context weakening, there's probably no way to unambiguously clarify using types which values are genuinely dependent on implicit parameters, and which are not (similar to {{{ask}}} versus {{{local (const 5) ask}}} in {{{Reader}}}). However, it seems odd that the type annotations make a difference, yet are not subsequently distinguished. It's also conceivable that the {{{() -> ((?x :: Int) => Int)}}} behavior is unintentional. I am unsure which, if any, of these resolutions is appropriate.\r\n\r\nSo, instead, I'll call this a proposal, that we determine whether this is the intended behavior (feel free to promote to a bug if it is decided that something needs to be fixed, however). :)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4179Infinite loop with type function inference2019-07-07T19:00:14ZSimon Peyton JonesInfinite loop with type function inferenceKevin Quick (quick\@sparq.org) writes:
I started with the following:
```
{-# LANGUAGE TypeFamilies #-}
class DoC a where
type A2 a
op :: a -> A2 a
data Con x = InCon (x (Con x))
type FCon x = x (Con x)
foldDoC :: Functor f...Kevin Quick (quick\@sparq.org) writes:
I started with the following:
```
{-# LANGUAGE TypeFamilies #-}
class DoC a where
type A2 a
op :: a -> A2 a
data Con x = InCon (x (Con x))
type FCon x = x (Con x)
foldDoC :: Functor f => (f a -> a) -> Con f -> a foldDoC f (InCon t) = f (fmap (foldDoC f) t)
doCon :: (DoC (FCon x)) => Con x -> A2 (FCon x) doCon (InCon x) = op x
fCon :: (Functor x, DoC (FCon x)) => Con x -> A2 (FCon x) fCon = foldDoC op
```
I then changed the rank of op, but forgot to update the foldDoC accordingly---see below. Attempting to compile this causes GHC to run forever using 100% cpu. The corrected definition of foldDoC works fine. Should the GHC (6.12.1) behavior in the face of my foolishness be reported as a bug or is this a legitimate infinite recursion of type deduction?
```
{-# LANGUAGE TypeFamilies #-}
class DoC a where
type A2 a
type A3 a
op :: a -> A2 a -> A3 a
data Con x = InCon (x (Con x))
type FCon x = x (Con x)
-- should have been changed to this, which works
-- foldDoC :: Functor f => (f a -> a) -> A2 (FCon f) -> Con f -> a
-- foldDoC f i (InCon t) = f (fmap (foldDoC f i) t)
-- this original version causes GHC to hang foldDoC :: Functor f => (f a -> a) -> Con f -> a foldDoC f (InCon t) = f (fmap (foldDoC f) t)
doCon :: (DoC (FCon x)) => Con x -> A2 (FCon x) -> A3 (FCon x) doCon (InCon x) = op x
-- note that if this is commented out then there's no hang: presumably because GHC doesn't have to perform type deduction for foldDoC.
fCon :: (Functor x, DoC (FCon x)) => Con x -> A2 (FCon x) -> A3 (FCon x) fCon = foldDoC op
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 6.12.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":"Infinite loop with type function inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Kevin Quick (quick@sparq.org) writes:\r\nI started with the following:\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\nclass DoC a where\r\n type A2 a\r\n op :: a -> A2 a\r\n\r\ndata Con x = InCon (x (Con x))\r\ntype FCon x = x (Con x)\r\n\r\nfoldDoC :: Functor f => (f a -> a) -> Con f -> a foldDoC f (InCon t) = f (fmap (foldDoC f) t)\r\n\r\ndoCon :: (DoC (FCon x)) => Con x -> A2 (FCon x) doCon (InCon x) = op x\r\n\r\nfCon :: (Functor x, DoC (FCon x)) => Con x -> A2 (FCon x) fCon = foldDoC op\r\n}}}\r\nI then changed the rank of op, but forgot to update the foldDoC accordingly---see below. Attempting to compile this causes GHC to run forever using 100% cpu. The corrected definition of foldDoC works fine. Should the GHC (6.12.1) behavior in the face of my foolishness be reported as a bug or is this a legitimate infinite recursion of type deduction?\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\nclass DoC a where\r\n type A2 a\r\n type A3 a\r\n op :: a -> A2 a -> A3 a\r\n\r\ndata Con x = InCon (x (Con x))\r\ntype FCon x = x (Con x)\r\n\r\n-- should have been changed to this, which works\r\n-- foldDoC :: Functor f => (f a -> a) -> A2 (FCon f) -> Con f -> a\r\n-- foldDoC f i (InCon t) = f (fmap (foldDoC f i) t)\r\n\r\n-- this original version causes GHC to hang foldDoC :: Functor f => (f a -> a) -> Con f -> a foldDoC f (InCon t) = f (fmap (foldDoC f) t)\r\n\r\ndoCon :: (DoC (FCon x)) => Con x -> A2 (FCon x) -> A3 (FCon x) doCon (InCon x) = op x\r\n\r\n-- note that if this is commented out then there's no hang: presumably because GHC doesn't have to perform type deduction for foldDoC.\r\nfCon :: (Functor x, DoC (FCon x)) => Con x -> A2 (FCon x) -> A3 (FCon x) fCon = foldDoC op\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4178Lazy evaluation of type families causes quantified type variables to escape2019-07-07T19:00:14ZintoverflowLazy evaluation of type families causes quantified type variables to escapeThis may be related to tickets #3005 and #3297.
Consider the following function, which is idiomatic for using rank-2 types to prevent data from escaping a context:
```
useRank2 :: (forall a . a -> b) -> b
useRank2 f = f "foo"
```
If `...This may be related to tickets #3005 and #3297.
Consider the following function, which is idiomatic for using rank-2 types to prevent data from escaping a context:
```
useRank2 :: (forall a . a -> b) -> b
useRank2 f = f "foo"
```
If `b` is unified to a type function that makes mention of `a`, the compiler will reject the program for allowing a quantified type variable to escape, even in circumstances where evaluating the type function would yield a type that does not mention `a`.
Here is complete source for demonstrating the issue:
```
{-# LANGUAGE
FlexibleContexts,
Rank2Types,
TypeFamilies,
MultiParamTypeClasses,
FlexibleInstances #-}
data True = T
data False = F
class Decide tf a b where
type If tf a b
nonFunctionalIf :: tf -> a -> b -> If tf a b
instance Decide True a b where
type If True a b = a
nonFunctionalIf T a b = a
instance Decide False a b where
type If False a b = b
nonFunctionalIf F a b = b
useRank2 :: (forall a . a -> b) -> b
useRank2 f = f "foo"
hasTrouble a = nonFunctionalIf F a (2 :: Int)
-- try useRank2 hasTrouble
hasNoTrouble :: a -> Int
hasNoTrouble = hasTrouble
-- try useRank2 hasNoTrouble
```
Certainly the program should be rejected when there is inadequate information to evaluate the type function, but it seems odd to reject `hasTrouble` and not `hasNoTrouble` given that they are equal.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 6.12.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":"Lazy evaluation of type families causes quantified type variables to escape","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be related to tickets #3005 and #3297.\r\n\r\nConsider the following function, which is idiomatic for using rank-2 types to prevent data from escaping a context:\r\n\r\n{{{\r\nuseRank2 :: (forall a . a -> b) -> b\r\nuseRank2 f = f \"foo\"\r\n}}}\r\n\r\nIf {{{b}}} is unified to a type function that makes mention of {{{a}}}, the compiler will reject the program for allowing a quantified type variable to escape, even in circumstances where evaluating the type function would yield a type that does not mention {{{a}}}.\r\n\r\nHere is complete source for demonstrating the issue:\r\n\r\n{{{\r\n{-# LANGUAGE\r\n\tFlexibleContexts,\r\n\tRank2Types,\r\n\tTypeFamilies,\r\n\tMultiParamTypeClasses,\r\n\tFlexibleInstances #-}\r\n\r\ndata True = T\r\ndata False = F\r\n\r\nclass Decide tf a b where\r\n type If tf a b\r\n nonFunctionalIf :: tf -> a -> b -> If tf a b\r\n\r\ninstance Decide True a b where\r\n type If True a b = a\r\n nonFunctionalIf T a b = a\r\n\r\ninstance Decide False a b where\r\n type If False a b = b\r\n nonFunctionalIf F a b = b\r\n\r\nuseRank2 :: (forall a . a -> b) -> b\r\nuseRank2 f = f \"foo\"\r\n\r\nhasTrouble a = nonFunctionalIf F a (2 :: Int)\r\n-- try useRank2 hasTrouble\r\n\r\nhasNoTrouble :: a -> Int\r\nhasNoTrouble = hasTrouble\r\n-- try useRank2 hasNoTrouble\r\n}}}\r\n\r\nCertainly the program should be rejected when there is inadequate information to evaluate the type function, but it seems odd to reject {{{hasTrouble}}} and not {{{hasNoTrouble}}} given that they are equal.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4174Jumbled error message from type family operator2019-07-07T19:00:15ZlilacJumbled error message from type family operatorThe attached file produces this error message:
```
Testcase.hs:82:0:
Couldn't match expected type `True'
against inferred type `Main.R::<=:GHC6'10GHC6'8 Minor1 minor'
When generalising the type(s) for `testcase'
```
...The attached file produces this error message:
```
Testcase.hs:82:0:
Couldn't match expected type `True'
against inferred type `Main.R::<=:GHC6'10GHC6'8 Minor1 minor'
When generalising the type(s) for `testcase'
```
That should say
```
[...] against inferred type `GHC6'10 Minor1 :<=: GHC6'8 minor'
```
Apologies for the complexity of the testcase; simpler testcases seem to not reproduce the problem.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.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":"Jumbled error message from type family operator","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The attached file produces this error message:\r\n\r\n{{{\r\nTestcase.hs:82:0:\r\n Couldn't match expected type `True'\r\n against inferred type `Main.R::<=:GHC6'10GHC6'8 Minor1 minor'\r\n When generalising the type(s) for `testcase'\r\n}}}\r\n\r\nThat should say\r\n{{{\r\n[...] against inferred type `GHC6'10 Minor1 :<=: GHC6'8 minor'\r\n}}}\r\n\r\nApologies for the complexity of the testcase; simpler testcases seem to not reproduce the problem.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4120Iface type variable out of scope in cast2019-07-07T19:00:29ZbenlIface type variable out of scope in castCompiling the following module against vector-0.6 or 0.7:
```
module Thing where
import Data.Vector.Unboxed
import Data.Vector.Unboxed.Mutable as MV
thing :: Vector Int
thing = create (MV.new 5)
```
Complains about:
```
desire:tmp be...Compiling the following module against vector-0.6 or 0.7:
```
module Thing where
import Data.Vector.Unboxed
import Data.Vector.Unboxed.Mutable as MV
thing :: Vector Int
thing = create (MV.new 5)
```
Complains about:
```
desire:tmp benl$ ghc -O -c -fglasgow-exts Thing.hs -fforce-recomp
/Users/benl/.cabal/lib/vector-0.7/ghc-6.13.20100607/Data/Vector/Unboxed.hi
Declaration for create
Unfolding of Data.Vector.Unboxed.create:
Iface type variable out of scope: s
```
Looking in the interface file we have:
```
create :: forall a.
Data.Vector.Unboxed.Base.Unbox a =>
(forall s. GHC.ST.ST s (Data.Vector.Unboxed.Base.MVector s a))
-> Data.Vector.Unboxed.Base.Vector a
{- Arity: 2, Strictness: U(SA)C(U(LL)),
Inline: INLINE (sat-args=0),
Unfolding: InlineRule (1, False, False)
(\ @ a
$dUnbox :: Data.Vector.Unboxed.Base.Unbox a
eta :: forall s.
GHC.ST.ST
s
(Data.Vector.Generic.Base.Mutable
Data.Vector.Unboxed.Base.Vector s a) ->
Data.Vector.Generic.new
@ Data.Vector.Unboxed.Base.Vector
@ a
(Data.Vector.Unboxed.Base.$p1Unbox @ a $dUnbox)
(Data.Vector.Generic.New.New
@ Data.Vector.Unboxed.Base.Vector
@ a
eta))
`cast`
(forall a.
Data.Vector.Unboxed.Base.Unbox a =>
GHC.ST.ST s (Data.Vector.Unboxed.Base.TFCo:R:MutableVector s a)
-> Data.Vector.Unboxed.Base.Vector a) -}
```
The variable `s` in the right of the cast is indeed not in scope.
This prevents `create` being inlined into client modules, which kills performance for benchmarks that create lots of small vectors (like a version of quickhull in DPH).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.13 |
| 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":"Iface type variable out of scope in cast","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.13","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling the following module against vector-0.6 or 0.7:\r\n\r\n{{{\r\nmodule Thing where\r\nimport Data.Vector.Unboxed\r\nimport Data.Vector.Unboxed.Mutable\tas MV\r\n\r\nthing :: Vector Int\r\nthing = create (MV.new 5)\r\n}}}\r\n\r\nComplains about:\r\n{{{\r\ndesire:tmp benl$ ghc -O -c -fglasgow-exts Thing.hs -fforce-recomp\r\n/Users/benl/.cabal/lib/vector-0.7/ghc-6.13.20100607/Data/Vector/Unboxed.hi\r\nDeclaration for create\r\nUnfolding of Data.Vector.Unboxed.create:\r\n Iface type variable out of scope: s\r\n}}}\r\n\r\nLooking in the interface file we have:\r\n{{{\r\n create :: forall a.\r\n Data.Vector.Unboxed.Base.Unbox a =>\r\n (forall s. GHC.ST.ST s (Data.Vector.Unboxed.Base.MVector s a))\r\n -> Data.Vector.Unboxed.Base.Vector a\r\n {- Arity: 2, Strictness: U(SA)C(U(LL)),\r\n Inline: INLINE (sat-args=0),\r\n Unfolding: InlineRule (1, False, False)\r\n (\\ @ a\r\n $dUnbox :: Data.Vector.Unboxed.Base.Unbox a\r\n eta :: forall s.\r\n GHC.ST.ST\r\n s\r\n (Data.Vector.Generic.Base.Mutable\r\n Data.Vector.Unboxed.Base.Vector s a) ->\r\n Data.Vector.Generic.new\r\n @ Data.Vector.Unboxed.Base.Vector\r\n @ a\r\n (Data.Vector.Unboxed.Base.$p1Unbox @ a $dUnbox)\r\n (Data.Vector.Generic.New.New\r\n @ Data.Vector.Unboxed.Base.Vector\r\n @ a\r\n eta))\r\n `cast`\r\n (forall a.\r\n Data.Vector.Unboxed.Base.Unbox a =>\r\n GHC.ST.ST s (Data.Vector.Unboxed.Base.TFCo:R:MutableVector s a)\r\n -> Data.Vector.Unboxed.Base.Vector a) -}\r\n}}}\r\n\r\nThe variable `s` in the right of the cast is indeed not in scope.\r\n\r\nThis prevents `create` being inlined into client modules, which kills performance for benchmarks that create lots of small vectors (like a version of quickhull in DPH).","type_of_failure":"OtherFailure","blocking":[]} -->