GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-11-09T15:26:20Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/16371GHC should be more forgiving with visible dependent quantification in visible...2020-11-09T15:26:20ZRyan ScottGHC should be more forgiving with visible dependent quantification in visible type applicationsGHC HEAD currently rejects the following code:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
imp...GHC HEAD currently rejects the following code:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x -> x -> Type). Proxy a
g = f @(forall x -> x -> Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x -> x -> *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x -> x -> Type). Proxy a
|
14 | g :: forall (a :: forall x -> x -> Type). Proxy a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x -> x -> *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a -> a -> a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"GHC should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x -> x -> Type). Proxy a\r\ng = f @(forall x -> x -> Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x -> x -> *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x -> x -> Type). Proxy a\r\n |\r\n14 | g :: forall (a :: forall x -> x -> Type). Proxy a\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x -> x -> *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a -> a -> a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16232Add setField to HasField2023-11-24T09:00:48ZAdam GundryAdd setField to HasFieldThis ticket is to track the implementation of https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-record-set-field.rst as modified by https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0583-hasfiel...This ticket is to track the implementation of https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-record-set-field.rst as modified by https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0583-hasfield-redesign.rst.
The following applies to the old proposal, not all of which is relevant to the new design.
----
I've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for `HasField` be generated?
To recap, recall that at present, `HasField x r a` is coercible to `r -> a` so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.
With the proposal, `HasField x r a` will instead be represented as `r -> (a -> r, a)` where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type `data T = MkT { foo :: Int, bar :: Bool }` we need to generate
```hs
\ r x -> case r of MkT {foo = _, bar = bar} -> MkT { foo = x, bar = bar }
```
The most obvious approach is to generate well-typed Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a `HasField` constraint is solved.
Would it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the type-checker. However, this would add some overhead for every field, even if `HasField` was not subsequently used, and would require some naming scheme for update functions.
Or are there other options? Is there some way to solve a `HasField` constraint and construct its dictionary by emitting renamed syntax for subsequent type-checking, such that subsequently solving similar constraints will use the same dictionary?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.7 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | NeilMitchell, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Add setField to HasField","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["ORF"],"differentials":[],"test_case":"","architecture":"","cc":["NeilMitchell","simonpj"],"type":"FeatureRequest","description":"This ticket is to track the implementation of https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-record-set-field.rst\r\n\r\nI've made a start on the implementation but have a question on which I'd appreciate some input: how should the dictionary for `HasField` be generated?\r\n\r\nTo recap, recall that at present, `HasField x r a` is coercible to `r -> a` so the dictionary can be constructed merely by taking the selector function for the field and wrapping it in an appropriate coercion.\r\n\r\nWith the proposal, `HasField x r a` will instead be represented as `r -> (a -> r, a)` where the first component of the tuple is an update function. The problem is how to define this update function in Core. This function should perform case analysis on the record data type, where each case replaces the value of the field being updated and preserves all the other fields. For example, given a data type `data T = MkT { foo :: Int, bar :: Bool }` we need to generate\r\n{{{#!hs\r\n\\ r x -> case r of MkT {foo = _, bar = bar} -> MkT { foo = x, bar = bar }\r\n}}}\r\n\r\nThe most obvious approach is to generate well-typed Core for the update function directly, but this seems to be rather complex, in particular because of the worker/wrapper distinction, as one ends up reconstructing much of the typechecking/desugaring for record pattern matching and construction. This also seems like a lot of work to do every time a `HasField` constraint is solved.\r\n\r\nWould it be reasonable to generate update functions for fields at definition sites, as we do for selector functions? I've implemented this in the past, and it is relatively simple to generate renamed syntax to feed in to the type-checker. However, this would add some overhead for every field, even if `HasField` was not subsequently used, and would require some naming scheme for update functions.\r\n\r\nOr are there other options? Is there some way to solve a `HasField` constraint and construct its dictionary by emitting renamed syntax for subsequent type-checking, such that subsequently solving similar constraints will use the same dictionary?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16154-Wredundant-constraints: False positive2023-04-03T10:46:04ZFumiaki Kinoshita-Wredundant-constraints: False positiveGHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:
```
redundant-constraint.hs:24:1: warning: [-Wredundant-constraints]
• Redundant constraints: (KnownNat 42, Capture ...GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:
```
redundant-constraint.hs:24:1: warning: [-Wredundant-constraints]
• Redundant constraints: (KnownNat 42, Capture 42 p)
• In the type signature for:
foo :: Foo 42
|
24 | foo :: Foo 42
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.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":"-Wredundant-constraints: False positive","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:\r\n\r\n{{{\r\nredundant-constraint.hs:24:1: warning: [-Wredundant-constraints]\r\n • Redundant constraints: (KnownNat 42, Capture 42 p)\r\n • In the type signature for:\r\n foo :: Foo 42\r\n |\r\n24 | foo :: Foo 42\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16115Missing associated type instance not reported with error2020-01-23T19:38:55ZDavid FeuerMissing associated type instance not reported with errorI noticed [this SO question](https://stackoverflow.com/questions/53987924/haskell-couldnt-match-expected-type-item-nat-with-actual-type) was caused by a warning disappearing as a result of the error it caused.
```hs
{-# language TypeFam...I noticed [this SO question](https://stackoverflow.com/questions/53987924/haskell-couldnt-match-expected-type-item-nat-with-actual-type) was caused by a warning disappearing as a result of the error it caused.
```hs
{-# language TypeFamilies, DataKinds #-}
module NoWarning where
data Nat = Zero | Succ Nat deriving Show
class FromList a where
type Item a :: *
fromList :: [Item a] -> a
instance FromList Nat where
fromList [] = Zero
fromList (a:as) = Succ (fromList as :: Nat)
fish :: Nat
fish = fromList [(),(),()]
```
If you delete `fish`, you get a nice warning:
```
NoWarning.hs:8:1: warning: [-Wmissing-methods]
• No explicit associated type or default declaration for ‘Item’
• In the instance declaration for ‘FromList Nat’
|
8 | instance FromList Nat where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
But with `fish`, all you get is
```
NoWarning.hs:13:18: error:
• Couldn't match expected type ‘Item Nat’ with actual type ‘()’
• In the expression: ()
In the first argument of ‘fromList’, namely ‘[(), (), ()]’
In the expression: fromList [(), (), ()]
|
13 | fish = fromList [(),(),()]
|
```
That warning is the proper explanation of the problem, and it's just missing!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.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":"Missing associated type instance not reported with error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I noticed [https://stackoverflow.com/questions/53987924/haskell-couldnt-match-expected-type-item-nat-with-actual-type this SO question] was caused by a warning disappearing as a result of the error it caused.\r\n\r\n{{{#!hs\r\n{-# language TypeFamilies, DataKinds #-}\r\nmodule NoWarning where\r\ndata Nat = Zero | Succ Nat deriving Show\r\nclass FromList a where\r\n type Item a :: *\r\n fromList :: [Item a] -> a\r\n\r\ninstance FromList Nat where\r\n fromList [] = Zero\r\n fromList (a:as) = Succ (fromList as :: Nat)\r\n\r\nfish :: Nat\r\nfish = fromList [(),(),()]\r\n}}}\r\n\r\nIf you delete `fish`, you get a nice warning:\r\n\r\n{{{\r\nNoWarning.hs:8:1: warning: [-Wmissing-methods]\r\n • No explicit associated type or default declaration for ‘Item’\r\n • In the instance declaration for ‘FromList Nat’\r\n |\r\n8 | instance FromList Nat where\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\n}}}\r\n\r\nBut with `fish`, all you get is\r\n\r\n{{{\r\nNoWarning.hs:13:18: error:\r\n • Couldn't match expected type ‘Item Nat’ with actual type ‘()’\r\n • In the expression: ()\r\n In the first argument of ‘fromList’, namely ‘[(), (), ()]’\r\n In the expression: fromList [(), (), ()]\r\n |\r\n13 | fish = fromList [(),(),()]\r\n | \r\n}}}\r\n\r\nThat warning is the proper explanation of the problem, and it's just missing!","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15708Cross-module SPECIALZE pragmas aren't typechecked in -O02024-01-03T13:27:47ZregnatCross-module SPECIALZE pragmas aren't typechecked in -O0If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc -O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For examp...If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc -O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
-- Foo.hs
module Foo where
foo :: a -> a
foo = id
----------
-- Bar.hs
module Bar where
import Foo
{-# SPECIALIZE foo :: Int -> Bool #-}
```
running `ghc --make Bar.hs` will run fine, while `ghc --make -O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int -> Int
Actual type: Int -> Bool
• In the SPECIALISE pragma {-# SPECIALIZE foo :: Int -> Bool #-}
|
5 | {-# SPECIALIZE foo :: Int -> Bool #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Cross-module SPECIALZE pragmas aren't typechecked in -O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc -O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n-- Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a -> a\r\nfoo = id\r\n\r\n\r\n----------\r\n-- Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{-# SPECIALIZE foo :: Int -> Bool #-}\r\n}}}\r\n\r\nrunning `ghc --make Bar.hs` will run fine, while `ghc --make -O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int -> Int\r\n Actual type: Int -> Bool\r\n • In the SPECIALISE pragma {-# SPECIALIZE foo :: Int -> Bool #-}\r\n |\r\n5 | {-# SPECIALIZE foo :: Int -> Bool #-}\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15351QuantifiedConstraints ignore FunctionalDependencies2020-12-03T08:24:56ZaaronvargoQuantifiedConstraints ignore FunctionalDependenciesThe following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String
bar = show . foo
```
...The following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
bar :: (forall a. C (f a) Int) => f a -> String
bar = show . foo
```
```
• Could not deduce (Show a0) arising from a use of ‘show’
...
The type variable ‘a0’ is ambiguous
• Could not deduce (C (f a) a0) arising from a use of ‘foo’
...
The type variable ‘a0’ is ambiguous
```
Yet it ought to work, since this is perfectly fine with top-level instances:
```hs
instance C [a] Int where ...
baz :: [a] -> String
baz = show . foo
```https://gitlab.haskell.org/ghc/ghc/-/issues/15347QuantifiedConstraints: Implication constraints with type families don't work2023-04-26T13:30:31ZaaronvargoQuantifiedConstraints: Implication constraints with type families don't workThis may be related to #14860, but I think it's different.
The following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}...This may be related to #14860, but I think it's different.
The following code fails to compile:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
import Prelude()
import Data.Kind
data Dict c = c => Dict
type family F a :: Constraint
foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
```
```
• Could not deduce: F b arising from a use of ‘Dict’
from the context: (a => F b, a)
```
Yet the following all do compile:
```hs
bar :: forall a. F a => Dict (F a)
bar = Dict
baz :: forall a b. (a => b, a) => Dict b
baz = Dict
qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict
```
It seems that a wanted `F b` can be solved with a given `F b`, but not with a given `a => F b`, which is bizarre. The fact that `qux` still works is also strange, as it means that you get a different result if you first simplify by substituting `c = F b`.
As a more practical example, the following similarly fails to compile, due to the `Cod f` type family:
```hs
-- in addition to the above extensions
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
class Ob p a
class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
type Dom f
type Cod f
liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict
```
While a version which uses fundeps instead does compile:
```hs
class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f -> dom cod
liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a))
liftOb = Dict
```https://gitlab.haskell.org/ghc/ghc/-/issues/15310Derive Generic1 instances for types of kind (k -> *) -> * that include applic...2019-07-07T18:13:20ZcedricshockDerive Generic1 instances for types of kind (k -> *) -> * that include applications of the parameterThe `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k -> *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to oth...The `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k -> *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to other types.
It currently cannot derive an instance for
```hs
newtype Fix f = In (f (Fix f))
deriving (Generic1)
```
or for
```hs
data Child f = Child {
ordinal :: Int,
nickname :: f String
}
deriving (Generic1)
```
It's possible to represent these types generically, either with composition that can include occurrences of the parameter or with new types that represent applications of the parameter.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Derive Generic1 instances for types of kind (k -> *) -> * that include applications of the parameter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":["DeriveGeneric","Generic1"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k -> *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to other types.\r\n\r\nIt currently cannot derive an instance for\r\n\r\n{{{#!hs\r\nnewtype Fix f = In (f (Fix f))\r\n deriving (Generic1)\r\n}}}\r\n\r\nor for \r\n\r\n{{{#!hs\r\ndata Child f = Child {\r\n ordinal :: Int,\r\n nickname :: f String\r\n}\r\n deriving (Generic1)\r\n}}}\r\n\r\nIt's possible to represent these types generically, either with composition that can include occurrences of the parameter or with new types that represent applications of the parameter.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15043A more aggressive version of -fprint-expanded-synonyms that prints all type s...2020-01-23T19:20:59ZDomen KožarA more aggressive version of -fprint-expanded-synonyms that prints all type synonymsUsing GHC 8.2.2 and `stack build --ghc-options=-fprint-expanded-synonyms` I have the following type synonym for servant:
```hs
type Get302 (cts :: [*]) (hs :: [*]) = Verb 'GET 302 cts
(Headers (Header "Location" String ': hs) NoConten...Using GHC 8.2.2 and `stack build --ghc-options=-fprint-expanded-synonyms` I have the following type synonym for servant:
```hs
type Get302 (cts :: [*]) (hs :: [*]) = Verb 'GET 302 cts
(Headers (Header "Location" String ': hs) NoContent)
```
and get the following error message when `String` is mismatched for `Text`:
```
• Couldn't match type ‘Text’ with ‘[Char]’
Expected type: AsServerT App
:- ("login"
:> ("callback"
:> (QueryParam "code" Text
:> (QueryParam "state" Text
:> MyApp.Types.Servant.Get302
'[PlainText]
'[Header "Set-Cookie" SetCookie,
Header "Set-Cookie" SetCookie]))))
Actual type: Maybe Code
-> Maybe Text
-> App
(Headers
'[Header "Location" Text, Header "Set-Cookie" SetCookie,
Header "Set-Cookie" SetCookie]
NoContent)
```
The error is confusing as type synonym is not expanded and offending `Header` is missing from the output in the expected type.https://gitlab.haskell.org/ghc/ghc/-/issues/14968QuantifiedConstraints: Can't be RHS of type family instances2019-07-07T18:14:51ZjosefQuantifiedConstraints: Can't be RHS of type family instancesHere's a type family that I tried to write using QuantifiedConstraints.
```hs
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-...Here's a type family that I tried to write using QuantifiedConstraints.
```hs
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
module QCTypeInstance where
import GHC.Exts (Constraint)
type family Functors (fs :: [(* -> *) -> * -> *]) :: Constraint
type instance Functors '[] = (() :: Constraint)
type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
```
Unfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.
```
$ ../ghc-wip/T2893/inplace/bin/ghc-stage2 --interactive QCTypeInstance.hs
GHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted )
QCTypeInstance.hs:13:15: error:
• Illegal polymorphic type:
forall (f :: * -> *). Functor f => Functor (t f)
• In the type instance declaration for ‘Functors’
|
13 | type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
| ^^^^^^^^
```
Would it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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":"QuantifiedConstraints: Can't be RHS of type family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's a type family that I tried to write using QuantifiedConstraints.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE QuantifiedConstraints #-}\r\nmodule QCTypeInstance where\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family Functors (fs :: [(* -> *) -> * -> *]) :: Constraint\r\ntype instance Functors '[] = (() :: Constraint)\r\ntype instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)\r\n}}}\r\n\r\nUnfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.\r\n\r\n{{{\r\n$ ../ghc-wip/T2893/inplace/bin/ghc-stage2 --interactive QCTypeInstance.hs \r\nGHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted )\r\n\r\nQCTypeInstance.hs:13:15: error:\r\n • Illegal polymorphic type:\r\n forall (f :: * -> *). Functor f => Functor (t f)\r\n • In the type instance declaration for ‘Functors’\r\n |\r\n13 | type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)\r\n | ^^^^^^^^\r\n}}}\r\n\r\nWould it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14860QuantifiedConstraints: Can't quantify constraint involving type family2023-07-05T21:01:48ZRyan ScottQuantifiedConstraints: Can't quantify constraint involving type familyThis program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Undecidabl...This program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Proxy
type family Apply (f :: * -> *) a
type instance Apply Proxy a = Proxy a
data ExTyFam f where
MkExTyFam :: Apply f a -> ExTyFam f
instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
show (MkExTyFam x) = show x
showsPrec = undefined -- Not defining these leads to the oddities observed in
showList = undefined -- https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32
test :: ExTyFam Proxy -> String
test = show
```
This fails with:
```
$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:24: error:
• Could not deduce (Show (Apply f a)) arising from a use of ‘show’
from the context: forall a. Show (Apply f a)
bound by the instance declaration at Bug.hs:16:10-57
• In the expression: show x
In an equation for ‘show’: show (MkExTyFam x) = show x
In the instance declaration for ‘Show (ExTyFam f)’
|
17 | show (MkExTyFam x) = show x
| ^^^^^^
```
I would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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":"QuantifiedConstraints: Can't quantify constraint involving type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program fails to typecheck using the `wip/T2893` branch, to my surprise:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE QuantifiedConstraints #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\ntype family Apply (f :: * -> *) a\r\ntype instance Apply Proxy a = Proxy a\r\n\r\ndata ExTyFam f where\r\n MkExTyFam :: Apply f a -> ExTyFam f\r\n\r\ninstance (forall a. Show (Apply f a)) => Show (ExTyFam f) where\r\n show (MkExTyFam x) = show x\r\n showsPrec = undefined -- Not defining these leads to the oddities observed in\r\n showList = undefined -- https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32\r\n\r\ntest :: ExTyFam Proxy -> String\r\ntest = show\r\n}}}\r\n\r\nThis fails with:\r\n\r\n{{{\r\n$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:17:24: error:\r\n • Could not deduce (Show (Apply f a)) arising from a use of ‘show’\r\n from the context: forall a. Show (Apply f a)\r\n bound by the instance declaration at Bug.hs:16:10-57\r\n • In the expression: show x\r\n In an equation for ‘show’: show (MkExTyFam x) = show x\r\n In the instance declaration for ‘Show (ExTyFam f)’\r\n |\r\n17 | show (MkExTyFam x) = show x\r\n | ^^^^^^\r\n}}}\r\n\r\nI would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14795Data type return kinds don't obey the forall-or-nothing rule2022-07-13T16:54:51ZRyan ScottData type return kinds don't obey the forall-or-nothing ruleOriginally noticed [here](https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364562974). GHC accepts this:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Fo...Originally noticed [here](https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364562974). GHC accepts this:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo :: forall a. a -> b -> Type where
MkFoo :: a -> Foo a b
```
Despite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.
The users' guide doesn't explicitly indicate that the `forall`-or-nothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [inconsistent design](https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364670215), so I'm opening this ticket to track this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.2 |
| 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":"Data type return kinds don't obey the forall-or-nothing rule","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Originally noticed [https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364562974 here]. GHC accepts this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo :: forall a. a -> b -> Type where\r\n MkFoo :: a -> Foo a b\r\n}}}\r\n\r\nDespite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.\r\n\r\nThe users' guide doesn't explicitly indicate that the `forall`-or-nothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [https://github.com/ghc-proposals/ghc-proposals/pull/103#issuecomment-364670215 inconsistent design], so I'm opening this ticket to track this.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14772Keep Role Annotations in the renamed syntax tree2019-07-07T18:15:41ZlazacKeep Role Annotations in the renamed syntax treeCurrently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that...Currently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that should return the renamed annotations.
Keeping role annotations would help tooling to be consistent. For example, renaming the datatype should also rename its occurrence in the role annotation.
Minimal example:
A.hs
```hs
module A where
import B
data A x = A B
```
B.hs
```hs
module B where
import {-# SOURCE #-} A
data B = B (A ())
```
A.hs-boot
```hs
{-# LANGUAGE RoleAnnotations #-}
module A where
type role A phantom -- the role annotation is needed here
data A x
```
When inspecting the representation using the GHC API, the role is present in the parsed representation:
```
module A where -- Parsed module
type role A phantom
data A x
```
But missing from the renamed one:
```
(data A x, [import (implicit) Prelude], Nothing, Nothing) -- RenamedSource
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.2 |
| 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":"Keep Role Annotations in the renamed syntax tree","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Currently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that should return the renamed annotations.\r\n\r\nKeeping role annotations would help tooling to be consistent. For example, renaming the datatype should also rename its occurrence in the role annotation.\r\n\r\nMinimal example:\r\n\r\nA.hs\r\n{{{#!hs\r\nmodule A where\r\nimport B\r\ndata A x = A B\r\n}}}\r\n\r\nB.hs\r\n{{{#!hs\r\nmodule B where\r\nimport {-# SOURCE #-} A\r\ndata B = B (A ())\r\n}}}\r\n\r\nA.hs-boot\r\n{{{#!hs\r\n{-# LANGUAGE RoleAnnotations #-}\r\nmodule A where\r\ntype role A phantom -- the role annotation is needed here\r\ndata A x\r\n}}}\r\n\r\nWhen inspecting the representation using the GHC API, the role is present in the parsed representation:\r\n\r\n{{{\r\nmodule A where -- Parsed module\r\ntype role A phantom\r\ndata A x\r\n}}}\r\n\r\nBut missing from the renamed one:\r\n\r\n{{{\r\n(data A x, [import (implicit) Prelude], Nothing, Nothing) -- RenamedSource\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14771TypeError reported too eagerly2021-12-17T15:02:30ZSylvain HenryTypeError reported too eagerlyConsider the following example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
impor...Consider the following example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
import Data.Proxy
data DUMMY
type family If c t e where
If True t e = t
If False t e = e
type family F (n :: Nat) where
--F n = If (n <=? 8) Int (TypeError (Text "ERROR"))
F n = If (n <=? 8) Int DUMMY
test :: (F n ~ Word) => Proxy n -> Int
test _ = 2
test2 :: Proxy (n :: Nat) -> Int
test2 p = test p
main :: IO ()
main = do
print (test2 (Proxy :: Proxy 5))
```
The type error is useful:
```
Bug.hs:26:11: error:
• Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’
arising from a use of ‘test’
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
• Relevant bindings include
p :: Proxy n (bound at Bug.hs:26:7)
test2 :: Proxy n -> Int (bound at Bug.hs:26:1)
|
26 | test2 p = test p
| ^^^^^^
```
Now if we use the commented implementation of `F` (using `TypeError`), with GHC 8.2.2 and 8.0.2 we get:
```
Bug.hs:26:11: error:
• ERROR
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
|
26 | test2 p = test p
| ^^^^^^
```
While with GHC 8.0.1 we get:
```
/home/hsyl20/tmp/Bug.hs:29:11: error:
• Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’
with ‘Word’
arising from a use of ‘test’
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
```
1) Could we restore the behavior of GHC 8.0.1?
2) In my real code, when I use DUMMY I get:
```
• Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
Expected type: Word
Actual type: F n
```
If we could get the same report (mentioning the "Actual type") when we use `TypeError` that would be great.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.2 |
| 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":"TypeError reported too eagerly","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following example:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\ndata DUMMY\r\n\r\ntype family If c t e where\r\n If True t e = t\r\n If False t e = e\r\n\r\n\r\ntype family F (n :: Nat) where\r\n --F n = If (n <=? 8) Int (TypeError (Text \"ERROR\"))\r\n F n = If (n <=? 8) Int DUMMY\r\n\r\ntest :: (F n ~ Word) => Proxy n -> Int\r\ntest _ = 2\r\n\r\ntest2 :: Proxy (n :: Nat) -> Int\r\ntest2 p = test p\r\n\r\nmain :: IO ()\r\nmain = do\r\n print (test2 (Proxy :: Proxy 5))\r\n}}}\r\n\r\nThe type error is useful:\r\n{{{\r\nBug.hs:26:11: error:\r\n • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’\r\n arising from a use of ‘test’\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n • Relevant bindings include\r\n p :: Proxy n (bound at Bug.hs:26:7)\r\n test2 :: Proxy n -> Int (bound at Bug.hs:26:1)\r\n |\r\n26 | test2 p = test p\r\n | ^^^^^^\r\n}}}\r\n\r\nNow if we use the commented implementation of `F` (using `TypeError`), with GHC 8.2.2 and 8.0.2 we get:\r\n{{{\r\nBug.hs:26:11: error:\r\n • ERROR\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n |\r\n26 | test2 p = test p\r\n | ^^^^^^\r\n}}}\r\n\r\nWhile with GHC 8.0.1 we get:\r\n{{{\r\n/home/hsyl20/tmp/Bug.hs:29:11: error:\r\n • Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’\r\n with ‘Word’\r\n arising from a use of ‘test’\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n}}}\r\n\r\n1) Could we restore the behavior of GHC 8.0.1?\r\n\r\n2) In my real code, when I use DUMMY I get:\r\n{{{\r\n • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’\r\n Expected type: Word\r\n Actual type: F n\r\n}}}\r\nIf we could get the same report (mentioning the \"Actual type\") when we use `TypeError` that would be great.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14668Ordering of declarations can cause typechecking to fail2023-06-30T17:10:59ZheptahedronOrdering of declarations can cause typechecking to failThe following will successfully typecheck:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
data CInst
data G (b :: ()) = G
class C a where
type family F a
...The following will successfully typecheck:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
-- data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’
|
23 | type F' CInst (b :: F CInst) = G b
|
```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n-- data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n |\r\n23 | type F' CInst (b :: F CInst) = G b\r\n | \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14570Untouchable error arises from type equality, but not equivalent program with ...2019-07-07T18:16:28ZAlexis KingUntouchable error arises from type equality, but not equivalent program with fundepsGiven some type definitions:
```hs
data A
data B (f :: * -> *)
data X (k :: *)
```
…and this typeclass:
```hs
class C k a | k -> a
```
…these (highly contrived for the purposes of a minimal example) function definitions typecheck:
`...Given some type definitions:
```hs
data A
data B (f :: * -> *)
data X (k :: *)
```
…and this typeclass:
```hs
class C k a | k -> a
```
…these (highly contrived for the purposes of a minimal example) function definitions typecheck:
```hs
f :: forall f. (forall k. (C k (B f)) => f k) -> A
f _ = undefined
g :: (forall k. (C k (B X)) => X k) -> A
g = f
```
However, if we use a type family instead of a class with a functional dependency:
```hs
type family F (k :: *)
```
…then the equivalent function definitions fail to typecheck:
```hs
f :: forall f. (forall k. (F k ~ B f) => f k) -> A
f _ = undefined
g :: (forall k. (F k ~ B X) => X k) -> A
g = f
```
```
• Couldn't match type ‘f0’ with ‘X’
‘f0’ is untouchable
inside the constraints: F k ~ B f0
bound by a type expected by the context:
F k ~ B f0 => f0 k
Expected type: f0 k
Actual type: X k
• In the expression: f
In an equation for ‘g’: g = f
```
I read Section 5.2 of the OutsideIn(X) paper, which describes touchable and untouchable type variables, and I *sort of* understand what’s going on here. If I add an extra argument to `f` that pushes the choice of `f` outside the inner `forall`, then the program typechecks:
```hs
f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A
f _ _ = undefined
g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A
g = f
```
I don’t know if this is actually a bug—it seems entirely reasonable to me that I don’t fully understand what is going on here—but I’m stumped as to *why* GHC rejects this program but accepts the one involving functional dependencies. I would expect it to either accept or reject both programs, given they *seem* equivalent.
Is this just an unfortunate infelicity of the differences between how functional dependencies and type equalities are internally solved? Or is there a deeper difference between these two programs?
,,(Note: This ticket is adapted from [this Stack Overflow question](https://stackoverflow.com/q/47734825/465378).),,
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| 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":"Untouchable error arises from type equality, but not equivalent program with fundeps","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Given some type definitions:\r\n\r\n{{{#!hs\r\ndata A\r\ndata B (f :: * -> *)\r\ndata X (k :: *)\r\n}}}\r\n\r\n…and this typeclass:\r\n\r\n{{{#!hs\r\nclass C k a | k -> a\r\n}}}\r\n\r\n…these (highly contrived for the purposes of a minimal example) function definitions typecheck:\r\n\r\n{{{#!hs\r\nf :: forall f. (forall k. (C k (B f)) => f k) -> A\r\nf _ = undefined\r\n\r\ng :: (forall k. (C k (B X)) => X k) -> A\r\ng = f\r\n}}}\r\n\r\nHowever, if we use a type family instead of a class with a functional dependency:\r\n\r\n{{{#!hs\r\ntype family F (k :: *)\r\n}}}\r\n\r\n…then the equivalent function definitions fail to typecheck:\r\n\r\n{{{#!hs\r\nf :: forall f. (forall k. (F k ~ B f) => f k) -> A\r\nf _ = undefined\r\n\r\ng :: (forall k. (F k ~ B X) => X k) -> A\r\ng = f\r\n}}}\r\n\r\n{{{\r\n• Couldn't match type ‘f0’ with ‘X’\r\n ‘f0’ is untouchable\r\n inside the constraints: F k ~ B f0\r\n bound by a type expected by the context:\r\n F k ~ B f0 => f0 k\r\n Expected type: f0 k\r\n Actual type: X k\r\n• In the expression: f\r\n In an equation for ‘g’: g = f\r\n}}}\r\n\r\nI read Section 5.2 of the OutsideIn(X) paper, which describes touchable and untouchable type variables, and I ''sort of'' understand what’s going on here. If I add an extra argument to `f` that pushes the choice of `f` outside the inner `forall`, then the program typechecks:\r\n\r\n{{{#!hs\r\nf :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A\r\nf _ _ = undefined\r\n\r\ng :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A\r\ng = f\r\n}}}\r\n\r\nI don’t know if this is actually a bug—it seems entirely reasonable to me that I don’t fully understand what is going on here—but I’m stumped as to ''why'' GHC rejects this program but accepts the one involving functional dependencies. I would expect it to either accept or reject both programs, given they ''seem'' equivalent.\r\n\r\nIs this just an unfortunate infelicity of the differences between how functional dependencies and type equalities are internally solved? Or is there a deeper difference between these two programs?\r\n\r\n,,(Note: This ticket is adapted from [https://stackoverflow.com/q/47734825/465378 this Stack Overflow question].),,","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14478Abstract pattern synonyms (for hsig and hs-boot)2019-07-07T18:16:52ZEdward Z. YangAbstract pattern synonyms (for hsig and hs-boot)Most declaration forms (data types, values, type families, etc) support forward declaration in hs-boot/hsig files. However, pattern synonyms do not. This seems like a major omission!
Some problems to solve:
- The obvious syntax `patter...Most declaration forms (data types, values, type families, etc) support forward declaration in hs-boot/hsig files. However, pattern synonyms do not. This seems like a major omission!
Some problems to solve:
- The obvious syntax `pattern Foo :: pat_ty` is insufficient to specify whether or not a pattern is bidirectional or unidirectional. How should this be represented syntactically?
- What is the interaction with bundling? Should it be possible to export a bundle of abstract pattern synonyms, with the intent that this means an implementation must also have bundled them together
- See also #12717; abstract pattern synonym should be implementable with a plain old constructor
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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":"Abstract pattern synonyms (for hsig and hs-boot)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Most declaration forms (data types, values, type families, etc) support forward declaration in hs-boot/hsig files. However, pattern synonyms do not. This seems like a major omission!\r\n\r\nSome problems to solve:\r\n\r\n* The obvious syntax `pattern Foo :: pat_ty` is insufficient to specify whether or not a pattern is bidirectional or unidirectional. How should this be represented syntactically?\r\n* What is the interaction with bundling? Should it be possible to export a bundle of abstract pattern synonyms, with the intent that this means an implementation must also have bundled them together\r\n* See also #12717; abstract pattern synonym should be implementable with a plain old constructor","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14423{-# complete #-} should be able to handle | like {-# minimal #-}2019-07-07T18:17:05ZEdward Kmett{-# complete #-} should be able to handle | like {-# minimal #-}It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of pattern...It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns.
I have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `|` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.
Consider what happens if you add a mix of actual and smart views of a data type:
```hs
{-# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #-}
newtype Delta = Delta Int deriving (Eq,Num)
instance Monoid Delta where
mempty = 0
mappend = (+)
data Exp = Var !Int | AP !Delta !Exp !Exp | LAM !Delta !Exp
rel 0 xs = xs
rel d (AP d' l r) = AP (d + d') l r
rel d (LAM d' b) = LAM (d + d') b
rel _ (Var n) = Var n
pattern Ap a b <- AP d (rel d -> a) (rel d -> b) where
Ap a b = AP 0 a b
pattern Lam b <- LAM d (rel d -> b) where
Lam b = LAM 0 b
{-# complete Var, AP, Lam #-}
{-# complete Var, Ap, LAM #-}
{-# complete Var, AP, LAM #-}
```
Every data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.
On the other hand with `|` patterns:
```hs
{-# complete Var, (Ap | AP), (Lam | LAM) #-}
```
extends linearly.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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":"{-# complete #-} should be able to handle | like {-# minimal #-}","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It'd be really convenient to be able to specify these like we can with `minimal` pragmas, mixing ands and ors. I wind up with a combinatorial explosion of such annotations for the cases where it works when I have large numbers of patterns. \r\n\r\nI have at least one use case where something that would be a trivial pattern to express with one (complicated) expression involving `|` becomes 64 lines of complete pragmas, and every time I extend it this count doubles.\r\n\r\nConsider what happens if you add a mix of actual and smart views of a data type:\r\n\r\n{{{#!hs\r\n{-# language ViewPatterns, PatternSynonyms, GeneralizedNewtypeDeriving #-}\r\n\r\nnewtype Delta = Delta Int deriving (Eq,Num)\r\n\r\ninstance Monoid Delta where\r\n mempty = 0\r\n mappend = (+)\r\n\r\ndata Exp = Var !Int | AP !Delta !Exp !Exp | LAM !Delta !Exp\r\n\r\nrel 0 xs = xs\r\nrel d (AP d' l r) = AP (d + d') l r\r\nrel d (LAM d' b) = LAM (d + d') b\r\nrel _ (Var n) = Var n\r\n\r\npattern Ap a b <- AP d (rel d -> a) (rel d -> b) where\r\n Ap a b = AP 0 a b\r\n\r\npattern Lam b <- LAM d (rel d -> b) where\r\n Lam b = LAM 0 b\r\n\r\n{-# complete Var, AP, Lam #-}\r\n{-# complete Var, Ap, LAM #-}\r\n{-# complete Var, AP, LAM #-}\r\n}}}\r\n\r\nEvery data constructor I add with a smart view adds to the powerset of complete pragmas I should supply.\r\n\r\nOn the other hand with `|` patterns:\r\n\r\n{{{#!hs\r\n{-# complete Var, (Ap | AP), (Lam | LAM) #-}\r\n}}} \r\n\r\nextends linearly.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14422{-# complete #-} should be able to be at least partially type directed2021-09-16T13:34:34ZEdward Kmett{-# complete #-} should be able to be at least partially type directedThe fact that `{-# complete #-}` pragma that was added in #8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share...The fact that `{-# complete #-}` pragma that was added in #8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.
Say I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{-# complete (:<), Empty #-}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `-Wno-incomplete-patterns` mess I was in before.
I cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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":"{-# complete #-} should be able to be at least partially type directed","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The fact that `{-# complete #-}` pragma that was added in#8779 is tied to the set of patterns only and not the types involved can make it rather awkward or impossible to use in practice.\r\n\r\nSay I have a bunch of types that happen to share a common `(:<)` and `Empty` pattern, for views. I'd like to be able to say that for one particular type `{-# complete (:<), Empty #-}` holds, but since both aren't defined in the same module and neither one mentions my type, I'm stuck in the same `-Wno-incomplete-patterns` mess I was in before. \r\n\r\nI cant move the pragma to the individual view patterns because in general they aren't known to be a complete pattern set.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14340Rename AND typecheck types before values2019-07-07T18:17:24ZEdward Z. YangRename AND typecheck types before valuesIn a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:
- #13905 - Here, we need to determine if a Name is a newtype const...In a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:
- #13905 - Here, we need to determine if a Name is a newtype constructor or data type constructor during renaming (desugaring of applicative do), which is not known until after typechecking
- #12088 - Perhaps? We want to rename and typecheck instance declarations at the same time, since they can occur between the type declarations.
One nit: you can't compute SCCs until you rename. But if you just rename ALL of the types at once, then SCC them, that should be fine.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Task |
| 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":"Rename AND typecheck types before values","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"In a few cases, we get in trouble during renaming of values because we don't have access to information that would be computed during typechecking. Two examples of this:\r\n\r\n* https://ghc.haskell.org/trac/ghc/ticket/13905 - Here, we need to determine if a Name is a newtype constructor or data type constructor during renaming (desugaring of applicative do), which is not known until after typechecking\r\n\r\n* https://ghc.haskell.org/trac/ghc/ticket/12088 - Perhaps? We want to rename and typecheck instance declarations at the same time, since they can occur between the type declarations.\r\n\r\nOne nit: you can't compute SCCs until you rename. But if you just rename ALL of the types at once, then SCC them, that should be fine.","type_of_failure":"OtherFailure","blocking":[]} -->