GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-09-28T10:28:48Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/17360Panic while printing levity polymorphism error2021-09-28T10:28:48ZmniipPanic while printing levity polymorphism error## Program
```haskell
{-# LANGUAGE UnliftedNewtypes #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE PolyKinds #-} ...## Program
```haskell
{-# LANGUAGE UnliftedNewtypes #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE PolyKinds #-}
import GHC.Exts
newtype Id (a :: TYPE r) = Id a
foo :: forall r (a :: TYPE r). Id a -> Id a
foo x = x
```
## Output
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20191008:
isUnliftedType
Id a_a1g7 :: TYPE r_a1g6
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2229:10 in ghc:Type
```
## Expected output
```
A levity-polymorphic type is not allowed here:
Type: Id a
Kind: TYPE r
In the type of binder ‘x’
```
The issue seems to be specific to binders of types that are unlifted newtypes.
## Environment
GHC HEAD8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/16900Poor SrcSpan for recursive pattern synonym error message2019-09-05T15:04:27ZRyan ScottPoor SrcSpan for recursive pattern synonym error messageIf you compile this code:
```hs
{-# LANGUAGE PatternSynonyms #-}
module Bug where
pattern P1 = P2
pattern P2 = P1
```
You'll get this error message:
```
$ /opt/ghc/8.6.5/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bu...If you compile this code:
```hs
{-# LANGUAGE PatternSynonyms #-}
module Bug where
pattern P1 = P2
pattern P2 = P1
```
You'll get this error message:
```
$ /opt/ghc/8.6.5/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:1:1: error:
Recursive pattern synonym definition with following bindings:
P1 (defined at Bug.hs:4:1-15)
P2 (defined at Bug.hs:5:1-15)
|
1 | {-# LANGUAGE PatternSynonyms #-}
| ^
```
While the guts of the error message do correctly identify the pattern synonyms involved in the recursive group, the caret points to line one, column one, which has absolutely nothing to do with `P1` or `P2`. A more sensible thing to do would be to emulate the location of this program's error message:
```hs
module Bug where
type P1 = P2
type P2 = P1
```
```
$ /opt/ghc/8.6.5/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:3:1: error:
Cycle in type synonym declarations:
Bug.hs:3:1-12: type P1 = P2
Bug.hs:4:1-12: type P2 = P1
|
3 | type P1 = P2
| ^^^^^^^^^^^^
```
This time, the caret points to the first type synonym declaration involved in the recursive group, which is as reasonable a choice as anything. It would make sense to do the same thing for recursive pattern synonym groups as well.
Patch incoming.8.10.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/16874Silly vertical printing of long argument lists2019-07-20T13:44:08ZAndreas AbelSilly vertical printing of long argument lists# Summary
GHC's pretty printer does not cope well with long argument lists.
Long argument lists do exist in practice, e.g, for records:
https://github.com/agda/agda/blob/83a48d27010d2c292cc42100081a24f8df573688/src/full/Agda/TypeChecki...# Summary
GHC's pretty printer does not cope well with long argument lists.
Long argument lists do exist in practice, e.g, for records:
https://github.com/agda/agda/blob/83a48d27010d2c292cc42100081a24f8df573688/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs#L192-L198
# Steps to reproduce
```haskell
type A = Int
data D = D A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A
test :: D -> D
test (D a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn)
= D a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn
```
The compiler reports:
```
ManyConstructorArgs.hs:5:7: error:
• The constructor ‘D’ should have 41 arguments, but has been given 40
• In the pattern:
D a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
aa
bb
cc
dd
ee
ff
gg
hh
ii
jj
kk
ll
mm
nn
In an equation for ‘test’:
test
(D a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
aa
bb
cc
dd
ee
ff
gg
hh
ii
jj
kk
ll
mm
nn)
= D a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
aa
bb
cc
dd
ee
ff
gg
hh
ii
jj
kk
ll
mm
nn
|
5 | test (D a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
# Expected behavior
Print argument list in horizontal mode and wrap it somewhere.
# Environment
* GHC version used: 8.6.48.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/16829Error messages could suggest UnliftedNewtypes in more situations2019-06-23T23:21:41ZRyan ScottError messages could suggest UnliftedNewtypes in more situationsConsider the following program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import GHC.Exts
newtype T :: TYPE IntRep where
MkT :: Int# -> T
```
T...Consider the following program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import GHC.Exts
newtype T :: TYPE IntRep where
MkT :: Int# -> T
```
This fails to compile with the following message:
```
GHCi, version 8.9.0.20190614: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:9:1: error:
• Kind signature on data type declaration has non-* return kind
TYPE 'IntRep
• In the newtype declaration for ‘T’
|
9 | newtype T :: TYPE IntRep where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
It took me a while before I realized what was wrong: I had simply forgotten to enable `UnliftedNewtypes`. I would have been spared some frustration if only GHC had just suggested "`Perhaps you intended to use UnliftedNewtypes`", as it usually does whenever one tries to use a feature that is gated on some language extension. This shouldn't be too difficult to arrange.8.10.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/16805Error message for `-Wunused-packages` is obnoxiously long2019-06-27T19:18:25ZMatthew PickeringError message for `-Wunused-packages` is obnoxiously longThe error message for `-Wunused-packages` is much longer than 80 characters which leads to ugly wrapping on a reasonably sized terminal.
![2019-06-12-102308_959x163_scrot](/uploads/a2809fa9aa5e7abf7d8574f396d10067/2019-06-12-102308_959...The error message for `-Wunused-packages` is much longer than 80 characters which leads to ugly wrapping on a reasonably sized terminal.
![2019-06-12-102308_959x163_scrot](/uploads/a2809fa9aa5e7abf7d8574f396d10067/2019-06-12-102308_959x163_scrot.png)8.10.1Alex DAlex Dhttps://gitlab.haskell.org/ghc/ghc/-/issues/16610Incorrect error message for a pragma on an invalid instance method.2019-06-12T10:14:41ZGalen HuntingtonIncorrect error message for a pragma on an invalid instance method.Compiling this code
```haskell
data Foo = Foo
instance Eq Foo where
{-# INLINE wrong #-}
wrong _ = True
```
I get these errors:
```
foo.hs:3:14: error:
The INLINE pragma for ‘wrong’ lacks an accompanying binding
|
3 | {-# ...Compiling this code
```haskell
data Foo = Foo
instance Eq Foo where
{-# INLINE wrong #-}
wrong _ = True
```
I get these errors:
```
foo.hs:3:14: error:
The INLINE pragma for ‘wrong’ lacks an accompanying binding
|
3 | {-# INLINE wrong #-}
| ^^^^^
foo.hs:4:3: error: ‘wrong’ is not a (visible) method of class ‘Eq’
|
4 | wrong _ = True
| ^^^^^
```
The first error I see is not really right. There is an accompanying binding, albeit a wrong one.
Of course, the next error shows what the actual problem is, so in practice this may not be a serious issue.
I tested this in GHC 8.6 and the alpha release of 8.8.8.10.1Alex DAlex Dhttps://gitlab.haskell.org/ghc/ghc/-/issues/16427Suggestions from 12087 (fix illegally nested foralls in GADTs) drop some argu...2019-04-26T09:23:19ZBen PriceSuggestions from 12087 (fix illegally nested foralls in GADTs) drop some argumentsThe issue https://ghc.haskell.org/trac/ghc/ticket/12087 led to GHC suggesting replacements for malformed GADT constructor types. However, it appears that the suggestions are incorrect. Consider the GHCi session:
```
GHCi, version 8.9.201...The issue https://ghc.haskell.org/trac/ghc/ticket/12087 led to GHC suggesting replacements for malformed GADT constructor types. However, it appears that the suggestions are incorrect. Consider the GHCi session:
```
GHCi, version 8.9.20190312: https://www.haskell.org/ghc/ :? for help
Prelude> :set -XGADTs
Prelude> data D where C :: Int -> forall b . b -> D
<interactive>:14:14: error:
• GADT constructor type signature cannot contain nested ‘forall’s or contexts
Suggestion: instead use this type signature: C :: forall b. b -> D
• In the definition of data constructor ‘C’
In the data type declaration for ‘D’
```
It seems that GHC has dropped the Int argument. Should it not suggest `C :: forall b . Int -> b -> D` ?
Similarly, for `data D where C :: forall a . Int -> forall b . b -> D`, it suggests `C :: forall a b. b -> D` rather than `C :: forall a b . Int -> b -> D`8.10.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/16411Inconsistent -Wpartial-fields warnings with (~) vs. (~~)2019-07-07T18:00:12ZRyan ScottInconsistent -Wpartial-fields warnings with (~) vs. (~~)In this program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wpartial-fields #-}
module Bug where
import Data.Type.Equality
data T1 z where
MkT1a :: { rec1 :: () } -> T1 Int
MkT1b :: (z ~ Bool) => ...In this program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wpartial-fields #-}
module Bug where
import Data.Type.Equality
data T1 z where
MkT1a :: { rec1 :: () } -> T1 Int
MkT1b :: (z ~ Bool) => T1 z
data T2 z where
MkT2a :: { rec2 :: () } -> T2 Int
MkT2b :: (z ~~ Bool) => T2 z
```
I get no `-Wpartial-fields`–related warnings for `rec1`, but I do for `rec2`:
```
GHCi, version 8.6.4: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:14: warning: [-Wpartial-fields]
Use of partial record field selector: ‘rec2’
|
13 | MkT2a :: { rec2 :: () } -> T2 Int
| ^^^^
```
This feels strangely inconsistent, since if GHC doesn't warn for `rec1`, which uses `(~)`, then I feel like it shouldn't warn for `rec2` either, as the only difference is that the surrounding constructor uses a slightly different equality constraint `(~~)`.
The reason this happens is because the `dataConCannotMatch` function has special reasoning for `(~)`, but not `(~~)`. Patch incoming.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.4 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Inconsistent -Wpartial-fields warnings with (~) vs. (~~)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In this program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# OPTIONS_GHC -Wpartial-fields #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ndata T1 z where\r\n MkT1a :: { rec1 :: () } -> T1 Int\r\n MkT1b :: (z ~ Bool) => T1 z\r\n\r\ndata T2 z where\r\n MkT2a :: { rec2 :: () } -> T2 Int\r\n MkT2b :: (z ~~ Bool) => T2 z\r\n}}}\r\n\r\nI get no `-Wpartial-fields`–related warnings for `rec1`, but I do for `rec2`:\r\n\r\n{{{\r\nGHCi, version 8.6.4: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:14: warning: [-Wpartial-fields]\r\n Use of partial record field selector: ‘rec2’\r\n |\r\n13 | MkT2a :: { rec2 :: () } -> T2 Int\r\n | ^^^^\r\n}}}\r\n\r\nThis feels strangely inconsistent, since if GHC doesn't warn for `rec1`, which uses `(~)`, then I feel like it shouldn't warn for `rec2` either, as the only difference is that the surrounding constructor uses a slightly different equality constraint `(~~)`.\r\n\r\nThe reason this happens is because the `dataConCannotMatch` function has special reasoning for `(~)`, but not `(~~)`. Patch incoming.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/16385Lousy error message for `instance forall c. c`2019-07-07T18:00:18ZRyan ScottLousy error message for `instance forall c. c`This erroneous program is rejected with a rather strange error message:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
instance forall c. c
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug...This erroneous program is rejected with a rather strange error message:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
instance forall c. c
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:4:20: error: Not in scope: type variable ‘c’
|
4 | instance forall c. c
| ^
```
This error message is hogwash, since `c` is absolutely in scope. The reason GHC believes that `c` is out of scope is because before GHC renamed the type signature in the instance, it performs a pass over all top-level binders in `RnNames.getLocalNonValBinders` to obtain their `Name`s. In particular, [this](https://gitlab.haskell.org/ghc/ghc/blob/473632d7671619ee08a2a0025aa22bd4f79eca2d/compiler/rename/RnNames.hs#L734-743) is the culprit:
```hs
new_assoc overload_ok (L _ (ClsInstD _ (ClsInstDecl { cid_poly_ty = inst_ty
, cid_datafam_insts = adts })))
| Just (L loc cls_rdr) <- getLHsInstDeclClass_maybe inst_ty
= do { cls_nm <- setSrcSpan loc $ lookupGlobalOccRn cls_rdr
; (avails, fldss)
<- mapAndUnzipM (new_loc_di overload_ok (Just cls_nm)) adts
; return (avails, concat fldss) }
| otherwise
= return ([], []) -- Do not crash on ill-formed instances
-- Eg instance !Show Int Trac #3811c
```
Notice the use of `lookupGlobalOccRn` there. Since this code just tunnels into the instance type signature (using `getLHsInstDeclClass_maybe`) without binding any type variables, this calls `lookupGlobalOcc` on an unbound type variable `c`. Eek.
I believe the fix would be to use `lookupGlobalOccRn_maybe` instead and simply default to `return ([], [])` in the event that `lookupGlobalOccRn_maybe` returns Nothing.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Lousy error message for `instance forall c. c`","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This erroneous program is rejected with a rather strange error message:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\nmodule Bug where\r\n\r\ninstance forall c. c\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:20: error: Not in scope: type variable ‘c’\r\n |\r\n4 | instance forall c. c\r\n | ^\r\n}}}\r\n\r\nThis error message is hogwash, since `c` is absolutely in scope. The reason GHC believes that `c` is out of scope is because before GHC renamed the type signature in the instance, it performs a pass over all top-level binders in `RnNames.getLocalNonValBinders` to obtain their `Name`s. In particular, [https://gitlab.haskell.org/ghc/ghc/blob/473632d7671619ee08a2a0025aa22bd4f79eca2d/compiler/rename/RnNames.hs#L734-743 this] is the culprit:\r\n\r\n{{{#!hs\r\n new_assoc overload_ok (L _ (ClsInstD _ (ClsInstDecl { cid_poly_ty = inst_ty\r\n , cid_datafam_insts = adts })))\r\n | Just (L loc cls_rdr) <- getLHsInstDeclClass_maybe inst_ty\r\n = do { cls_nm <- setSrcSpan loc $ lookupGlobalOccRn cls_rdr\r\n ; (avails, fldss)\r\n <- mapAndUnzipM (new_loc_di overload_ok (Just cls_nm)) adts\r\n ; return (avails, concat fldss) }\r\n | otherwise\r\n = return ([], []) -- Do not crash on ill-formed instances\r\n -- Eg instance !Show Int Trac #3811c\r\n}}}\r\n\r\nNotice the use of `lookupGlobalOccRn` there. Since this code just tunnels into the instance type signature (using `getLHsInstDeclClass_maybe`) without binding any type variables, this calls `lookupGlobalOcc` on an unbound type variable `c`. Eek.\r\n\r\nI believe the fix would be to use `lookupGlobalOccRn_maybe` instead and simply default to `return ([], [])` in the event that `lookupGlobalOccRn_maybe` returns Nothing.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/16261[] interpreted as an overloaded list in rule LHS2019-07-07T18:00:46ZDavid Feuer[] interpreted as an overloaded list in rule LHSCompiling `Data.Set.Internal` produces the following:
```
Data/Set/Internal.hs:958:11: warning: [-Winline-rule-shadowing]
Rule "Set.toAscListBack" may never fire
because rule "Class op fromListN" for ‘GHCExts.fromListN’ might ...Compiling `Data.Set.Internal` produces the following:
```
Data/Set/Internal.hs:958:11: warning: [-Winline-rule-shadowing]
Rule "Set.toAscListBack" may never fire
because rule "Class op fromListN" for ‘GHCExts.fromListN’ might fire first
Probable fix: add phase [n] or [~n] to the competing rule
|
958 | {-# RULES "Set.toAscListBack" [1] foldrFB (:) [] = toAscList #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Data/Set/Internal.hs:960:11: warning: [-Winline-rule-shadowing]
Rule "Set.toDescListBack" may never fire
because rule "Class op fromListN" for ‘GHCExts.fromListN’ might fire first
Probable fix: add phase [n] or [~n] to the competing rule
|
960 | {-# RULES "Set.toDescListBack" [1] foldlFB (\xs x -> x : xs) [] = toDescList #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
As mpickering figured out, the trouble is that `[]` in the rule LHS is being interpreted as an overloaded list. The module does *not* enable `OverloadedLists`. Furthermore, even if it *did*, I would argue that it is *never* correct to put one in a rule LHS, so we should always interpret `[]` as the empty list constructor in `RULES` left-hand sides.8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15872Odd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)2019-07-07T18:02:37ZIcelandjackOdd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)Maybe indicative of deeper issues:
```hs
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data WHICH = OP | OPOP
data Fun :: forall (a :: WHICH). a ~ OP ...Maybe indicative of deeper issues:
```hs
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data WHICH = OP | OPOP
data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
MkFun :: (a -> b) -> Fun a b
```
There are some artifacts `Fun ('GHC.Type.Eq# <>)` in the type of `MkFun` that shouldn't be there
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci ~/hs/655_bug.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/655_bug.hs, interpreted )
Ok, one module loaded.
*Main> :t MkFun
MkFun :: (a -> b) -> Fun ('GHC.Types.Eq# <>) a b
*Main> :k Fun
Fun :: (a ~ 'OP) => * -> * -> *
*Main>
```
----
Tangent: Omitting `{-# Language GADTs #-}` we get the term "equational constraint" which is not the term I have seen in the wild
```
$ latestbug 655_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 655_bug.hs, interpreted )
655_bug.hs:9:1: error:
Illegal equational constraint a ~ 'OP
(Use GADTs or TypeFamilies to permit this)
|
9 | data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Odd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Maybe indicative of deeper issues:\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language DataKinds #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata WHICH = OP | OPOP\r\n\r\ndata Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where\r\n MkFun :: (a -> b) -> Fun a b\r\n}}}\r\n\r\nThere are some artifacts `Fun ('GHC.Type.Eq# <>)` in the type of `MkFun` that shouldn't be there\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci ~/hs/655_bug.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/655_bug.hs, interpreted )\r\nOk, one module loaded.\r\n*Main> :t MkFun\r\nMkFun :: (a -> b) -> Fun ('GHC.Types.Eq# <>) a b\r\n*Main> :k Fun\r\nFun :: (a ~ 'OP) => * -> * -> *\r\n*Main>\r\n}}}\r\n\r\n----\r\n\r\nTangent: Omitting `{-# Language GADTs #-}` we get the term \"equational constraint\" which is not the term I have seen in the wild\r\n\r\n{{{\r\n$ latestbug 655_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 655_bug.hs, interpreted )\r\n\r\n655_bug.hs:9:1: error:\r\n Illegal equational constraint a ~ 'OP\r\n (Use GADTs or TypeFamilies to permit this)\r\n |\r\n9 | data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\nFailed, no modules loaded.\r\nPrelude>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15839DerivingStrategies defaulting warning has no associated enable/suppress flag2019-09-25T17:58:18ZAkhra GannonDerivingStrategies defaulting warning has no associated enable/suppress flagWhen `DeriveAnyClass` and `GeneralizedNewtypeDeriving` are enabled together, an instance that could be derived with either one defaults to `DeriveAnyClass` and throws a warning to that effect. There is currently no flag to suppress that ...When `DeriveAnyClass` and `GeneralizedNewtypeDeriving` are enabled together, an instance that could be derived with either one defaults to `DeriveAnyClass` and throws a warning to that effect. There is currently no flag to suppress that warning (it appears even with `-w`).
In the presence of `DerivingStrategies`, it seems desirable to be able to suppress this.
Proposed flag to control it: `-Wderiving-defaults`, after the pattern of `-Wtype-defaults`.
This flag should be part of the default warning set, as without `DerivingStrategies` it remains a bad idea to have both newtype and anyclass active.
Minimal example (thanks RyanGIScott):
```
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Bug where
class C a
newtype T a = MkT a deriving C
```
```
$ /opt/ghc/8.6.1/bin/ghci Bug.hs
GHCi, version 8.6.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:6:30: warning:
• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled
Defaulting to the DeriveAnyClass strategy for instantiating C
• In the newtype declaration for ‘T’
|
6 | newtype T a = MkT a deriving C
| ^
Ok, one module loaded.
```8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15831DerivingVia allows bogus implicit quantification in `via` type2019-07-26T10:41:30ZRyan ScottDerivingVia allows bogus implicit quantification in `via` typeConsider the following code:
```hs
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
import Data.Functor.Const (Const(..))
import GHC.Exts (Any)
newtype Age = MkAge Int
deriving Eq
via Const Int Any
```
T...Consider the following code:
```hs
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE PolyKinds #-}
module Bug where
import Data.Functor.Const (Const(..))
import GHC.Exts (Any)
newtype Age = MkAge Int
deriving Eq
via Const Int Any
```
This fails to compile with a spectacularly unhelpful error message:
```
$ /opt/ghc/8.6.1/bin/ghc -ddump-deriv Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
==================== Derived instances ====================
Derived class instances:
instance GHC.Classes.Eq Bug.Age where
(GHC.Classes.==)
= GHC.Prim.coerce
@((Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
-> (Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
-> GHC.Types.Bool)
@(Bug.Age -> Bug.Age -> GHC.Types.Bool)
(GHC.Classes.==) ::
Bug.Age -> Bug.Age -> GHC.Types.Bool
(GHC.Classes./=)
= GHC.Prim.coerce
@((Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
-> (Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)
-> GHC.Types.Bool)
@(Bug.Age -> Bug.Age -> GHC.Types.Bool)
(GHC.Classes./=) ::
Bug.Age -> Bug.Age -> GHC.Types.Bool
Derived type family instances:
Bug.hs:9:12: error:
The exact Name ‘k’ is not in scope
Probable cause: you used a unique Template Haskell name (NameU),
perhaps via newName, but did not bind it
If that's it, then -ddump-splices might be useful
|
9 | deriving Eq
| ^^
Bug.hs:9:12: error:
The exact Name ‘k’ is not in scope
Probable cause: you used a unique Template Haskell name (NameU),
perhaps via newName, but did not bind it
If that's it, then -ddump-splices might be useful
|
9 | deriving Eq
| ^^
Bug.hs:9:12: error:
The exact Name ‘k’ is not in scope
Probable cause: you used a unique Template Haskell name (NameU),
perhaps via newName, but did not bind it
If that's it, then -ddump-splices might be useful
|
9 | deriving Eq
| ^^
Bug.hs:9:12: error:
The exact Name ‘k’ is not in scope
Probable cause: you used a unique Template Haskell name (NameU),
perhaps via newName, but did not bind it
If that's it, then -ddump-splices might be useful
|
9 | deriving Eq
| ^^
```
There are two things that are strange here:
- Notice that in the derived `Eq` instance, there are references to `(GHC.Types.Any :: k_a24l)`, where `k_a24l` is completely free! This should never happen, and is almost surely the cause of the resulting volley of errors.
- It's quite odd that we didn't reject this `deriving` clause outright //before// generating the derived code. In fact, if we explicitly mention the kind `k`:
```hs
newtype Age = MkAge Int
deriving Eq
via Const Int (Any :: k)
```
> //Then// it's rejected properly:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:12: error:
Type variable ‘k’ is bound in the ‘via’ type ‘Const Int (Any :: k)’
but is not mentioned in the derived class ‘Eq’, which is illegal
|
9 | deriving Eq
| ^^
```
> Something about implicit quantification must be sneaking by this validity check.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"DerivingVia allows bogus implicit quantification in `via` type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["deriving"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DerivingVia #-}\r\n{-# LANGUAGE PolyKinds #-}\r\nmodule Bug where\r\n\r\nimport Data.Functor.Const (Const(..))\r\nimport GHC.Exts (Any)\r\n\r\nnewtype Age = MkAge Int\r\n deriving Eq\r\n via Const Int Any\r\n}}}\r\n\r\nThis fails to compile with a spectacularly unhelpful error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc -ddump-deriv Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance GHC.Classes.Eq Bug.Age where\r\n (GHC.Classes.==)\r\n = GHC.Prim.coerce\r\n @((Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)\r\n -> (Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)\r\n -> GHC.Types.Bool)\r\n @(Bug.Age -> Bug.Age -> GHC.Types.Bool)\r\n (GHC.Classes.==) ::\r\n Bug.Age -> Bug.Age -> GHC.Types.Bool\r\n (GHC.Classes./=)\r\n = GHC.Prim.coerce\r\n @((Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)\r\n -> (Data.Functor.Const.Const GHC.Types.Int (GHC.Types.Any :: k_a24l) :: TYPE GHC.Types.LiftedRep)\r\n -> GHC.Types.Bool)\r\n @(Bug.Age -> Bug.Age -> GHC.Types.Bool)\r\n (GHC.Classes./=) ::\r\n Bug.Age -> Bug.Age -> GHC.Types.Bool\r\n \r\n\r\nDerived type family instances:\r\n\r\n\r\n\r\nBug.hs:9:12: error:\r\n The exact Name ‘k’ is not in scope\r\n Probable cause: you used a unique Template Haskell name (NameU), \r\n perhaps via newName, but did not bind it\r\n If that's it, then -ddump-splices might be useful\r\n |\r\n9 | deriving Eq\r\n | ^^\r\n\r\nBug.hs:9:12: error:\r\n The exact Name ‘k’ is not in scope\r\n Probable cause: you used a unique Template Haskell name (NameU), \r\n perhaps via newName, but did not bind it\r\n If that's it, then -ddump-splices might be useful\r\n |\r\n9 | deriving Eq\r\n | ^^\r\n\r\nBug.hs:9:12: error:\r\n The exact Name ‘k’ is not in scope\r\n Probable cause: you used a unique Template Haskell name (NameU), \r\n perhaps via newName, but did not bind it\r\n If that's it, then -ddump-splices might be useful\r\n |\r\n9 | deriving Eq\r\n | ^^\r\n\r\nBug.hs:9:12: error:\r\n The exact Name ‘k’ is not in scope\r\n Probable cause: you used a unique Template Haskell name (NameU), \r\n perhaps via newName, but did not bind it\r\n If that's it, then -ddump-splices might be useful\r\n |\r\n9 | deriving Eq\r\n | ^^\r\n}}}\r\n\r\nThere are two things that are strange here:\r\n\r\n* Notice that in the derived `Eq` instance, there are references to `(GHC.Types.Any :: k_a24l)`, where `k_a24l` is completely free! This should never happen, and is almost surely the cause of the resulting volley of errors.\r\n* It's quite odd that we didn't reject this `deriving` clause outright //before// generating the derived code. In fact, if we explicitly mention the kind `k`:\r\n\r\n{{{#!hs\r\nnewtype Age = MkAge Int\r\n deriving Eq\r\n via Const Int (Any :: k)\r\n}}}\r\n\r\n //Then// it's rejected properly:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o ) \r\n \r\nBug.hs:9:12: error: \r\n Type variable ‘k’ is bound in the ‘via’ type ‘Const Int (Any :: k)’ \r\n but is not mentioned in the derived class ‘Eq’, which is illegal \r\n | \r\n9 | deriving Eq \r\n | ^^\r\n}}}\r\n\r\n Something about implicit quantification must be sneaking by this validity check.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15753Inconsistent pattern-match warnings when using guards versus case expressions2019-09-18T14:14:54ZRyan ScottInconsistent pattern-match warnings when using guards versus case expressionsConsider the following code (apologies for the rather non-minimal example):
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTyp...Consider the following code (apologies for the rather non-minimal example):
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
module Bug where
import Data.Kind
import Data.Type.Bool
import Data.Type.Equality ((:~:)(..))
import Data.Void
data family Sing :: forall k. k -> Type
data instance Sing :: Bool -> Type where
SFalse :: Sing False
STrue :: Sing True
data instance Sing :: forall a. [a] -> Type where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x:xs)
data instance Sing :: forall a b. (a, b) -> Type where
STuple2 :: Sing x -> Sing y -> Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (f :: k1 ~> k2) @@ (x :: k1) :: k2
infixl 9 @@
newtype Map k v = MkMap [(k, v)]
data instance Sing :: forall k v. Map k v -> Type where
SMkMap :: Sing x -> Sing (MkMap x)
type family MapEmpty :: Map k v where
MapEmpty = MkMap '[]
type family MapInsertWith (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v) :: Map k v where
MapInsertWith _ new_k new_v (MkMap '[]) = MkMap '[ '(new_k, new_v)]
MapInsertWith f new_k new_v (MkMap ('(old_k,old_v):old_kvs)) =
If (old_k == new_k)
(MkMap ('(new_k,f @@ new_v @@ old_v):old_kvs))
(Case (MapInsertWith f new_k new_v (MkMap old_kvs)) old_k old_v)
type family Case (m :: Map k v) (old_k :: k) (old_v :: v) :: Map k v where
Case (MkMap kvs) old_k old_v = MkMap ('(old_k,old_v) : kvs)
sMapInsertWith :: forall k v (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v).
SEq k
=> Sing f -> Sing new_k -> Sing new_v -> Sing m
-> Sing (MapInsertWith f new_k new_v m)
sMapInsertWith _ snew_k snew_v (SMkMap SNil) = SMkMap (STuple2 snew_k snew_v `SCons` SNil)
sMapInsertWith sf snew_k snew_v (SMkMap (STuple2 sold_k sold_v `SCons` sold_kvs)) =
case sold_k %== snew_k of
STrue -> SMkMap (STuple2 snew_k (sf @@ snew_v @@ sold_v) `SCons` sold_kvs)
SFalse ->
case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of
SMkMap skvs -> SMkMap (STuple2 sold_k sold_v `SCons` skvs)
class PEq a where
type (x :: a) == (y :: a) :: Bool
class SEq a where
(%==) :: forall (x :: a) (y :: a).
Sing x -> Sing y -> Sing (x == y)
mapInsertWithNonEmpty1 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])
(new_k :: k) (new_v :: v) (m :: Map k v).
SEq k
=> Sing f -> Sing new_k -> Sing new_v -> Sing m
-> m :~: MkMap ('(old_k,old_v) : old_kvs)
-> MapInsertWith f new_k new_v m :~: MapEmpty
-> Void
mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
| STuple2 sold_k _ `SCons` sold_kvs <- sm
, SFalse <- sold_k %== snew_k
= case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}
mapInsertWithNonEmpty2 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])
(new_k :: k) (new_v :: v) (m :: Map k v).
SEq k
=> Sing f -> Sing new_k -> Sing new_v -> Sing m
-> m :~: MkMap ('(old_k,old_v) : old_kvs)
-> MapInsertWith f new_k new_v m :~: MapEmpty
-> Void
mapInsertWithNonEmpty2 sf snew_k snew_v (SMkMap sm) Refl Refl
| STuple2 sold_k _ `SCons` sold_kvs <- sm
= case sold_k %== snew_k of
SFalse ->
case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}
```
If you compile this with GHC 8.6.1 or later, you'll notice something interesting happening with the pattern-match coverage checker warnings:
```
$ /opt/ghc/8.6.1/bin/ghci Bug.hs
GHCi, version 8.6.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:78:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘mapInsertWithNonEmpty1’:
Patterns not matched: _ _ _ (SMkMap _) Refl Refl
|
78 | mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Ok, one module loaded.
```
`mapInsertWithNonEmpty1` is deemed non-exhaustive, but `mapInsertWithNonEmpty2` is deemed exhaustive. However, the code for the two functions are functionally identical—the only difference is that `mapInsertWithNonEmpty1` uses one more pattern guard than `mapInsertWithNonEmpty2` does.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Inconsistent pattern-match warnings when using guards versus case expressions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["PatternMatchWarnings"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code (apologies for the rather non-minimal example):\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE EmptyCase #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Bool\r\nimport Data.Type.Equality ((:~:)(..))\r\nimport Data.Void\r\n\r\ndata family Sing :: forall k. k -> Type\r\ndata instance Sing :: Bool -> Type where\r\n SFalse :: Sing False\r\n STrue :: Sing True\r\ndata instance Sing :: forall a. [a] -> Type where\r\n SNil :: Sing '[]\r\n SCons :: Sing x -> Sing xs -> Sing (x:xs)\r\ndata instance Sing :: forall a b. (a, b) -> Type where\r\n STuple2 :: Sing x -> Sing y -> Sing '(x, y)\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family (f :: k1 ~> k2) @@ (x :: k1) :: k2\r\ninfixl 9 @@\r\n\r\nnewtype Map k v = MkMap [(k, v)]\r\ndata instance Sing :: forall k v. Map k v -> Type where\r\n SMkMap :: Sing x -> Sing (MkMap x)\r\n\r\ntype family MapEmpty :: Map k v where\r\n MapEmpty = MkMap '[]\r\n\r\ntype family MapInsertWith (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v) :: Map k v where\r\n MapInsertWith _ new_k new_v (MkMap '[]) = MkMap '[ '(new_k, new_v)]\r\n MapInsertWith f new_k new_v (MkMap ('(old_k,old_v):old_kvs)) =\r\n If (old_k == new_k)\r\n (MkMap ('(new_k,f @@ new_v @@ old_v):old_kvs))\r\n (Case (MapInsertWith f new_k new_v (MkMap old_kvs)) old_k old_v)\r\n\r\ntype family Case (m :: Map k v) (old_k :: k) (old_v :: v) :: Map k v where\r\n Case (MkMap kvs) old_k old_v = MkMap ('(old_k,old_v) : kvs)\r\n\r\nsMapInsertWith :: forall k v (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v).\r\n SEq k\r\n => Sing f -> Sing new_k -> Sing new_v -> Sing m\r\n -> Sing (MapInsertWith f new_k new_v m)\r\nsMapInsertWith _ snew_k snew_v (SMkMap SNil) = SMkMap (STuple2 snew_k snew_v `SCons` SNil)\r\nsMapInsertWith sf snew_k snew_v (SMkMap (STuple2 sold_k sold_v `SCons` sold_kvs)) =\r\n case sold_k %== snew_k of\r\n STrue -> SMkMap (STuple2 snew_k (sf @@ snew_v @@ sold_v) `SCons` sold_kvs)\r\n SFalse ->\r\n case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of\r\n SMkMap skvs -> SMkMap (STuple2 sold_k sold_v `SCons` skvs)\r\n\r\nclass PEq a where\r\n type (x :: a) == (y :: a) :: Bool\r\nclass SEq a where\r\n (%==) :: forall (x :: a) (y :: a).\r\n Sing x -> Sing y -> Sing (x == y)\r\n\r\nmapInsertWithNonEmpty1 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])\r\n (new_k :: k) (new_v :: v) (m :: Map k v).\r\n SEq k\r\n => Sing f -> Sing new_k -> Sing new_v -> Sing m\r\n -> m :~: MkMap ('(old_k,old_v) : old_kvs)\r\n -> MapInsertWith f new_k new_v m :~: MapEmpty\r\n -> Void\r\nmapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl\r\n | STuple2 sold_k _ `SCons` sold_kvs <- sm\r\n , SFalse <- sold_k %== snew_k\r\n = case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}\r\n\r\nmapInsertWithNonEmpty2 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])\r\n (new_k :: k) (new_v :: v) (m :: Map k v).\r\n SEq k\r\n => Sing f -> Sing new_k -> Sing new_v -> Sing m\r\n -> m :~: MkMap ('(old_k,old_v) : old_kvs)\r\n -> MapInsertWith f new_k new_v m :~: MapEmpty\r\n -> Void\r\nmapInsertWithNonEmpty2 sf snew_k snew_v (SMkMap sm) Refl Refl\r\n | STuple2 sold_k _ `SCons` sold_kvs <- sm\r\n = case sold_k %== snew_k of\r\n SFalse ->\r\n case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}\r\n}}}\r\n\r\nIf you compile this with GHC 8.6.1 or later, you'll notice something interesting happening with the pattern-match coverage checker warnings:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghci Bug.hs\r\nGHCi, version 8.6.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:78:1: warning: [-Wincomplete-patterns]\r\n Pattern match(es) are non-exhaustive\r\n In an equation for ‘mapInsertWithNonEmpty1’:\r\n Patterns not matched: _ _ _ (SMkMap _) Refl Refl\r\n |\r\n78 | mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\nOk, one module loaded.\r\n}}}\r\n\r\n`mapInsertWithNonEmpty1` is deemed non-exhaustive, but `mapInsertWithNonEmpty2` is deemed exhaustive. However, the code for the two functions are functionally identical—the only difference is that `mapInsertWithNonEmpty1` uses one more pattern guard than `mapInsertWithNonEmpty2` does.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/-/issues/13971Misleading "Kind mis-match on LHS of default declaration" error2020-09-07T14:18:06ZRyan ScottMisleading "Kind mis-match on LHS of default declaration" errorThis program fails to typecheck, unsurprisingly:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
class C a where
type T a :: k
type T a = Int
```
But the error message it gives threw me for a loop i...This program fails to typecheck, unsurprisingly:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
class C a where
type T a :: k
type T a = Int
```
But the error message it gives threw me for a loop initially:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:7:3: error:
• Kind mis-match on LHS of default declaration for ‘T’
• In the default type instance declaration for ‘T’
In the class declaration for ‘C’
|
7 | type T a = Int
| ^^^^^^^^^^^^^^
Failed, 0 modules loaded.
```
The LHS of the default declaration is perfectly fine - the real source of the error is the RHS!
<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":"Misleading \"Kind mis-match on LHS of default declaration\" error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program fails to typecheck, unsurprisingly:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nclass C a where\r\n type T a :: k\r\n type T a = Int\r\n}}}\r\n\r\nBut the error message it gives threw me for a loop initially:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:7:3: error:\r\n • Kind mis-match on LHS of default declaration for ‘T’\r\n • In the default type instance declaration for ‘T’\r\n In the class declaration for ‘C’\r\n |\r\n7 | type T a = Int\r\n | ^^^^^^^^^^^^^^\r\nFailed, 0 modules loaded.\r\n}}}\r\n\r\nThe LHS of the default declaration is perfectly fine - the real source of the error is the RHS!","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/13717Pattern synonym exhaustiveness checks don't play well with EmptyCase2020-09-02T10:19:21ZDavid FeuerPattern synonym exhaustiveness checks don't play well with EmptyCaseIn #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write
```hs
newtype Fin...In #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness checking for matches involving pattern synonyms. Unfortunately, there is still one piece missing: the interaction with `EmptyCase`. Suppose I write
```hs
newtype Fin (n :: Nat) = Fin Natural -- constructor not exported
pattern FZ :: () => n ~ 'S m => Fin n
pattern FS :: () => n ~ 'S m => Fin m -> Fin n
{-# COMPLETE FZ, FS #-}
```
I would very much like to be able to write
```hs
finZAbsurd :: Fin 'Z -> Void
finZAbsurd x = case x of
```
but this gives me a pattern coverage warning! That's certainly not what we want. I believe what we actually want is this:
> When checking empty case, check that *at least one* complete pattern set is impossible.
In this case, it would see two complete pattern sets: the built-in `{Fin}` and the user-decreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching types, we should conclude that the empty case is fine.8.10.1Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/-/issues/13363Wildcard patterns and COMPLETE sets can lead to misleading redundant pattern-...2019-09-17T15:35:35ZRyan ScottWildcard patterns and COMPLETE sets can lead to misleading redundant pattern-match warningsConsider this program:
```hs
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
data Boolean = F | T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGo...Consider this program:
```hs
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
data Boolean = F | T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue <- ((== T) -> True)
where
TooGoodToBeTrue = T
{-# COMPLETE F, TooGoodToBeTrue #-}
catchAll :: Boolean -> Int
catchAll F = 0
catchAll TooGoodToBeTrue = 1
```
This compiles with no warnings with `-Wall`. But if you tweak `catchAll` to add a catch-all case at the end:
```hs
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
data Boolean = F | T
deriving Eq
pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue <- ((== T) -> True)
where
TooGoodToBeTrue = T
{-# COMPLETE F, TooGoodToBeTrue #-}
catchAll :: Boolean -> Int
catchAll F = 0
catchAll TooGoodToBeTrue = 1
catchAll _ = error "impossible"
```
Then if you compile it with `-Wall`, you'll get a very misleading warning:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -Wall
GHCi, version 8.1.20170228: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:1: warning: [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘catchAll’: catchAll TooGoodToBeTrue = ...
|
17 | catchAll TooGoodToBeTrue = 1
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
I would have expected the warning to be on the `catchAll _ = error "impossible"` case!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mpickering |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Wildcarn patterns and COMPLETE sets can lead to misleading redundant pattern-match warnings","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":["mpickering"],"type":"Bug","description":"Consider this program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE ViewPatterns #-}\r\n{-# OPTIONS_GHC -Wincomplete-patterns #-}\r\nmodule Bug where\r\n\r\ndata Boolean = F | T\r\n deriving Eq\r\n\r\npattern TooGoodToBeTrue :: Boolean\r\npattern TooGoodToBeTrue <- ((== T) -> True)\r\n where\r\n TooGoodToBeTrue = T\r\n{-# COMPLETE F, TooGoodToBeTrue #-}\r\n\r\ncatchAll :: Boolean -> Int\r\ncatchAll F = 0\r\ncatchAll TooGoodToBeTrue = 1\r\n}}}\r\n\r\nThis compiles with no warnings with `-Wall`. But if you tweak `catchAll` to add a catch-all case at the end:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PatternSynonyms #-}\r\n{-# LANGUAGE ViewPatterns #-}\r\n{-# OPTIONS_GHC -Wincomplete-patterns #-}\r\nmodule Bug where\r\n\r\ndata Boolean = F | T\r\n deriving Eq\r\n\r\npattern TooGoodToBeTrue :: Boolean\r\npattern TooGoodToBeTrue <- ((== T) -> True)\r\n where\r\n TooGoodToBeTrue = T\r\n{-# COMPLETE F, TooGoodToBeTrue #-}\r\n\r\ncatchAll :: Boolean -> Int\r\ncatchAll F = 0\r\ncatchAll TooGoodToBeTrue = 1\r\ncatchAll _ = error \"impossible\"\r\n}}}\r\n\r\nThen if you compile it with `-Wall`, you'll get a very misleading warning:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -Wall\r\nGHCi, version 8.1.20170228: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:17:1: warning: [-Woverlapping-patterns]\r\n Pattern match is redundant\r\n In an equation for ‘catchAll’: catchAll TooGoodToBeTrue = ...\r\n |\r\n17 | catchAll TooGoodToBeTrue = 1\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI would have expected the warning to be on the `catchAll _ = error \"impossible\"` case!","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/-/issues/12949Pattern coverage checker ignores dictionary arguments2023-03-21T23:48:45ZDavid FeuerPattern coverage checker ignores dictionary argumentsI disabled syntax highlighting below; the bugs highlighting single quotes made the code unreadable.
```
{-# LANGUAGE DataKinds, TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, ConstraintKinds, StandaloneDeriving #-}
{-# OPTIONS...I disabled syntax highlighting below; the bugs highlighting single quotes made the code unreadable.
```
{-# LANGUAGE DataKinds, TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, ConstraintKinds, StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall #-}
import Data.Constraint
import Data.Type.Bool
-- Bool singletons
data Boolly b where
Falsey :: Boolly 'False
Truey :: Boolly 'True
deriving instance Show (Boolly b)
class KnownBool b where
knownBool :: Boolly b
instance KnownBool 'False where
knownBool = Falsey
instance KnownBool 'True where
knownBool = Truey
-- OrRel a b r expresses all the usual implications inherent
-- in the statement that r ~ (a || b).
type OrRel (a :: Bool) (b :: Bool) (r :: Bool) :: Constraint =
(r ~ (a || b),
If r
(If (Not a) (b ~ 'True) (() :: Constraint),
If (Not b) (a ~ 'True) (() :: Constraint))
(a ~ 'False, b ~ 'False))
-- Given known Bools, their disjunction is also known
abr :: forall a b r p1 p2 . (OrRel a b r, KnownBool a, KnownBool b) => p1 a -> p2 b -> Dict (KnownBool r)
abr _ _ = case knownBool :: Boolly a of
Truey -> Dict
Falsey -> case knownBool :: Boolly b of
Truey -> Dict -- Problematic match
Falsey -> Dict
```
The trouble is that GHC warns that the problematic match is redundant, which it is not. If I remove it, GHC *fails* to warn that the patterns are incomplete, which they are.
<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":"Pattern coverage mistake","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":"I disabled syntax highlighting below; the bugs highlighting single quotes made the code unreadable.\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, ConstraintKinds, StandaloneDeriving #-}\r\n{-# OPTIONS_GHC -Wall #-}\r\n\r\nimport Data.Constraint\r\nimport Data.Type.Bool\r\n\r\n-- Bool singletons\r\ndata Boolly b where\r\n Falsey :: Boolly 'False\r\n Truey :: Boolly 'True\r\nderiving instance Show (Boolly b)\r\n\r\nclass KnownBool b where\r\n knownBool :: Boolly b\r\ninstance KnownBool 'False where\r\n knownBool = Falsey\r\ninstance KnownBool 'True where\r\n knownBool = Truey\r\n\r\n-- OrRel a b r expresses all the usual implications inherent\r\n-- in the statement that r ~ (a || b).\r\ntype OrRel (a :: Bool) (b :: Bool) (r :: Bool) :: Constraint =\r\n (r ~ (a || b),\r\n If r\r\n (If (Not a) (b ~ 'True) (() :: Constraint),\r\n If (Not b) (a ~ 'True) (() :: Constraint))\r\n (a ~ 'False, b ~ 'False))\r\n\r\n-- Given known Bools, their disjunction is also known\r\n\r\nabr :: forall a b r p1 p2 . (OrRel a b r, KnownBool a, KnownBool b) => p1 a -> p2 b -> Dict (KnownBool r)\r\nabr _ _ = case knownBool :: Boolly a of\r\n Truey -> Dict\r\n Falsey -> case knownBool :: Boolly b of\r\n Truey -> Dict -- Problematic match\r\n Falsey -> Dict\r\n}}}\r\n\r\nThe trouble is that GHC warns that the problematic match is redundant, which it is not. If I remove it, GHC ''fails'' to warn that the patterns are incomplete, which they are.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1Sebastian GrafSebastian Graf