GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:24:23Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/12975Suggested type signature for a pattern synonym causes program to fail to type...2019-07-07T18:24:23ZOllie CharlesSuggested type signature for a pattern synonym causes program to fail to type checkTake the following program:
```hs
{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}
import Data.Typeable
data T where
MkT :: Typeable a => a -> T
pattern Cast a <- MkT (cast -> Just a)
```
When compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`:
```
Top-level binding with no type signature:
Cast :: forall b. Typeable b => forall a. Typeable a => b -> T
```
However, using this suggested type signature causes the program to fail to type check:
```hs
• Could not deduce (Typeable a0)
arising from the "provided" constraints claimed by
the signature of ‘Cast’
from the context: Typeable a
bound by a pattern with constructor:
MkT :: forall a. Typeable a => a -> T,
in a pattern synonym declaration
at ../foo.hs:9:19-38
In other words, a successful match on the pattern
MkT (cast -> Just a)
does not provide the constraint (Typeable a0)
The type variable ‘a0’ is ambiguous
• In the declaration for pattern synonym ‘Cast’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Suggested type signature for a pattern synonym causes program to fail to type check","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["patternsynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}\r\n\r\nimport Data.Typeable\r\n\r\ndata T where\r\n MkT :: Typeable a => a -> T\r\n\r\npattern Cast a <- MkT (cast -> Just a)\r\n}}}\r\n\r\nWhen compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`:\r\n\r\n{{{\r\n Top-level binding with no type signature:\r\n Cast :: forall b. Typeable b => forall a. Typeable a => b -> T\r\n}}}\r\n\r\nHowever, using this suggested type signature causes the program to fail to type check:\r\n\r\n{{{#!hs\r\n • Could not deduce (Typeable a0)\r\n arising from the \"provided\" constraints claimed by\r\n the signature of ‘Cast’\r\n from the context: Typeable a\r\n bound by a pattern with constructor:\r\n MkT :: forall a. Typeable a => a -> T,\r\n in a pattern synonym declaration\r\n at ../foo.hs:9:19-38\r\n In other words, a successful match on the pattern\r\n MkT (cast -> Just a)\r\n does not provide the constraint (Typeable a0)\r\n The type variable ‘a0’ is ambiguous\r\n • In the declaration for pattern synonym ‘Cast’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->Take the following program:
```hs
{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}
import Data.Typeable
data T where
MkT :: Typeable a => a -> T
pattern Cast a <- MkT (cast -> Just a)
```
When compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`:
```
Top-level binding with no type signature:
Cast :: forall b. Typeable b => forall a. Typeable a => b -> T
```
However, using this suggested type signature causes the program to fail to type check:
```hs
• Could not deduce (Typeable a0)
arising from the "provided" constraints claimed by
the signature of ‘Cast’
from the context: Typeable a
bound by a pattern with constructor:
MkT :: forall a. Typeable a => a -> T,
in a pattern synonym declaration
at ../foo.hs:9:19-38
In other words, a successful match on the pattern
MkT (cast -> Just a)
does not provide the constraint (Typeable a0)
The type variable ‘a0’ is ambiguous
• In the declaration for pattern synonym ‘Cast’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Suggested type signature for a pattern synonym causes program to fail to type check","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["patternsynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}\r\n\r\nimport Data.Typeable\r\n\r\ndata T where\r\n MkT :: Typeable a => a -> T\r\n\r\npattern Cast a <- MkT (cast -> Just a)\r\n}}}\r\n\r\nWhen compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`:\r\n\r\n{{{\r\n Top-level binding with no type signature:\r\n Cast :: forall b. Typeable b => forall a. Typeable a => b -> T\r\n}}}\r\n\r\nHowever, using this suggested type signature causes the program to fail to type check:\r\n\r\n{{{#!hs\r\n • Could not deduce (Typeable a0)\r\n arising from the \"provided\" constraints claimed by\r\n the signature of ‘Cast’\r\n from the context: Typeable a\r\n bound by a pattern with constructor:\r\n MkT :: forall a. Typeable a => a -> T,\r\n in a pattern synonym declaration\r\n at ../foo.hs:9:19-38\r\n In other words, a successful match on the pattern\r\n MkT (cast -> Just a)\r\n does not provide the constraint (Typeable a0)\r\n The type variable ‘a0’ is ambiguous\r\n • In the declaration for pattern synonym ‘Cast’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12864Produce type errors after looking at whole applications2019-07-07T18:24:51ZJoachim Breitnermail@joachim-breitner.deProduce type errors after looking at whole applicationsCurrently, the type error messages we produce in case of function applications are rather dumb, in particular if arguments were ommited, added, swapped or not parenthized correctly. (Examples in the first comment below.)
In many cases a procedure like the following would be better: For a given application `f a1 a2 a3`, present the user with the (inferred) type of `f`, as well as the (expected) type `f` needs to have to be used with arguments `a1 a2 a3`. This way, only one type error will be reported per function application, instead of many, and comparing these two reported types will allow the user to spot the problem more easily.
(With „one application“ I mean `e1 e2 e3 … en` where `e1` is not of that form.)
Furthermore, once we have these two types in our hands, we can look for common patterns, and give even more helpful error messages, such as suggesting to swap two arguments.
Clearly, there are many tricky corner cases (e.g. polymorphic functions, types with constraints or type classes, type applications etc.). But that should not stop us from trying better in obvious, monomorphic cases.Currently, the type error messages we produce in case of function applications are rather dumb, in particular if arguments were ommited, added, swapped or not parenthized correctly. (Examples in the first comment below.)
In many cases a procedure like the following would be better: For a given application `f a1 a2 a3`, present the user with the (inferred) type of `f`, as well as the (expected) type `f` needs to have to be used with arguments `a1 a2 a3`. This way, only one type error will be reported per function application, instead of many, and comparing these two reported types will allow the user to spot the problem more easily.
(With „one application“ I mean `e1 e2 e3 … en` where `e1` is not of that form.)
Furthermore, once we have these two types in our hands, we can look for common patterns, and give even more helpful error messages, such as suggesting to swap two arguments.
Clearly, there are many tricky corner cases (e.g. polymorphic functions, types with constraints or type classes, type applications etc.). But that should not stop us from trying better in obvious, monomorphic cases.https://gitlab.haskell.org/ghc/ghc/-/issues/12860GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an ...2019-08-01T11:47:53ZRyan ScottGeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loopThis worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:
```hs
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Bug where
class C a b | a -> b where
c :: a -> Int
newtype Foo a = Foo a
deriving (C b)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\nmodule Bug where\r\n\r\nclass C a b | a -> b where\r\n c :: a -> Int\r\n\r\nnewtype Foo a = Foo a\r\n deriving (C b)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:
```hs
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Bug where
class C a b | a -> b where
c :: a -> Int
newtype Foo a = Foo a
deriving (C b)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"GeneralizedNewtypeDeriving + MultiParamTypeClasses sends typechecker into an infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This worked in GHC 7.6.3, but ever since GHC 7.8, this code will cause the typechecker to loop infinitely:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\nmodule Bug where\r\n\r\nclass C a b | a -> b where\r\n c :: a -> Int\r\n\r\nnewtype Foo a = Foo a\r\n deriving (C b)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12823Inconsistency in acceptance of equality constraints in different forms2019-07-07T18:25:00ZDavid FeuerInconsistency in acceptance of equality constraints in different formsCurrently, we (correctly) require a language extension to accept a declaration like
<table><tr><th>foo </th>
<td>a \~ b =\> f a -\> f b</td></tr>
<tr><td></td>
<td>foo x = x</td></tr></table>
Suppose I write
```hs
{-# LANGUAGE GADTs, UndecidableInstances, ConstraintKinds #-}
module A where
class a ~ b => Equal a b
instance a ~ b => Equal a b
type EqualS a b = a ~ b
```
and then
```hs
-- No extensions
module B where
-- This works
useEqual :: Equal a b => f a -> f b
useEqual x = x
-- But this does not
useEqualF :: EqualF a b => f a -> f b
useEqualF x = x
```
It seems that GHC expands type synonyms, but does not reduce constraints, before deciding whether enough extensions are in play to allow equality constraints. This mismatch feels weird. Is there something about `~` proper, and not `Equal`, that triggers the difficulties with let generalization? If not, I think they should either both work or both fail (probably both fail).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Inconsistency in acceptance of equality constraints in different forms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Currently, we (correctly) require a language extension to accept a declaration like\r\n\r\n foo :: a ~ b => f a -> f b\r\n foo x = x\r\n\r\nSuppose I write\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, UndecidableInstances, ConstraintKinds #-}\r\nmodule A where\r\nclass a ~ b => Equal a b\r\ninstance a ~ b => Equal a b\r\n\r\ntype EqualS a b = a ~ b\r\n}}}\r\n\r\nand then\r\n\r\n{{{#!hs\r\n-- No extensions\r\nmodule B where\r\n\r\n-- This works\r\nuseEqual :: Equal a b => f a -> f b\r\nuseEqual x = x\r\n\r\n-- But this does not\r\nuseEqualF :: EqualF a b => f a -> f b\r\nuseEqualF x = x\r\n}}}\r\n\r\nIt seems that GHC expands type synonyms, but does not reduce constraints, before deciding whether enough extensions are in play to allow equality constraints. This mismatch feels weird. Is there something about `~` proper, and not `Equal`, that triggers the difficulties with let generalization? If not, I think they should either both work or both fail (probably both fail).","type_of_failure":"OtherFailure","blocking":[]} -->Currently, we (correctly) require a language extension to accept a declaration like
<table><tr><th>foo </th>
<td>a \~ b =\> f a -\> f b</td></tr>
<tr><td></td>
<td>foo x = x</td></tr></table>
Suppose I write
```hs
{-# LANGUAGE GADTs, UndecidableInstances, ConstraintKinds #-}
module A where
class a ~ b => Equal a b
instance a ~ b => Equal a b
type EqualS a b = a ~ b
```
and then
```hs
-- No extensions
module B where
-- This works
useEqual :: Equal a b => f a -> f b
useEqual x = x
-- But this does not
useEqualF :: EqualF a b => f a -> f b
useEqualF x = x
```
It seems that GHC expands type synonyms, but does not reduce constraints, before deciding whether enough extensions are in play to allow equality constraints. This mismatch feels weird. Is there something about `~` proper, and not `Equal`, that triggers the difficulties with let generalization? If not, I think they should either both work or both fail (probably both fail).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Inconsistency in acceptance of equality constraints in different forms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Currently, we (correctly) require a language extension to accept a declaration like\r\n\r\n foo :: a ~ b => f a -> f b\r\n foo x = x\r\n\r\nSuppose I write\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, UndecidableInstances, ConstraintKinds #-}\r\nmodule A where\r\nclass a ~ b => Equal a b\r\ninstance a ~ b => Equal a b\r\n\r\ntype EqualS a b = a ~ b\r\n}}}\r\n\r\nand then\r\n\r\n{{{#!hs\r\n-- No extensions\r\nmodule B where\r\n\r\n-- This works\r\nuseEqual :: Equal a b => f a -> f b\r\nuseEqual x = x\r\n\r\n-- But this does not\r\nuseEqualF :: EqualF a b => f a -> f b\r\nuseEqualF x = x\r\n}}}\r\n\r\nIt seems that GHC expands type synonyms, but does not reduce constraints, before deciding whether enough extensions are in play to allow equality constraints. This mismatch feels weird. Is there something about `~` proper, and not `Equal`, that triggers the difficulties with let generalization? If not, I think they should either both work or both fail (probably both fail).","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12820Regression around pattern synonyms and higher-rank types2019-07-07T18:25:01ZRichard Eisenbergrae@richarde.devRegression around pattern synonyms and higher-rank typesGHC 8.0.1 accepts, but HEAD rejects:
```hs
{-# LANGUAGE PatternSynonyms, RankNTypes, ViewPatterns #-}
module Bug where
pattern P :: (forall a. a -> a) -> String
pattern P x <- (\ _ -> id -> x)
```
(Sidenote: kudos to the parser on figuring out my view pattern.)
HEAD gives this error:
```
Bug.hs:6:30: error:
• Couldn't match expected type ‘forall a. a -> a’
with actual type ‘a0 -> a0’
• In the declaration for pattern synonym ‘P’
• Relevant bindings include x :: a0 -> a0 (bound at Bug.hs:6:30)
```
The code looks correct to me.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Regression around pattern synonyms and higher-rank types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.0.1 accepts, but HEAD rejects:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PatternSynonyms, RankNTypes, ViewPatterns #-}\r\n\r\nmodule Bug where\r\n\r\npattern P :: (forall a. a -> a) -> String\r\npattern P x <- (\\ _ -> id -> x)\r\n}}}\r\n\r\n(Sidenote: kudos to the parser on figuring out my view pattern.)\r\n\r\nHEAD gives this error:\r\n\r\n{{{\r\nBug.hs:6:30: error:\r\n • Couldn't match expected type ‘forall a. a -> a’\r\n with actual type ‘a0 -> a0’\r\n • In the declaration for pattern synonym ‘P’\r\n • Relevant bindings include x :: a0 -> a0 (bound at Bug.hs:6:30)\r\n}}}\r\n\r\nThe code looks correct to me.","type_of_failure":"OtherFailure","blocking":[]} -->GHC 8.0.1 accepts, but HEAD rejects:
```hs
{-# LANGUAGE PatternSynonyms, RankNTypes, ViewPatterns #-}
module Bug where
pattern P :: (forall a. a -> a) -> String
pattern P x <- (\ _ -> id -> x)
```
(Sidenote: kudos to the parser on figuring out my view pattern.)
HEAD gives this error:
```
Bug.hs:6:30: error:
• Couldn't match expected type ‘forall a. a -> a’
with actual type ‘a0 -> a0’
• In the declaration for pattern synonym ‘P’
• Relevant bindings include x :: a0 -> a0 (bound at Bug.hs:6:30)
```
The code looks correct to me.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Regression around pattern synonyms and higher-rank types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.0.1 accepts, but HEAD rejects:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PatternSynonyms, RankNTypes, ViewPatterns #-}\r\n\r\nmodule Bug where\r\n\r\npattern P :: (forall a. a -> a) -> String\r\npattern P x <- (\\ _ -> id -> x)\r\n}}}\r\n\r\n(Sidenote: kudos to the parser on figuring out my view pattern.)\r\n\r\nHEAD gives this error:\r\n\r\n{{{\r\nBug.hs:6:30: error:\r\n • Couldn't match expected type ‘forall a. a -> a’\r\n with actual type ‘a0 -> a0’\r\n • In the declaration for pattern synonym ‘P’\r\n • Relevant bindings include x :: a0 -> a0 (bound at Bug.hs:6:30)\r\n}}}\r\n\r\nThe code looks correct to me.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12717Permit data types in signatures to be implemented with equivalent pattern syn...2019-07-07T18:25:26ZEdward Z. YangPermit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)Suppose I write in a signature:
```
data Type = TArrow t1 t2 | TApp String [Type]
```
But it turns out that the real data type only has TApp (and uses "-\>" as the TyCon for TArrow). It would be nice if a pattern synonym could be used to implement this "concrete abstract data type" instead. Signature matching would have to typecheck the pattern synonyms against each other, and also check for totality. Note that in this example, App would need a guard against the Arrow case; otherwise the patterns overlap, whereas in the data type above it shouldn't matter what order the patterns go in.
The converse might be useful too:
```
data Type
pattern TArrow :: Type -> Type -> Type
pattern TInt :: Type
```
These patterns would be available for matching, with the assumption that they weren't total. If they were implemented directly using constructors, that should not be a problem. (In fact, do we even support abstract pattern synonyms?)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Suppose I write in a signature:\r\n\r\n{{{\r\ndata Type = TArrow t1 t2 | TApp String [Type]\r\n}}}\r\n\r\nBut it turns out that the real data type only has TApp (and uses \"->\" as the TyCon for TArrow). It would be nice if a pattern synonym could be used to implement this \"concrete abstract data type\" instead. Signature matching would have to typecheck the pattern synonyms against each other, and also check for totality. Note that in this example, App would need a guard against the Arrow case; otherwise the patterns overlap, whereas in the data type above it shouldn't matter what order the patterns go in.\r\n\r\nThe converse might be useful too:\r\n\r\n{{{\r\ndata Type\r\npattern TArrow :: Type -> Type -> Type\r\npattern TInt :: Type\r\n}}}\r\n\r\nThese patterns would be available for matching, with the assumption that they weren't total. If they were implemented directly using constructors, that should not be a problem. (In fact, do we even support abstract pattern synonyms?)","type_of_failure":"OtherFailure","blocking":[]} -->Suppose I write in a signature:
```
data Type = TArrow t1 t2 | TApp String [Type]
```
But it turns out that the real data type only has TApp (and uses "-\>" as the TyCon for TArrow). It would be nice if a pattern synonym could be used to implement this "concrete abstract data type" instead. Signature matching would have to typecheck the pattern synonyms against each other, and also check for totality. Note that in this example, App would need a guard against the Arrow case; otherwise the patterns overlap, whereas in the data type above it shouldn't matter what order the patterns go in.
The converse might be useful too:
```
data Type
pattern TArrow :: Type -> Type -> Type
pattern TInt :: Type
```
These patterns would be available for matching, with the assumption that they weren't total. If they were implemented directly using constructors, that should not be a problem. (In fact, do we even support abstract pattern synonyms?)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Permit data types in signatures to be implemented with equivalent pattern synonyms (and vice versa)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Suppose I write in a signature:\r\n\r\n{{{\r\ndata Type = TArrow t1 t2 | TApp String [Type]\r\n}}}\r\n\r\nBut it turns out that the real data type only has TApp (and uses \"->\" as the TyCon for TArrow). It would be nice if a pattern synonym could be used to implement this \"concrete abstract data type\" instead. Signature matching would have to typecheck the pattern synonyms against each other, and also check for totality. Note that in this example, App would need a guard against the Arrow case; otherwise the patterns overlap, whereas in the data type above it shouldn't matter what order the patterns go in.\r\n\r\nThe converse might be useful too:\r\n\r\n{{{\r\ndata Type\r\npattern TArrow :: Type -> Type -> Type\r\npattern TInt :: Type\r\n}}}\r\n\r\nThese patterns would be available for matching, with the assumption that they weren't total. If they were implemented directly using constructors, that should not be a problem. (In fact, do we even support abstract pattern synonyms?)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12705Renamer should reject signatures that reexport only part of a declaration2019-07-07T18:25:29ZEdward Z. YangRenamer should reject signatures that reexport only part of a declarationThe following signature is bogus, and also, unfortunately, accepted by GHC at the moment:
```
signature A(f) where
data T = MkT { f :: Bool }
```
This doesn't make any sense at all. We should reject it early. It can lead to very strange errors (see bkpreex05 in tree) but happily it is fairly easy to avoid.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| 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":"Renamer should reject signatures that reexport only part of a declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following signature is bogus, and also, unfortunately, accepted by GHC at the moment:\r\n\r\n{{{\r\nsignature A(f) where\r\ndata T = MkT { f :: Bool }\r\n}}}\r\n\r\nThis doesn't make any sense at all. We should reject it early. It can lead to very strange errors (see bkpreex05 in tree) but happily it is fairly easy to avoid.","type_of_failure":"OtherFailure","blocking":[]} -->The following signature is bogus, and also, unfortunately, accepted by GHC at the moment:
```
signature A(f) where
data T = MkT { f :: Bool }
```
This doesn't make any sense at all. We should reject it early. It can lead to very strange errors (see bkpreex05 in tree) but happily it is fairly easy to avoid.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| 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":"Renamer should reject signatures that reexport only part of a declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following signature is bogus, and also, unfortunately, accepted by GHC at the moment:\r\n\r\n{{{\r\nsignature A(f) where\r\ndata T = MkT { f :: Bool }\r\n}}}\r\n\r\nThis doesn't make any sense at all. We should reject it early. It can lead to very strange errors (see bkpreex05 in tree) but happily it is fairly easy to avoid.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12704Check if constraint synonym satisfies functional dependencies2019-07-07T18:25:29ZEdward Z. YangCheck if constraint synonym satisfies functional dependenciesWhen we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:
```
signature H where
class F a b | a -> b
-- This should be an invalid implementation
module H where
type F a b = (Eq a, Eq b)
```
The check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| 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":"Check if constraint synonym satisfies functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:\r\n\r\n{{{\r\nsignature H where\r\n class F a b | a -> b\r\n\r\n-- This should be an invalid implementation\r\nmodule H where\r\n type F a b = (Eq a, Eq b)\r\n}}}\r\n\r\nThe check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.","type_of_failure":"OtherFailure","blocking":[]} -->When we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:
```
signature H where
class F a b | a -> b
-- This should be an invalid implementation
module H where
type F a b = (Eq a, Eq b)
```
The check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| 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":"Check if constraint synonym satisfies functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When we resolve #12679, it will be possible to implement an abstract type class using a constraint synonym. However, in my implementation, I didn't implement functional dependency checking:\r\n\r\n{{{\r\nsignature H where\r\n class F a b | a -> b\r\n\r\n-- This should be an invalid implementation\r\nmodule H where\r\n type F a b = (Eq a, Eq b)\r\n}}}\r\n\r\nThe check is annoying fiddly: we have to descend into the constraint synonym, collect all the implied fundeps, and then see if we have the ones we need, so I didn't implement it. Maybe some time.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12703Expand Backpack's signature matching relation beyond definitional equality2019-07-07T18:25:29ZEdward Z. YangExpand Backpack's signature matching relation beyond definitional equalityCurrently, signature matching is done by strict definitional equality. This can be pretty inconvenient in some cases (it is also the only place in the Haskell language that we actually expose definitional equality):
- \*Polymorphism.\*\* This is the obvious one. If I have an implementing function that is more polymorphic than my signature, I have to manually monomorphize it.
```
unit p where
signature H where
import Prelude (Int)
data String
length :: String -> Int
unit q where
module H(String, length) where
-- from Prelude
unit r where
dependency p[H=q:H]
```
Gives
```
<no location info>: error:
Identifier ‘Data.Foldable.length’ has conflicting definitions in the module
and its hsig file
Main module: Data.Foldable.length ::
Data.Foldable.Foldable t => forall a. t a -> GHC.Types.Int
Hsig file: Data.Foldable.length ::
GHC.Base.String -> GHC.Types.Int
The two types are different
```
Essentially, you have to monomorphize any functions you want to use. Annoying!
One particular place this shows up is if you're incrementally Backpack'ing an interface that has an existing type class. In this case, you might like to just reexport the methods of the type class and "fill" the imports; but these methods have the wrong types! (They're not monomorphic enough).
- \*Quantifier ordering.\*\* Here's a more subtle one: if I don't explicitly specify a type signature, GHC will pick whatever quantifier ordering it wants. Quantifier ordering affects definitional equality.
It's actually pretty easy to trigger this, since GHC seems to always pick the reverse of what you'd get if you explicitly specified the type signature:
```
unit p where
signature H where
k :: a -> b -> a
unit q where
module H where
k x y = x
unit r where
dependency p[H=q:H]
```
Fails with:
```
q.bkp:7:9: error:
Identifier ‘q:H.k’ has conflicting definitions in the module
and its hsig file
Main module: q:H.k :: t2 -> t1 -> t2
Hsig file: q:H.k :: a -> b -> a
The two types are different
```
- \*Constraint relaxation.\*\* In #12679, you might want to define an abstract class which you can use to let implementors pass in type class instances that they might need. But you often end up in situations where the real implementations of your functions require less constraint than the signature specifies; for example, you might write `insert :: Key k => k -> a -> Map k a -> Map k a`, but if Map is an association list and just appends the new value onto the front of the list, no Eq constraint needed! There goes another impedance matching binding.
- \*Type families.\*\* Type family applications aren't reduced when deciding definitional equality.
```
{-# LANGUAGE TypeFamilies #-}
unit p where
signature H where
f :: Int
unit q where
module H where
type family F
type instance F = Int
f :: F
f = 2
unit r where
dependency p[H=q:H]
```
Gives
```
q.bkp:11:9: error:
Identifier ‘q:H.f’ has conflicting definitions in the module
and its hsig file
Main module: q:H.f :: q:H.F
Hsig file: q:H.f :: GHC.Types.Int
The two types are different
```
- \*Discussion.\*\* It's instructive to consider what the impacts of this sort of relaxation would have on hs-boot files. Some of the equalities that users expect in the source language have operational impact: for example, the ordering of constraints affects the calling convention of the function in question. So there would need to be an impedance matching binding to reorder/drop constraints to match the defining function. We already do an impedance matching of this sort with dictionary functions; this would be a logical extension. Thus, a signature would have to monomorphize, coerce, etc--whatever it needs to show the matching holds. I think this is quite plausible, although it would require rewriting this chunk of code.Currently, signature matching is done by strict definitional equality. This can be pretty inconvenient in some cases (it is also the only place in the Haskell language that we actually expose definitional equality):
- \*Polymorphism.\*\* This is the obvious one. If I have an implementing function that is more polymorphic than my signature, I have to manually monomorphize it.
```
unit p where
signature H where
import Prelude (Int)
data String
length :: String -> Int
unit q where
module H(String, length) where
-- from Prelude
unit r where
dependency p[H=q:H]
```
Gives
```
<no location info>: error:
Identifier ‘Data.Foldable.length’ has conflicting definitions in the module
and its hsig file
Main module: Data.Foldable.length ::
Data.Foldable.Foldable t => forall a. t a -> GHC.Types.Int
Hsig file: Data.Foldable.length ::
GHC.Base.String -> GHC.Types.Int
The two types are different
```
Essentially, you have to monomorphize any functions you want to use. Annoying!
One particular place this shows up is if you're incrementally Backpack'ing an interface that has an existing type class. In this case, you might like to just reexport the methods of the type class and "fill" the imports; but these methods have the wrong types! (They're not monomorphic enough).
- \*Quantifier ordering.\*\* Here's a more subtle one: if I don't explicitly specify a type signature, GHC will pick whatever quantifier ordering it wants. Quantifier ordering affects definitional equality.
It's actually pretty easy to trigger this, since GHC seems to always pick the reverse of what you'd get if you explicitly specified the type signature:
```
unit p where
signature H where
k :: a -> b -> a
unit q where
module H where
k x y = x
unit r where
dependency p[H=q:H]
```
Fails with:
```
q.bkp:7:9: error:
Identifier ‘q:H.k’ has conflicting definitions in the module
and its hsig file
Main module: q:H.k :: t2 -> t1 -> t2
Hsig file: q:H.k :: a -> b -> a
The two types are different
```
- \*Constraint relaxation.\*\* In #12679, you might want to define an abstract class which you can use to let implementors pass in type class instances that they might need. But you often end up in situations where the real implementations of your functions require less constraint than the signature specifies; for example, you might write `insert :: Key k => k -> a -> Map k a -> Map k a`, but if Map is an association list and just appends the new value onto the front of the list, no Eq constraint needed! There goes another impedance matching binding.
- \*Type families.\*\* Type family applications aren't reduced when deciding definitional equality.
```
{-# LANGUAGE TypeFamilies #-}
unit p where
signature H where
f :: Int
unit q where
module H where
type family F
type instance F = Int
f :: F
f = 2
unit r where
dependency p[H=q:H]
```
Gives
```
q.bkp:11:9: error:
Identifier ‘q:H.f’ has conflicting definitions in the module
and its hsig file
Main module: q:H.f :: q:H.F
Hsig file: q:H.f :: GHC.Types.Int
The two types are different
```
- \*Discussion.\*\* It's instructive to consider what the impacts of this sort of relaxation would have on hs-boot files. Some of the equalities that users expect in the source language have operational impact: for example, the ordering of constraints affects the calling convention of the function in question. So there would need to be an impedance matching binding to reorder/drop constraints to match the defining function. We already do an impedance matching of this sort with dictionary functions; this would be a logical extension. Thus, a signature would have to monomorphize, coerce, etc--whatever it needs to show the matching holds. I think this is quite plausible, although it would require rewriting this chunk of code.John EricsonJohn Ericsonhttps://gitlab.haskell.org/ghc/ghc/-/issues/12694GHC HEAD no longer reports inaccessible code2019-07-07T18:25:33ZEdward Z. YangGHC HEAD no longer reports inaccessible codeGiven this A.hs:
```
{-# LANGUAGE GADTs #-}
module A where
f :: Bool ~ Int => a -> b
f x = x
```
I get:
```
ezyang@sabre:~$ ghc-head --version
The Glorious Glasgow Haskell Compilation System, version 8.1.20161010
ezyang@sabre:~$ ghc-head --make A.hs
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:4:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f’: f x = ...
```
In contrast:
```
ezyang@sabre:~$ ghc-8.0 --make A.hs
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:3:6: error:
• Couldn't match type ‘Bool’ with ‘Int’
Inaccessible code in
the type signature for:
f :: Bool ~ Int => a -> b
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: Bool ~ Int => a -> b
```
Is this expected? I'd expect at least a warning!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD no longer reports inaccessible code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Given this A.hs:\r\n\r\n{{{\r\n{-# LANGUAGE GADTs #-}\r\nmodule A where\r\nf :: Bool ~ Int => a -> b\r\nf x = x\r\n}}}\r\n\r\nI get:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-head --version\r\nThe Glorious Glasgow Haskell Compilation System, version 8.1.20161010\r\nezyang@sabre:~$ ghc-head --make A.hs \r\n[1 of 1] Compiling A ( A.hs, A.o )\r\n\r\nA.hs:4:1: warning: [-Woverlapping-patterns]\r\n Pattern match is redundant\r\n In an equation for ‘f’: f x = ...\r\n}}}\r\n\r\nIn contrast:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --make A.hs \r\n[1 of 1] Compiling A ( A.hs, A.o )\r\n\r\nA.hs:3:6: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Inaccessible code in\r\n the type signature for:\r\n f :: Bool ~ Int => a -> b\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: Bool ~ Int => a -> b\r\n}}}\r\n\r\nIs this expected? I'd expect at least a warning!","type_of_failure":"OtherFailure","blocking":[]} -->Given this A.hs:
```
{-# LANGUAGE GADTs #-}
module A where
f :: Bool ~ Int => a -> b
f x = x
```
I get:
```
ezyang@sabre:~$ ghc-head --version
The Glorious Glasgow Haskell Compilation System, version 8.1.20161010
ezyang@sabre:~$ ghc-head --make A.hs
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:4:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘f’: f x = ...
```
In contrast:
```
ezyang@sabre:~$ ghc-8.0 --make A.hs
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:3:6: error:
• Couldn't match type ‘Bool’ with ‘Int’
Inaccessible code in
the type signature for:
f :: Bool ~ Int => a -> b
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: Bool ~ Int => a -> b
```
Is this expected? I'd expect at least a warning!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD no longer reports inaccessible code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Given this A.hs:\r\n\r\n{{{\r\n{-# LANGUAGE GADTs #-}\r\nmodule A where\r\nf :: Bool ~ Int => a -> b\r\nf x = x\r\n}}}\r\n\r\nI get:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-head --version\r\nThe Glorious Glasgow Haskell Compilation System, version 8.1.20161010\r\nezyang@sabre:~$ ghc-head --make A.hs \r\n[1 of 1] Compiling A ( A.hs, A.o )\r\n\r\nA.hs:4:1: warning: [-Woverlapping-patterns]\r\n Pattern match is redundant\r\n In an equation for ‘f’: f x = ...\r\n}}}\r\n\r\nIn contrast:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --make A.hs \r\n[1 of 1] Compiling A ( A.hs, A.o )\r\n\r\nA.hs:3:6: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Inaccessible code in\r\n the type signature for:\r\n f :: Bool ~ Int => a -> b\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: Bool ~ Int => a -> b\r\n}}}\r\n\r\nIs this expected? I'd expect at least a warning!","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12680Permit type equality instances in signatures2019-11-26T18:32:56ZEdward Z. YangPermit type equality instances in signaturesDavid Christiansen requested this, and I want to record it so I don't forget. What he wants to be able to do is say things like this in signatures:
```
signature A where
data T
data S
type family F a
instance T ~ S
instance F Int ~ S
```
This is currently rejected by GHC because you are not allowed to define instances of type equality. But really all this is saying is that the type equality must hold when we eventually implement the module; easy to check.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"Permit type equality instances in signatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"David Christiansen requested this, and I want to record it so I don't forget. What he wants to be able to do is say things like this in signatures:\r\n\r\n{{{\r\nsignature A where\r\n\r\ndata T\r\ndata S\r\ntype family F a\r\n\r\ninstance T ~ S\r\ninstance F Int ~ S\r\n}}}\r\n\r\nThis is currently rejected by GHC because you are not allowed to define instances of type equality. But really all this is saying is that the type equality must hold when we eventually implement the module; easy to check.","type_of_failure":"OtherFailure","blocking":[]} -->David Christiansen requested this, and I want to record it so I don't forget. What he wants to be able to do is say things like this in signatures:
```
signature A where
data T
data S
type family F a
instance T ~ S
instance F Int ~ S
```
This is currently rejected by GHC because you are not allowed to define instances of type equality. But really all this is saying is that the type equality must hold when we eventually implement the module; easy to check.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"Permit type equality instances in signatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"David Christiansen requested this, and I want to record it so I don't forget. What he wants to be able to do is say things like this in signatures:\r\n\r\n{{{\r\nsignature A where\r\n\r\ndata T\r\ndata S\r\ntype family F a\r\n\r\ninstance T ~ S\r\ninstance F Int ~ S\r\n}}}\r\n\r\nThis is currently rejected by GHC because you are not allowed to define instances of type equality. But really all this is saying is that the type equality must hold when we eventually implement the module; easy to check.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12652Type checker no longer accepting code using function composition and rank-n t...2021-07-11T13:33:45ZEdward Z. YangType checker no longer accepting code using function composition and rank-n typesThe following program (reduced from Cabal code that uses HasCallStack) typechecks in GHC 8.0, but not on HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImplicitParams #-}
module Foo where
type T a = (?x :: Int) => a
type M a = T (IO a)
f :: T (T a -> a)
f x = x
g :: Int -> M ()
g = undefined
h :: Int -> M ()
-- h x = f (g x) -- works on HEAD
h = f . g -- fails on HEAD, works on GHC 8.0
```
It's possible that this is just fall out from the recent impredicativity changes but I just wanted to make sure that this was on purpose.The following program (reduced from Cabal code that uses HasCallStack) typechecks in GHC 8.0, but not on HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImplicitParams #-}
module Foo where
type T a = (?x :: Int) => a
type M a = T (IO a)
f :: T (T a -> a)
f x = x
g :: Int -> M ()
g = undefined
h :: Int -> M ()
-- h x = f (g x) -- works on HEAD
h = f . g -- fails on HEAD, works on GHC 8.0
```
It's possible that this is just fall out from the recent impredicativity changes but I just wanted to make sure that this was on purpose.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/12639Inconsistent treatment of FlexibleInstances and MPTCs with standard vs. flexi...2019-07-07T18:25:44ZDavid FeuerInconsistent treatment of FlexibleInstances and MPTCs with standard vs. flexible derivingGiven `{-# LANGUAGE GeneralizedNewtypeDeriving #-}`, I can write
```hs
import Control.Monad.State.Strict
newtype Foo s m a = Foo (StateT s m a)
deriving (Functor, Applicative, Monad, MonadState s)
```
However, if I want to use `StandaloneDeriving` to make the `MonadState` instance more explicit,
```hs
deriving instance Monad m => MonadState s (Foo s m)
```
I suddenly need to add `FlexibleInstances` and `MultiParamTypeClasses`.
In my personal opinion, the most sensible way to handle this is to change two things in two different directions:
1. Allow MPTC instance declarations (but not class declarations) without `MultiParamTypeClasses`.
1. Require `FlexibleInstances` for standard deriving clauses when they would be required for standalone deriving declarations.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Inconsistent treatment of FlexibleInstances and MPTCs with standard vs. flexible deriving","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Given `{-# LANGUAGE GeneralizedNewtypeDeriving #-}`, I can write\r\n\r\n{{{#!hs\r\nimport Control.Monad.State.Strict\r\n\r\nnewtype Foo s m a = Foo (StateT s m a)\r\n deriving (Functor, Applicative, Monad, MonadState s)\r\n}}}\r\n\r\nHowever, if I want to use `StandaloneDeriving` to make the `MonadState` instance more explicit,\r\n\r\n{{{#!hs\r\nderiving instance Monad m => MonadState s (Foo s m)\r\n}}}\r\n\r\nI suddenly need to add `FlexibleInstances` and `MultiParamTypeClasses`.\r\n\r\nIn my personal opinion, the most sensible way to handle this is to change two things in two different directions:\r\n\r\n1. Allow MPTC instance declarations (but not class declarations) without `MultiParamTypeClasses`.\r\n\r\n2. Require `FlexibleInstances` for standard deriving clauses when they would be required for standalone deriving declarations.","type_of_failure":"OtherFailure","blocking":[]} -->Given `{-# LANGUAGE GeneralizedNewtypeDeriving #-}`, I can write
```hs
import Control.Monad.State.Strict
newtype Foo s m a = Foo (StateT s m a)
deriving (Functor, Applicative, Monad, MonadState s)
```
However, if I want to use `StandaloneDeriving` to make the `MonadState` instance more explicit,
```hs
deriving instance Monad m => MonadState s (Foo s m)
```
I suddenly need to add `FlexibleInstances` and `MultiParamTypeClasses`.
In my personal opinion, the most sensible way to handle this is to change two things in two different directions:
1. Allow MPTC instance declarations (but not class declarations) without `MultiParamTypeClasses`.
1. Require `FlexibleInstances` for standard deriving clauses when they would be required for standalone deriving declarations.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Inconsistent treatment of FlexibleInstances and MPTCs with standard vs. flexible deriving","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Given `{-# LANGUAGE GeneralizedNewtypeDeriving #-}`, I can write\r\n\r\n{{{#!hs\r\nimport Control.Monad.State.Strict\r\n\r\nnewtype Foo s m a = Foo (StateT s m a)\r\n deriving (Functor, Applicative, Monad, MonadState s)\r\n}}}\r\n\r\nHowever, if I want to use `StandaloneDeriving` to make the `MonadState` instance more explicit,\r\n\r\n{{{#!hs\r\nderiving instance Monad m => MonadState s (Foo s m)\r\n}}}\r\n\r\nI suddenly need to add `FlexibleInstances` and `MultiParamTypeClasses`.\r\n\r\nIn my personal opinion, the most sensible way to handle this is to change two things in two different directions:\r\n\r\n1. Allow MPTC instance declarations (but not class declarations) without `MultiParamTypeClasses`.\r\n\r\n2. Require `FlexibleInstances` for standard deriving clauses when they would be required for standalone deriving declarations.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12580Eagerly simplify inherently-coherent instances2019-07-07T18:25:59ZDavid FeuerEagerly simplify inherently-coherent instances[https://downloads.haskell.org/\~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/src/TysPrim.html](https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/src/TysPrim.html) explains that `~~` and `~` are "inherently coherent", so GHC can reduce them immediately to their constraints. It seems to me that certain user-written classes can also be seen to be inherently coherent in this fashion. Specifically, given
```hs
class constraintC => C a1 a2 ...
instance constraintI => C a1 a2 ...
```
where `a1`, `a2`, etc., are type variables, `C` is inherently coherent if both of the following hold:
1. `C` has no methods whatsoever.
1. `constraintC` entails `constraintI` (so the constraints are effectively identical).
I believe in these cases GHC can and probably should reduce `C a1 a2` immediately to `constraintC`. Condition (2) is more general that we really need; in realistic cases, the constraints will be identical up to alpha renaming because most people don't write obfuscated code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Eagerly simplify inherently-coherent instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"[https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/src/TysPrim.html] explains that `~~` and `~` are \"inherently coherent\", so GHC can reduce them immediately to their constraints. It seems to me that certain user-written classes can also be seen to be inherently coherent in this fashion. Specifically, given\r\n\r\n{{{#!hs\r\nclass constraintC => C a1 a2 ...\r\ninstance constraintI => C a1 a2 ...\r\n}}}\r\n\r\nwhere `a1`, `a2`, etc., are type variables, `C` is inherently coherent if both of the following hold:\r\n\r\n1. `C` has no methods whatsoever.\r\n\r\n2. `constraintC` entails `constraintI` (so the constraints are effectively identical).\r\n\r\nI believe in these cases GHC can and probably should reduce `C a1 a2` immediately to `constraintC`. Condition (2) is more general that we really need; in realistic cases, the constraints will be identical up to alpha renaming because most people don't write obfuscated code.","type_of_failure":"OtherFailure","blocking":[]} -->[https://downloads.haskell.org/\~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/src/TysPrim.html](https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/src/TysPrim.html) explains that `~~` and `~` are "inherently coherent", so GHC can reduce them immediately to their constraints. It seems to me that certain user-written classes can also be seen to be inherently coherent in this fashion. Specifically, given
```hs
class constraintC => C a1 a2 ...
instance constraintI => C a1 a2 ...
```
where `a1`, `a2`, etc., are type variables, `C` is inherently coherent if both of the following hold:
1. `C` has no methods whatsoever.
1. `constraintC` entails `constraintI` (so the constraints are effectively identical).
I believe in these cases GHC can and probably should reduce `C a1 a2` immediately to `constraintC`. Condition (2) is more general that we really need; in realistic cases, the constraints will be identical up to alpha renaming because most people don't write obfuscated code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Eagerly simplify inherently-coherent instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"[https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/src/TysPrim.html] explains that `~~` and `~` are \"inherently coherent\", so GHC can reduce them immediately to their constraints. It seems to me that certain user-written classes can also be seen to be inherently coherent in this fashion. Specifically, given\r\n\r\n{{{#!hs\r\nclass constraintC => C a1 a2 ...\r\ninstance constraintI => C a1 a2 ...\r\n}}}\r\n\r\nwhere `a1`, `a2`, etc., are type variables, `C` is inherently coherent if both of the following hold:\r\n\r\n1. `C` has no methods whatsoever.\r\n\r\n2. `constraintC` entails `constraintI` (so the constraints are effectively identical).\r\n\r\nI believe in these cases GHC can and probably should reduce `C a1 a2` immediately to `constraintC`. Condition (2) is more general that we really need; in realistic cases, the constraints will be identical up to alpha renaming because most people don't write obfuscated code.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12569TypeApplications allows instantiation of implicitly-quantified kind variables2019-07-07T18:26:02ZAlexey VagarenkoTypeApplications allows instantiation of implicitly-quantified kind variablesTypeApplications doesn't allow unticked list constructor even when it is unambiguous:
```
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
> :set -XDataKinds
> :set -XTypeApplications
> :set -XScopedTypeVariables
> :set -XKindSignatures
> let foo :: forall (xs :: [Nat]). (); foo = ()
> foo @'[0]
()
> foo @[0]
<interactive>:17:6: error:
* Expected kind `[Nat]', but `[0]' has kind `*'
* In the type `[0]'
In the expression: foo @[0]
In an equation for `it': it = foo @[0]
<interactive>:17:7: error:
* Expected a type, but `0' has kind `Nat'
* In the type `[0]'
In the expression: foo @[0]
In an equation for `it': it = foo @[0]
```
why `[0]` has kind `*` here?
However this is legal:
```
> let foo :: forall (x :: Bool). (); foo = ()
> foo @True
()
> foo @'True
()
```
and this is wierd:
```
> :set -XPolyKinds
> let foo :: forall (x :: k). (); foo = ()
> foo @'True
<interactive>:12:6: error:
* Expected a type, but 'True has kind `Bool'
* In the type `True'
In the expression: foo @True
In an equation for `it': it = foo @True
> foo @True
<interactive>:13:6: error:
* Expected a type, but 'True has kind `Bool'
* In the type `True'
In the expression: foo @True
In an equation for `it': it = foo @True
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.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":"TypeApplications doesn't allow unticked list constructors.","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"TypeApplications doesn't allow unticked list constructor even when it is unambiguous:\r\n\r\n{{{\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\n> :set -XDataKinds\r\n> :set -XTypeApplications\r\n> :set -XScopedTypeVariables\r\n> :set -XKindSignatures\r\n> let foo :: forall (xs :: [Nat]). (); foo = ()\r\n> foo @'[0]\r\n()\r\n> foo @[0]\r\n\r\n<interactive>:17:6: error:\r\n * Expected kind `[Nat]', but `[0]' has kind `*'\r\n * In the type `[0]'\r\n In the expression: foo @[0]\r\n In an equation for `it': it = foo @[0]\r\n\r\n<interactive>:17:7: error:\r\n * Expected a type, but `0' has kind `Nat'\r\n * In the type `[0]'\r\n In the expression: foo @[0]\r\n In an equation for `it': it = foo @[0]\r\n}}}\r\nwhy `[0]` has kind `*` here?\r\n\r\nHowever this is legal:\r\n{{{\r\n> let foo :: forall (x :: Bool). (); foo = ()\r\n> foo @True\r\n()\r\n> foo @'True\r\n()\r\n}}}\r\n\r\nand this is wierd: \r\n{{{\r\n> :set -XPolyKinds\r\n> let foo :: forall (x :: k). (); foo = ()\r\n> foo @'True\r\n\r\n<interactive>:12:6: error:\r\n * Expected a type, but 'True has kind `Bool'\r\n * In the type `True'\r\n In the expression: foo @True\r\n In an equation for `it': it = foo @True\r\n> foo @True\r\n\r\n<interactive>:13:6: error:\r\n * Expected a type, but 'True has kind `Bool'\r\n * In the type `True'\r\n In the expression: foo @True\r\n In an equation for `it': it = foo @True\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->TypeApplications doesn't allow unticked list constructor even when it is unambiguous:
```
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
> :set -XDataKinds
> :set -XTypeApplications
> :set -XScopedTypeVariables
> :set -XKindSignatures
> let foo :: forall (xs :: [Nat]). (); foo = ()
> foo @'[0]
()
> foo @[0]
<interactive>:17:6: error:
* Expected kind `[Nat]', but `[0]' has kind `*'
* In the type `[0]'
In the expression: foo @[0]
In an equation for `it': it = foo @[0]
<interactive>:17:7: error:
* Expected a type, but `0' has kind `Nat'
* In the type `[0]'
In the expression: foo @[0]
In an equation for `it': it = foo @[0]
```
why `[0]` has kind `*` here?
However this is legal:
```
> let foo :: forall (x :: Bool). (); foo = ()
> foo @True
()
> foo @'True
()
```
and this is wierd:
```
> :set -XPolyKinds
> let foo :: forall (x :: k). (); foo = ()
> foo @'True
<interactive>:12:6: error:
* Expected a type, but 'True has kind `Bool'
* In the type `True'
In the expression: foo @True
In an equation for `it': it = foo @True
> foo @True
<interactive>:13:6: error:
* Expected a type, but 'True has kind `Bool'
* In the type `True'
In the expression: foo @True
In an equation for `it': it = foo @True
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.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":"TypeApplications doesn't allow unticked list constructors.","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"TypeApplications doesn't allow unticked list constructor even when it is unambiguous:\r\n\r\n{{{\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\n> :set -XDataKinds\r\n> :set -XTypeApplications\r\n> :set -XScopedTypeVariables\r\n> :set -XKindSignatures\r\n> let foo :: forall (xs :: [Nat]). (); foo = ()\r\n> foo @'[0]\r\n()\r\n> foo @[0]\r\n\r\n<interactive>:17:6: error:\r\n * Expected kind `[Nat]', but `[0]' has kind `*'\r\n * In the type `[0]'\r\n In the expression: foo @[0]\r\n In an equation for `it': it = foo @[0]\r\n\r\n<interactive>:17:7: error:\r\n * Expected a type, but `0' has kind `Nat'\r\n * In the type `[0]'\r\n In the expression: foo @[0]\r\n In an equation for `it': it = foo @[0]\r\n}}}\r\nwhy `[0]` has kind `*` here?\r\n\r\nHowever this is legal:\r\n{{{\r\n> let foo :: forall (x :: Bool). (); foo = ()\r\n> foo @True\r\n()\r\n> foo @'True\r\n()\r\n}}}\r\n\r\nand this is wierd: \r\n{{{\r\n> :set -XPolyKinds\r\n> let foo :: forall (x :: k). (); foo = ()\r\n> foo @'True\r\n\r\n<interactive>:12:6: error:\r\n * Expected a type, but 'True has kind `Bool'\r\n * In the type `True'\r\n In the expression: foo @True\r\n In an equation for `it': it = foo @True\r\n> foo @True\r\n\r\n<interactive>:13:6: error:\r\n * Expected a type, but 'True has kind `Bool'\r\n * In the type `True'\r\n In the expression: foo @True\r\n In an equation for `it': it = foo @True\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12535Bad error message when unidirectional pattern synonym used in bidirectional p...2019-07-07T18:26:11ZEdward Z. YangBad error message when unidirectional pattern synonym used in bidirectional pattern synonymIf I write:
```
{-# LANGUAGE PatternSynonyms #-}
module I where
pattern P2 x y <- (x, y)
pattern P1 x y = P2 x y
```
I get the error:
```
ezyang@sabre:~$ ghc-8.0 -c I.hs
I.hs:5:18: error:
• non-bidirectional pattern synonym ‘P2’ used in an expression
• In the expression: P2 x y
In an equation for ‘$bP1’: $bP1 x y = P2 x y
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| 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":"Bad error message when unidirectional pattern synonym used in bidirectional pattern synonym","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I write:\r\n\r\n{{{\r\n{-# LANGUAGE PatternSynonyms #-}\r\nmodule I where\r\n\r\npattern P2 x y <- (x, y)\r\npattern P1 x y = P2 x y\r\n}}}\r\n\r\nI get the error:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 -c I.hs\r\n\r\nI.hs:5:18: error:\r\n • non-bidirectional pattern synonym ‘P2’ used in an expression\r\n • In the expression: P2 x y\r\n In an equation for ‘$bP1’: $bP1 x y = P2 x y\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->If I write:
```
{-# LANGUAGE PatternSynonyms #-}
module I where
pattern P2 x y <- (x, y)
pattern P1 x y = P2 x y
```
I get the error:
```
ezyang@sabre:~$ ghc-8.0 -c I.hs
I.hs:5:18: error:
• non-bidirectional pattern synonym ‘P2’ used in an expression
• In the expression: P2 x y
In an equation for ‘$bP1’: $bP1 x y = P2 x y
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| 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":"Bad error message when unidirectional pattern synonym used in bidirectional pattern synonym","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I write:\r\n\r\n{{{\r\n{-# LANGUAGE PatternSynonyms #-}\r\nmodule I where\r\n\r\npattern P2 x y <- (x, y)\r\npattern P1 x y = P2 x y\r\n}}}\r\n\r\nI get the error:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 -c I.hs\r\n\r\nI.hs:5:18: error:\r\n • non-bidirectional pattern synonym ‘P2’ used in an expression\r\n • In the expression: P2 x y\r\n In an equation for ‘$bP1’: $bP1 x y = P2 x y\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12362don't complain about type variable ambiguity when the expression is parametri...2019-07-07T18:26:56Zrwbartondon't complain about type variable ambiguity when the expression is parametrically polymorphicI'm not sure this is really a good idea, but it did come up in practice.
Consider the following rather contrived program:
```hs
{-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables,
AllowAmbiguousTypes, TypeApplications #-}
module E where
type family T a
type instance T Int = Char
type instance T String = Char
type instance T Bool = ()
newtype FT a = FT [T a]
m :: forall a. (forall x. T x -> Int) -> FT a -> [Int]
m f (FT xs) = map f xs
```
GHC rejects it with the error:
```
E.hs:14:21: error:
• Couldn't match type ‘T a’ with ‘T x0’
Expected type: [T x0]
Actual type: [T a]
NB: ‘T’ is a type function, and may not be injective
The type variable ‘x0’ is ambiguous
• In the second argument of ‘map’, namely ‘xs’
In the expression: map f xs
In an equation for ‘m’: m f (FT xs) = map f xs
• Relevant bindings include
xs :: [T a] (bound at E.hs:14:9)
m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1)
```
The problem seems to be that GHC doesn't know at what type to instantiate `f`, because it can't conclude from the argument of `f` being `T a` that the type parameter of `f` needs to be `x`. In fact, `T` here really is not injective, so if `a` is `Int`, `x` could just as well be `String`.
However, in this case the ambiguity doesn't actually matter. If `f @Int` and `f @String` have the same type because `T Int ~ T String`, then they are actually the same value too by parametricity, because there is no class constraint on `x`. Since GHC prints a message saying that `T` is not known to be injective, it sounds like it knows about the possible solution `x0 = a`. So it could just pick it, and accept the original program.
With TypeApplications I can just specify the intended value of `x` by writing
```
m f (FT xs) = map (f @a) xs
```
which is a reasonable workaround in my real use case also. Interestingly I can't seem to achieve the same thing without TypeApplications without adding a proxy argument to `f`, which I don't much want to do.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"don't complain about type variable ambiguity when the expression is parametrically polymorphic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I'm not sure this is really a good idea, but it did come up in practice.\r\nConsider the following rather contrived program:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables,\r\n AllowAmbiguousTypes, TypeApplications #-}\r\n\r\nmodule E where\r\n\r\ntype family T a\r\ntype instance T Int = Char\r\ntype instance T String = Char\r\ntype instance T Bool = ()\r\n\r\nnewtype FT a = FT [T a]\r\n\r\nm :: forall a. (forall x. T x -> Int) -> FT a -> [Int]\r\nm f (FT xs) = map f xs\r\n}}}\r\nGHC rejects it with the error:\r\n{{{\r\nE.hs:14:21: error:\r\n • Couldn't match type ‘T a’ with ‘T x0’\r\n Expected type: [T x0]\r\n Actual type: [T a]\r\n NB: ‘T’ is a type function, and may not be injective\r\n The type variable ‘x0’ is ambiguous\r\n • In the second argument of ‘map’, namely ‘xs’\r\n In the expression: map f xs\r\n In an equation for ‘m’: m f (FT xs) = map f xs\r\n • Relevant bindings include\r\n xs :: [T a] (bound at E.hs:14:9)\r\n m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1)\r\n}}}\r\nThe problem seems to be that GHC doesn't know at what type to instantiate `f`, because it can't conclude from the argument of `f` being `T a` that the type parameter of `f` needs to be `x`. In fact, `T` here really is not injective, so if `a` is `Int`, `x` could just as well be `String`.\r\n\r\nHowever, in this case the ambiguity doesn't actually matter. If `f @Int` and `f @String` have the same type because `T Int ~ T String`, then they are actually the same value too by parametricity, because there is no class constraint on `x`. Since GHC prints a message saying that `T` is not known to be injective, it sounds like it knows about the possible solution `x0 = a`. So it could just pick it, and accept the original program.\r\n\r\nWith TypeApplications I can just specify the intended value of `x` by writing\r\n{{{\r\nm f (FT xs) = map (f @a) xs\r\n}}}\r\nwhich is a reasonable workaround in my real use case also. Interestingly I can't seem to achieve the same thing without TypeApplications without adding a proxy argument to `f`, which I don't much want to do.","type_of_failure":"OtherFailure","blocking":[]} -->I'm not sure this is really a good idea, but it did come up in practice.
Consider the following rather contrived program:
```hs
{-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables,
AllowAmbiguousTypes, TypeApplications #-}
module E where
type family T a
type instance T Int = Char
type instance T String = Char
type instance T Bool = ()
newtype FT a = FT [T a]
m :: forall a. (forall x. T x -> Int) -> FT a -> [Int]
m f (FT xs) = map f xs
```
GHC rejects it with the error:
```
E.hs:14:21: error:
• Couldn't match type ‘T a’ with ‘T x0’
Expected type: [T x0]
Actual type: [T a]
NB: ‘T’ is a type function, and may not be injective
The type variable ‘x0’ is ambiguous
• In the second argument of ‘map’, namely ‘xs’
In the expression: map f xs
In an equation for ‘m’: m f (FT xs) = map f xs
• Relevant bindings include
xs :: [T a] (bound at E.hs:14:9)
m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1)
```
The problem seems to be that GHC doesn't know at what type to instantiate `f`, because it can't conclude from the argument of `f` being `T a` that the type parameter of `f` needs to be `x`. In fact, `T` here really is not injective, so if `a` is `Int`, `x` could just as well be `String`.
However, in this case the ambiguity doesn't actually matter. If `f @Int` and `f @String` have the same type because `T Int ~ T String`, then they are actually the same value too by parametricity, because there is no class constraint on `x`. Since GHC prints a message saying that `T` is not known to be injective, it sounds like it knows about the possible solution `x0 = a`. So it could just pick it, and accept the original program.
With TypeApplications I can just specify the intended value of `x` by writing
```
m f (FT xs) = map (f @a) xs
```
which is a reasonable workaround in my real use case also. Interestingly I can't seem to achieve the same thing without TypeApplications without adding a proxy argument to `f`, which I don't much want to do.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"don't complain about type variable ambiguity when the expression is parametrically polymorphic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I'm not sure this is really a good idea, but it did come up in practice.\r\nConsider the following rather contrived program:\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables,\r\n AllowAmbiguousTypes, TypeApplications #-}\r\n\r\nmodule E where\r\n\r\ntype family T a\r\ntype instance T Int = Char\r\ntype instance T String = Char\r\ntype instance T Bool = ()\r\n\r\nnewtype FT a = FT [T a]\r\n\r\nm :: forall a. (forall x. T x -> Int) -> FT a -> [Int]\r\nm f (FT xs) = map f xs\r\n}}}\r\nGHC rejects it with the error:\r\n{{{\r\nE.hs:14:21: error:\r\n • Couldn't match type ‘T a’ with ‘T x0’\r\n Expected type: [T x0]\r\n Actual type: [T a]\r\n NB: ‘T’ is a type function, and may not be injective\r\n The type variable ‘x0’ is ambiguous\r\n • In the second argument of ‘map’, namely ‘xs’\r\n In the expression: map f xs\r\n In an equation for ‘m’: m f (FT xs) = map f xs\r\n • Relevant bindings include\r\n xs :: [T a] (bound at E.hs:14:9)\r\n m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1)\r\n}}}\r\nThe problem seems to be that GHC doesn't know at what type to instantiate `f`, because it can't conclude from the argument of `f` being `T a` that the type parameter of `f` needs to be `x`. In fact, `T` here really is not injective, so if `a` is `Int`, `x` could just as well be `String`.\r\n\r\nHowever, in this case the ambiguity doesn't actually matter. If `f @Int` and `f @String` have the same type because `T Int ~ T String`, then they are actually the same value too by parametricity, because there is no class constraint on `x`. Since GHC prints a message saying that `T` is not known to be injective, it sounds like it knows about the possible solution `x0 = a`. So it could just pick it, and accept the original program.\r\n\r\nWith TypeApplications I can just specify the intended value of `x` by writing\r\n{{{\r\nm f (FT xs) = map (f @a) xs\r\n}}}\r\nwhich is a reasonable workaround in my real use case also. Interestingly I can't seem to achieve the same thing without TypeApplications without adding a proxy argument to `f`, which I don't much want to do.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12203Allow constructors on LHS of (implicit) bidirectional pattern synonym2021-07-27T05:38:09ZEdward Z. YangAllow constructors on LHS of (implicit) bidirectional pattern synonymInspired by the recent Ghostbuster paper http://www.cs.ox.ac.uk/people/timothy.zakian/ghostbuster.pdf , I was experimenting with using pattern synonyms to simulate GADTs. In the process, I noticed that we should be able to generalize the implicit bidirectional synonyms to allow constructors on the LHS.
Consider this program:
```
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module GhostBuster where
import GHC.TypeLits
newtype Vec a (n :: Nat) = Vec { unVec :: [a] }
pattern VNil :: Vec a 0
pattern VNil = Vec []
pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x xs <- Vec (x : (Vec -> xs)) where
VCons x (Vec xs) = Vec (x : xs)
headVec :: Vec a (n + 1) -> a
headVec (VCons x _) = x
```
In effect, we simulate a vector GADT using pattern synonyms to handle the newtype `Vec`.
I would like it if I could specify the `VCons` pattern more simply, as just:
```
pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x (Vec xs) = Vec (x : xs)
```
And GHC would infer the correct pattern (the constructor can be read off immediately), automatically replacing occurrences of `xs` with a view pattern that reconstructs the constructors that were stripped off on the LHS.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| 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":"Allow constructors on LHS of (implicit) bidirectional pattern synonym","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Inspired by the recent Ghostbuster paper http://www.cs.ox.ac.uk/people/timothy.zakian/ghostbuster.pdf , I was experimenting with using pattern synonyms to simulate GADTs. In the process, I noticed that we should be able to generalize the implicit bidirectional synonyms to allow constructors on the LHS.\r\n\r\nConsider this program:\r\n\r\n{{{\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE ViewPatterns #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}\r\nmodule GhostBuster where\r\n\r\nimport GHC.TypeLits\r\n\r\nnewtype Vec a (n :: Nat) = Vec { unVec :: [a] }\r\n\r\npattern VNil :: Vec a 0\r\npattern VNil = Vec []\r\n\r\npattern VCons :: a -> Vec a n -> Vec a (n + 1)\r\npattern VCons x xs <- Vec (x : (Vec -> xs)) where\r\n VCons x (Vec xs) = Vec (x : xs)\r\n\r\nheadVec :: Vec a (n + 1) -> a\r\nheadVec (VCons x _) = x\r\n}}}\r\n\r\nIn effect, we simulate a vector GADT using pattern synonyms to handle the newtype `Vec`.\r\n\r\nI would like it if I could specify the `VCons` pattern more simply, as just:\r\n\r\n{{{\r\npattern VCons :: a -> Vec a n -> Vec a (n + 1)\r\npattern VCons x (Vec xs) = Vec (x : xs)\r\n}}}\r\n\r\nAnd GHC would infer the correct pattern (the constructor can be read off immediately), automatically replacing occurrences of `xs` with a view pattern that reconstructs the constructors that were stripped off on the LHS.","type_of_failure":"OtherFailure","blocking":[]} -->Inspired by the recent Ghostbuster paper http://www.cs.ox.ac.uk/people/timothy.zakian/ghostbuster.pdf , I was experimenting with using pattern synonyms to simulate GADTs. In the process, I noticed that we should be able to generalize the implicit bidirectional synonyms to allow constructors on the LHS.
Consider this program:
```
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module GhostBuster where
import GHC.TypeLits
newtype Vec a (n :: Nat) = Vec { unVec :: [a] }
pattern VNil :: Vec a 0
pattern VNil = Vec []
pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x xs <- Vec (x : (Vec -> xs)) where
VCons x (Vec xs) = Vec (x : xs)
headVec :: Vec a (n + 1) -> a
headVec (VCons x _) = x
```
In effect, we simulate a vector GADT using pattern synonyms to handle the newtype `Vec`.
I would like it if I could specify the `VCons` pattern more simply, as just:
```
pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x (Vec xs) = Vec (x : xs)
```
And GHC would infer the correct pattern (the constructor can be read off immediately), automatically replacing occurrences of `xs` with a view pattern that reconstructs the constructors that were stripped off on the LHS.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| 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":"Allow constructors on LHS of (implicit) bidirectional pattern synonym","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Inspired by the recent Ghostbuster paper http://www.cs.ox.ac.uk/people/timothy.zakian/ghostbuster.pdf , I was experimenting with using pattern synonyms to simulate GADTs. In the process, I noticed that we should be able to generalize the implicit bidirectional synonyms to allow constructors on the LHS.\r\n\r\nConsider this program:\r\n\r\n{{{\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE ViewPatterns #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}\r\nmodule GhostBuster where\r\n\r\nimport GHC.TypeLits\r\n\r\nnewtype Vec a (n :: Nat) = Vec { unVec :: [a] }\r\n\r\npattern VNil :: Vec a 0\r\npattern VNil = Vec []\r\n\r\npattern VCons :: a -> Vec a n -> Vec a (n + 1)\r\npattern VCons x xs <- Vec (x : (Vec -> xs)) where\r\n VCons x (Vec xs) = Vec (x : xs)\r\n\r\nheadVec :: Vec a (n + 1) -> a\r\nheadVec (VCons x _) = x\r\n}}}\r\n\r\nIn effect, we simulate a vector GADT using pattern synonyms to handle the newtype `Vec`.\r\n\r\nI would like it if I could specify the `VCons` pattern more simply, as just:\r\n\r\n{{{\r\npattern VCons :: a -> Vec a n -> Vec a (n + 1)\r\npattern VCons x (Vec xs) = Vec (x : xs)\r\n}}}\r\n\r\nAnd GHC would infer the correct pattern (the constructor can be read off immediately), automatically replacing occurrences of `xs` with a view pattern that reconstructs the constructors that were stripped off on the LHS.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12190Generalize irrefutable patterns (static semantics like let-bindings)2019-07-07T18:27:14ZEdward Z. YangGeneralize irrefutable patterns (static semantics like let-bindings)tl;dr It is not let-bindings that should be generalized, it is \*\*irrefutable\*\* patterns that should be generalized.
I know GHC's trend has been to reduce the amount of let-generalization we do (since it interacts poorly with GADTs). However, I was recently working with some useful rank-2 definitions, and found that I would have really appreciated let-style generalization for irrefutable pattern matches. Here is the motivating example:
```
{-# LANGUAGE Rank2Types #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module X where
data IntStreamK k
= Cons { hd :: Int, tl :: IntStreamK k }
data IntStream
= IntStream { unIntStream :: forall k. IntStreamK k }
f1, f2, f3, f4 :: IntStream -> IntStream
-- Does not work, type variable escapes
f1 (IntStream (Cons x xs)) = IntStream (Cons (x + 1) xs)
-- OK
f2 (IntStream s) = IntStream (Cons (hd s + 1) (tl s))
-- Works UNLESS GADTs are enabled (uses let generalization)
f3 (IntStream s) =
let Cons x xs = s
in IntStream (Cons (x + 1) xs)
-- Does not work, type variable escapes
f4 (IntStream ~(Cons x xs)) = IntStream (Cons (x + 1) xs)
```
`IntStreamK` is modeled off of a clock-indexed stream representation ala "Productive Coprogramming with Guarded Recursion" (c.f., http://bentnib.org/productive.pdf), although I've simplified the type a bit for this example. The important thing in this example `IntStream` takes a `IntStreamK` which is universally quantified over the clock index.
I want to define a simple function: take a stream and increment its head (without using a record update). There are a number of very similar looking definitions, but only some of them typecheck; in the rest, `xs` fails to be sufficiently generalized.
1. `f1` is the most obvious code to write, but actually we can't elaborate this into Core:
```
f1 = \ (x :: IntStream) ->
case x of { IntStream s ->
case s @ ??? of { Cons x xs ->
IntStream
(\ (@ k) -> Cons @ k (x+1) xs ) }}
```
> The problem arises when we consider what type we will apply to `s` (which has type `forall k. IntStreamK k`): we want to use `k` bound by the type lambda inside `IntStream`, but it is not yet in scope!
1. `f2` works. Here is its Core elaboration:
```
f2 = \ (x :: IntStream) ->
case x of { IntStream s ->
IntStream
(\ (@ k) -> Cons @ k (hd (s @ k) + 1) (tl (s @ k))) }
```
1. `f3` works, because the let-binding gets generalized. We end up with this Core elaboration:
```
f3 = \ (x :: IntStream) ->
case x of { IntStream s ->
let {
y :: forall k. (Int, IntStreamK k)
y =
\ (@ k) -> case s @ k of { Cons x xs ->
(x, xs) } in
IntStream
(\ (@ k) -> Cons @ k
((case y of {(x, _) -> x}) + 1)
(case y of {(_, xs) -> xs})) }
```
> (GHC's actual desugaring for `y` is a bit more complex so I shortened it.) Note that this core is effectively the same as `f2`, except that (1) the type application has been commoned up, and (2) the `hd`/`tl` functions are inlined. If we turn on GADTs (without NoMonoLocalBinds) GHC stops generalizing this let binding and thus fails to typecheck. If you make this a strict let-binding this fails to typecheck (since we can't generalize strict let bindings; they're just like case.)
1. The important one: this does not work, because when we bind `x` and `xs`, we immediately apply the type application, but do not generalize so no suitable type is in scope. However, operationally, the core elaboration should be exactly the same as in (3). So it would be fine to generalize here: the static semantics are validated by elaborating irrefutable pattern matches into let bindings.
So, it would be convenient for this application of irrefutable patterns were generalized; then I could write almost the obvious code and have GHC accept it. The same caveat with GADTs and let-bindings would apply: with GADTs enabled irrefutable patterns would not be generalized.
Unfortunately, if we add another constructor to `Cons` there is NO total System FC program that works (e.g. http://stackoverflow.com/questions/7720108/total-function-of-type-forall-n-maybe-f-n-maybe-forall-n-f-n)... but that's a story for another day.
#11700 seems a bit related.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Generalize irrefutable patterns (static semantics like let-bindings)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"FeatureRequest","description":"tl;dr It is not let-bindings that should be generalized, it is **irrefutable** patterns that should be generalized.\r\n\r\nI know GHC's trend has been to reduce the amount of let-generalization we do (since it interacts poorly with GADTs). However, I was recently working with some useful rank-2 definitions, and found that I would have really appreciated let-style generalization for irrefutable pattern matches. Here is the motivating example:\r\n\r\n{{{\r\n{-# LANGUAGE Rank2Types #-}\r\n{-# OPTIONS_GHC -fdefer-type-errors #-}\r\nmodule X where\r\n\r\ndata IntStreamK k\r\n = Cons { hd :: Int, tl :: IntStreamK k }\r\ndata IntStream\r\n = IntStream { unIntStream :: forall k. IntStreamK k }\r\n\r\nf1, f2, f3, f4 :: IntStream -> IntStream\r\n\r\n-- Does not work, type variable escapes\r\nf1 (IntStream (Cons x xs)) = IntStream (Cons (x + 1) xs)\r\n\r\n-- OK\r\nf2 (IntStream s) = IntStream (Cons (hd s + 1) (tl s))\r\n\r\n-- Works UNLESS GADTs are enabled (uses let generalization)\r\nf3 (IntStream s) =\r\n let Cons x xs = s\r\n in IntStream (Cons (x + 1) xs)\r\n\r\n-- Does not work, type variable escapes\r\nf4 (IntStream ~(Cons x xs)) = IntStream (Cons (x + 1) xs)\r\n}}}\r\n\r\n`IntStreamK` is modeled off of a clock-indexed stream representation ala \"Productive Coprogramming with Guarded Recursion\" (c.f., http://bentnib.org/productive.pdf), although I've simplified the type a bit for this example. The important thing in this example `IntStream` takes a `IntStreamK` which is universally quantified over the clock index.\r\n\r\nI want to define a simple function: take a stream and increment its head (without using a record update). There are a number of very similar looking definitions, but only some of them typecheck; in the rest, `xs` fails to be sufficiently generalized.\r\n\r\n1. `f1` is the most obvious code to write, but actually we can't elaborate this into Core:\r\n{{{\r\nf1 = \\ (x :: IntStream) ->\r\n case x of { IntStream s ->\r\n case s @ ??? of { Cons x xs ->\r\n IntStream\r\n (\\ (@ k) -> Cons @ k (x+1) xs ) }}\r\n}}}\r\n The problem arises when we consider what type we will apply to `s` (which has type `forall k. IntStreamK k`): we want to use `k` bound by the type lambda inside `IntStream`, but it is not yet in scope!\r\n\r\n2. `f2` works. Here is its Core elaboration:\r\n{{{\r\nf2 = \\ (x :: IntStream) ->\r\n case x of { IntStream s ->\r\n IntStream\r\n (\\ (@ k) -> Cons @ k (hd (s @ k) + 1) (tl (s @ k))) }\r\n}}}\r\n\r\n3. `f3` works, because the let-binding gets generalized. We end up with this Core elaboration:\r\n{{{\r\nf3 = \\ (x :: IntStream) ->\r\n case x of { IntStream s ->\r\n let {\r\n y :: forall k. (Int, IntStreamK k)\r\n y =\r\n \\ (@ k) -> case s @ k of { Cons x xs ->\r\n (x, xs) } in\r\n IntStream\r\n (\\ (@ k) -> Cons @ k\r\n ((case y of {(x, _) -> x}) + 1)\r\n (case y of {(_, xs) -> xs})) }\r\n}}}\r\n (GHC's actual desugaring for `y` is a bit more complex so I shortened it.) Note that this core is effectively the same as `f2`, except that (1) the type application has been commoned up, and (2) the `hd`/`tl` functions are inlined. If we turn on GADTs (without NoMonoLocalBinds) GHC stops generalizing this let binding and thus fails to typecheck. If you make this a strict let-binding this fails to typecheck (since we can't generalize strict let bindings; they're just like case.)\r\n\r\n4. The important one: this does not work, because when we bind `x` and `xs`, we immediately apply the type application, but do not generalize so no suitable type is in scope. However, operationally, the core elaboration should be exactly the same as in (3). So it would be fine to generalize here: the static semantics are validated by elaborating irrefutable pattern matches into let bindings.\r\n\r\nSo, it would be convenient for this application of irrefutable patterns were generalized; then I could write almost the obvious code and have GHC accept it. The same caveat with GADTs and let-bindings would apply: with GADTs enabled irrefutable patterns would not be generalized.\r\n\r\nUnfortunately, if we add another constructor to `Cons` there is NO total System FC program that works (e.g. http://stackoverflow.com/questions/7720108/total-function-of-type-forall-n-maybe-f-n-maybe-forall-n-f-n)... but that's a story for another day.\r\n\r\n#11700 seems a bit related.","type_of_failure":"OtherFailure","blocking":[]} -->tl;dr It is not let-bindings that should be generalized, it is \*\*irrefutable\*\* patterns that should be generalized.
I know GHC's trend has been to reduce the amount of let-generalization we do (since it interacts poorly with GADTs). However, I was recently working with some useful rank-2 definitions, and found that I would have really appreciated let-style generalization for irrefutable pattern matches. Here is the motivating example:
```
{-# LANGUAGE Rank2Types #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module X where
data IntStreamK k
= Cons { hd :: Int, tl :: IntStreamK k }
data IntStream
= IntStream { unIntStream :: forall k. IntStreamK k }
f1, f2, f3, f4 :: IntStream -> IntStream
-- Does not work, type variable escapes
f1 (IntStream (Cons x xs)) = IntStream (Cons (x + 1) xs)
-- OK
f2 (IntStream s) = IntStream (Cons (hd s + 1) (tl s))
-- Works UNLESS GADTs are enabled (uses let generalization)
f3 (IntStream s) =
let Cons x xs = s
in IntStream (Cons (x + 1) xs)
-- Does not work, type variable escapes
f4 (IntStream ~(Cons x xs)) = IntStream (Cons (x + 1) xs)
```
`IntStreamK` is modeled off of a clock-indexed stream representation ala "Productive Coprogramming with Guarded Recursion" (c.f., http://bentnib.org/productive.pdf), although I've simplified the type a bit for this example. The important thing in this example `IntStream` takes a `IntStreamK` which is universally quantified over the clock index.
I want to define a simple function: take a stream and increment its head (without using a record update). There are a number of very similar looking definitions, but only some of them typecheck; in the rest, `xs` fails to be sufficiently generalized.
1. `f1` is the most obvious code to write, but actually we can't elaborate this into Core:
```
f1 = \ (x :: IntStream) ->
case x of { IntStream s ->
case s @ ??? of { Cons x xs ->
IntStream
(\ (@ k) -> Cons @ k (x+1) xs ) }}
```
> The problem arises when we consider what type we will apply to `s` (which has type `forall k. IntStreamK k`): we want to use `k` bound by the type lambda inside `IntStream`, but it is not yet in scope!
1. `f2` works. Here is its Core elaboration:
```
f2 = \ (x :: IntStream) ->
case x of { IntStream s ->
IntStream
(\ (@ k) -> Cons @ k (hd (s @ k) + 1) (tl (s @ k))) }
```
1. `f3` works, because the let-binding gets generalized. We end up with this Core elaboration:
```
f3 = \ (x :: IntStream) ->
case x of { IntStream s ->
let {
y :: forall k. (Int, IntStreamK k)
y =
\ (@ k) -> case s @ k of { Cons x xs ->
(x, xs) } in
IntStream
(\ (@ k) -> Cons @ k
((case y of {(x, _) -> x}) + 1)
(case y of {(_, xs) -> xs})) }
```
> (GHC's actual desugaring for `y` is a bit more complex so I shortened it.) Note that this core is effectively the same as `f2`, except that (1) the type application has been commoned up, and (2) the `hd`/`tl` functions are inlined. If we turn on GADTs (without NoMonoLocalBinds) GHC stops generalizing this let binding and thus fails to typecheck. If you make this a strict let-binding this fails to typecheck (since we can't generalize strict let bindings; they're just like case.)
1. The important one: this does not work, because when we bind `x` and `xs`, we immediately apply the type application, but do not generalize so no suitable type is in scope. However, operationally, the core elaboration should be exactly the same as in (3). So it would be fine to generalize here: the static semantics are validated by elaborating irrefutable pattern matches into let bindings.
So, it would be convenient for this application of irrefutable patterns were generalized; then I could write almost the obvious code and have GHC accept it. The same caveat with GADTs and let-bindings would apply: with GADTs enabled irrefutable patterns would not be generalized.
Unfortunately, if we add another constructor to `Cons` there is NO total System FC program that works (e.g. http://stackoverflow.com/questions/7720108/total-function-of-type-forall-n-maybe-f-n-maybe-forall-n-f-n)... but that's a story for another day.
#11700 seems a bit related.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Generalize irrefutable patterns (static semantics like let-bindings)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"FeatureRequest","description":"tl;dr It is not let-bindings that should be generalized, it is **irrefutable** patterns that should be generalized.\r\n\r\nI know GHC's trend has been to reduce the amount of let-generalization we do (since it interacts poorly with GADTs). However, I was recently working with some useful rank-2 definitions, and found that I would have really appreciated let-style generalization for irrefutable pattern matches. Here is the motivating example:\r\n\r\n{{{\r\n{-# LANGUAGE Rank2Types #-}\r\n{-# OPTIONS_GHC -fdefer-type-errors #-}\r\nmodule X where\r\n\r\ndata IntStreamK k\r\n = Cons { hd :: Int, tl :: IntStreamK k }\r\ndata IntStream\r\n = IntStream { unIntStream :: forall k. IntStreamK k }\r\n\r\nf1, f2, f3, f4 :: IntStream -> IntStream\r\n\r\n-- Does not work, type variable escapes\r\nf1 (IntStream (Cons x xs)) = IntStream (Cons (x + 1) xs)\r\n\r\n-- OK\r\nf2 (IntStream s) = IntStream (Cons (hd s + 1) (tl s))\r\n\r\n-- Works UNLESS GADTs are enabled (uses let generalization)\r\nf3 (IntStream s) =\r\n let Cons x xs = s\r\n in IntStream (Cons (x + 1) xs)\r\n\r\n-- Does not work, type variable escapes\r\nf4 (IntStream ~(Cons x xs)) = IntStream (Cons (x + 1) xs)\r\n}}}\r\n\r\n`IntStreamK` is modeled off of a clock-indexed stream representation ala \"Productive Coprogramming with Guarded Recursion\" (c.f., http://bentnib.org/productive.pdf), although I've simplified the type a bit for this example. The important thing in this example `IntStream` takes a `IntStreamK` which is universally quantified over the clock index.\r\n\r\nI want to define a simple function: take a stream and increment its head (without using a record update). There are a number of very similar looking definitions, but only some of them typecheck; in the rest, `xs` fails to be sufficiently generalized.\r\n\r\n1. `f1` is the most obvious code to write, but actually we can't elaborate this into Core:\r\n{{{\r\nf1 = \\ (x :: IntStream) ->\r\n case x of { IntStream s ->\r\n case s @ ??? of { Cons x xs ->\r\n IntStream\r\n (\\ (@ k) -> Cons @ k (x+1) xs ) }}\r\n}}}\r\n The problem arises when we consider what type we will apply to `s` (which has type `forall k. IntStreamK k`): we want to use `k` bound by the type lambda inside `IntStream`, but it is not yet in scope!\r\n\r\n2. `f2` works. Here is its Core elaboration:\r\n{{{\r\nf2 = \\ (x :: IntStream) ->\r\n case x of { IntStream s ->\r\n IntStream\r\n (\\ (@ k) -> Cons @ k (hd (s @ k) + 1) (tl (s @ k))) }\r\n}}}\r\n\r\n3. `f3` works, because the let-binding gets generalized. We end up with this Core elaboration:\r\n{{{\r\nf3 = \\ (x :: IntStream) ->\r\n case x of { IntStream s ->\r\n let {\r\n y :: forall k. (Int, IntStreamK k)\r\n y =\r\n \\ (@ k) -> case s @ k of { Cons x xs ->\r\n (x, xs) } in\r\n IntStream\r\n (\\ (@ k) -> Cons @ k\r\n ((case y of {(x, _) -> x}) + 1)\r\n (case y of {(_, xs) -> xs})) }\r\n}}}\r\n (GHC's actual desugaring for `y` is a bit more complex so I shortened it.) Note that this core is effectively the same as `f2`, except that (1) the type application has been commoned up, and (2) the `hd`/`tl` functions are inlined. If we turn on GADTs (without NoMonoLocalBinds) GHC stops generalizing this let binding and thus fails to typecheck. If you make this a strict let-binding this fails to typecheck (since we can't generalize strict let bindings; they're just like case.)\r\n\r\n4. The important one: this does not work, because when we bind `x` and `xs`, we immediately apply the type application, but do not generalize so no suitable type is in scope. However, operationally, the core elaboration should be exactly the same as in (3). So it would be fine to generalize here: the static semantics are validated by elaborating irrefutable pattern matches into let bindings.\r\n\r\nSo, it would be convenient for this application of irrefutable patterns were generalized; then I could write almost the obvious code and have GHC accept it. The same caveat with GADTs and let-bindings would apply: with GADTs enabled irrefutable patterns would not be generalized.\r\n\r\nUnfortunately, if we add another constructor to `Cons` there is NO total System FC program that works (e.g. http://stackoverflow.com/questions/7720108/total-function-of-type-forall-n-maybe-f-n-maybe-forall-n-f-n)... but that's a story for another day.\r\n\r\n#11700 seems a bit related.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12183Do not display global bindings with -fno-max-relevant-binds2019-07-07T18:27:18ZEdward Z. YangDo not display global bindings with -fno-max-relevant-bindsPresently, "Relevant bindings" messages (e.g., from holes) will attempt to report all local bindings, and relevant global bindings (by some heuristic), up to the number of bindings specified by `-fmax-relevant-binds=N`. For example, here is an error I recently had with a small number of relevant bindings:
```
Productive.hs:162:16: error:
• Found hole: _ :: Par (D k0 (Stream k0 b))
Where: ‘k0’ is an ambiguous type variable
‘b’ is a rigid type variable bound by
the type signature for:
maapM :: forall a b.
(a -> Par b)
-> (forall (k :: Clock). Stream k a) -> Par (Forall1 Stream b)
at Productive.hs:155:10
• In the second argument of ‘(<$>)’, namely ‘_’
In a stmt of a 'do' block: Cons b <$> _
In the expression:
do { (a, s') <- deStreamCons s;
b <- f a;
b' <- f (scar (unForall1 s'));
Cons b <$> _ }
• Relevant bindings include
b' :: b (bound at Productive.hs:159:5)
b :: b (bound at Productive.hs:158:5)
s' :: Forall1 Stream a (bound at Productive.hs:157:9)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
```
When I set `-fno-max-relevant-binds)`, this extends with:
```
a :: a (bound at Productive.hs:157:6)
s :: forall (k :: Clock). Stream k a (bound at Productive.hs:156:9)
f :: a -> Par b (bound at Productive.hs:156:7)
maapM :: (a -> Par b)
-> (forall (k :: Clock). Stream k a) -> Par (Forall1 Stream b)
(bound at Productive.hs:156:1)
take :: forall a.
Int -> (forall (k :: Clock). Stream k a) -> Par [a]
(bound at Productive.hs:143:1)
...and a pile more global binds...
```
I think this is not really the behavior we want. If I'm doing an Agda/Coq development, what I want is for the compiler to tell me all LOCAL bindings. Heuristically picked global bindings might be nice, but it's not a priority (after all, I probably have explicit type signatures for all of these anyway.) So really, to see all local bindings I just want to set `-fmax-relevant-binds=100000` (i.e., to a large number.)
So, I think there should be another flag `-frelevant-global-binds` which triggers display of global relevant bindings, making `-fno-max-relevant-binds` equivalent to `-fmax-relevant-binds=BIGNUM`; i.e., it does NOT report global bindings. I don't know if the error message should mention `-frelevant-global-binds` by default, but for now I would say it shouldn't.
As a minor addendum, I don't find the context information `In the second argument of ‘(<$>)’, namely ‘_’`, etc. very useful. Just makes the message longer and harder to view.Presently, "Relevant bindings" messages (e.g., from holes) will attempt to report all local bindings, and relevant global bindings (by some heuristic), up to the number of bindings specified by `-fmax-relevant-binds=N`. For example, here is an error I recently had with a small number of relevant bindings:
```
Productive.hs:162:16: error:
• Found hole: _ :: Par (D k0 (Stream k0 b))
Where: ‘k0’ is an ambiguous type variable
‘b’ is a rigid type variable bound by
the type signature for:
maapM :: forall a b.
(a -> Par b)
-> (forall (k :: Clock). Stream k a) -> Par (Forall1 Stream b)
at Productive.hs:155:10
• In the second argument of ‘(<$>)’, namely ‘_’
In a stmt of a 'do' block: Cons b <$> _
In the expression:
do { (a, s') <- deStreamCons s;
b <- f a;
b' <- f (scar (unForall1 s'));
Cons b <$> _ }
• Relevant bindings include
b' :: b (bound at Productive.hs:159:5)
b :: b (bound at Productive.hs:158:5)
s' :: Forall1 Stream a (bound at Productive.hs:157:9)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
```
When I set `-fno-max-relevant-binds)`, this extends with:
```
a :: a (bound at Productive.hs:157:6)
s :: forall (k :: Clock). Stream k a (bound at Productive.hs:156:9)
f :: a -> Par b (bound at Productive.hs:156:7)
maapM :: (a -> Par b)
-> (forall (k :: Clock). Stream k a) -> Par (Forall1 Stream b)
(bound at Productive.hs:156:1)
take :: forall a.
Int -> (forall (k :: Clock). Stream k a) -> Par [a]
(bound at Productive.hs:143:1)
...and a pile more global binds...
```
I think this is not really the behavior we want. If I'm doing an Agda/Coq development, what I want is for the compiler to tell me all LOCAL bindings. Heuristically picked global bindings might be nice, but it's not a priority (after all, I probably have explicit type signatures for all of these anyway.) So really, to see all local bindings I just want to set `-fmax-relevant-binds=100000` (i.e., to a large number.)
So, I think there should be another flag `-frelevant-global-binds` which triggers display of global relevant bindings, making `-fno-max-relevant-binds` equivalent to `-fmax-relevant-binds=BIGNUM`; i.e., it does NOT report global bindings. I don't know if the error message should mention `-frelevant-global-binds` by default, but for now I would say it shouldn't.
As a minor addendum, I don't find the context information `In the second argument of ‘(<$>)’, namely ‘_’`, etc. very useful. Just makes the message longer and harder to view.