GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-05-27T10:33:08Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/20311Pattern match warnings suggest internal constructors2022-05-27T10:33:08ZBinderDavidPattern match warnings suggest internal constructors## Summary
The pattern-match exhaustiveness checker displays a list of non-matched constructors which are internal and shouldn't be displayed. I have checked the issues tagged with "pattern match warnings" in the issue tracker and haven...## Summary
The pattern-match exhaustiveness checker displays a list of non-matched constructors which are internal and shouldn't be displayed. I have checked the issues tagged with "pattern match warnings" in the issue tracker and haven't found a similar issue.
## Steps to reproduce
Compile the following snippet with `-Wall` or `-Wincomplete-patterns`.
```haskell
module Compiler where
import Data.Map
type Var = String
data Prim = Mult | Add
data Term = Var Var
| BinaryPrim Term Prim Term
type Heap = Map Var Term
type State = (Heap, Term)
stepVar :: State -> Maybe State
stepVar (h, Var v) = if member v h
then Just (h, h ! v)
else Nothing
```
This produces the following warning:
```
Compiler.hs:17:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘stepVar’:
Patterns not matched:
((Data.Map.Internal.Bin _ _ _ _ _), (BinaryPrim _ _ _))
(Data.Map.Internal.Tip, (BinaryPrim _ _ _))
|
17 | stepVar (h, Var v) = if member v h
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
## Expected behavior
The internal implementation of Map in terms of Tip and Bin should not be made visible to the user. Importing the internal modules and pattern matching on Bin and Tip is almost always the wrong solution, and especially confusing for newcomers.
The expected warning should look like this:
```
Compiler.hs:17:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘stepVar’:
Patterns not matched:
(_, (BinaryPrim _ _ _))
|
17 | stepVar (h, Var v) = if member v h
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
## Environment
* GHC version used: 8.10.4⊥https://gitlab.haskell.org/ghc/ghc/-/issues/16965Error spans of unused imports could be improved2021-02-02T02:29:06ZÖmer Sinan AğacanError spans of unused imports could be improvedExample:
```
compiler/codeGen/StgCmmExpr.hs:44:1: warning: [-Wunused-imports]
The import of ‘primRepSlot’ from module ‘RepType’ is redundant
|
44 | import RepType ( isVoidTy, countConRepArgs, primRepSlot )
| ^^^^^^^^^...Example:
```
compiler/codeGen/StgCmmExpr.hs:44:1: warning: [-Wunused-imports]
The import of ‘primRepSlot’ from module ‘RepType’ is redundant
|
44 | import RepType ( isVoidTy, countConRepArgs, primRepSlot )
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
compiler/codeGen/StgCmmExpr.hs:53:1: warning: [-Wunused-imports]
The import of ‘Data.Function’ is redundant
except perhaps to import instances from ‘Data.Function’
To import instances alone, use: import Data.Function()
|
53 | import Data.Function ( on )
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Second error message is fine, but in the first one the span looks as if the
whole import line is the problem. I think a better error would be:
```
compiler/codeGen/StgCmmExpr.hs:44:54: warning: [-Wunused-imports]
The import of ‘primRepSlot’ from module ‘RepType’ is redundant
|
44 | import RepType ( isVoidTy, countConRepArgs, primRepSlot )
| ^^^^^^^^^^^
```
Now it's clear that only the `primRepSlot` part is the problem.
(Note that in the "improved" error message I also updated the "column" part of
the location)⊥https://gitlab.haskell.org/ghc/ghc/-/issues/16786GHC suggests that infix operators might have the wrong number of arguments2019-07-07T18:00:03ZChris SmithGHC suggests that infix operators might have the wrong number of arguments# Summary
GHC sometimes suggests that you have passed the wrong number of arguments to an infix operator.
# Steps to reproduce
Compile this code with GHC 8.6.5:
answer = map (foo ++ bar) "hello, world"
foo = toUpper
bar ...# Summary
GHC sometimes suggests that you have passed the wrong number of arguments to an infix operator.
# Steps to reproduce
Compile this code with GHC 8.6.5:
answer = map (foo ++ bar) "hello, world"
foo = toUpper
bar = take 10
The first error message says:
Test.hs:1:15: error:
• Couldn't match expected type ‘Char -> b’ with actual type ‘[a1]’
• Possible cause: ‘(++)’ is applied to too many arguments
In the first argument of ‘map’, namely ‘(foo ++ bar)’
In the expression: map (foo ++ bar) "hello, world"
In an equation for ‘answer’:
answer = map (foo ++ bar) "hello, world"
• Relevant bindings include answer :: [b] (bound at Test.hs:1:1)
The suggestion that I have applied (++) to too many arguments is not a very likely one, since infix operators must take two arguments just by their syntax alone. I suppose it's possible that I intended to write an operator section, but it seems like a stretch.
# Expected behavior
I would expect this error message without the suggest that (++) is applied to too many arguments.
# Environment
* GHC version used: 8.6.5⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15931MonoLocalBinds + MonomorphismRestriction prevents generalization for a top le...2019-07-07T18:02:24ZVarun GandhiMonoLocalBinds + MonomorphismRestriction prevents generalization for a top level definitionConsider the following code sample
```haskell
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MonomorphismRestriction #-}
tmp = 10
picker x y = if tmp > 11 then x else y
main = do
print (picker "x" "y")
print (picker 10 11)
```
It fai...Consider the following code sample
```haskell
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MonomorphismRestriction #-}
tmp = 10
picker x y = if tmp > 11 then x else y
main = do
print (picker "x" "y")
print (picker 10 11)
```
It fails with the misleading error message "\* No instance for (Num \[Char\]) arising from the literal \`10'...", from what seems to be an interaction between MonoLocalBinds and MonomorphismRestriction (turn either off and the error goes away).
Should this be happening only for local bindings, or is it correct for this error to occur for top-level definitions too?
In either case, would it be possible to give a better error message here?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"MonoLocalBinds + MonomorphismRestriction prevents generalization for a top level definition","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"⊥","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":["MonoLocalBinds,","MonomorphismRestriction"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code sample\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE MonoLocalBinds #-}\r\n{-# LANGUAGE MonomorphismRestriction #-}\r\ntmp = 10\r\npicker x y = if tmp > 11 then x else y\r\nmain = do\r\n print (picker \"x\" \"y\")\r\n print (picker 10 11)\r\n}}}\r\n\r\nIt fails with the misleading error message \"* No instance for (Num [Char]) arising from the literal `10'...\", from what seems to be an interaction between MonoLocalBinds and MonomorphismRestriction (turn either off and the error goes away).\r\n\r\nShould this be happening only for local bindings, or is it correct for this error to occur for top-level definitions too?\r\n\r\nIn either case, would it be possible to give a better error message here?","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15678Provide the provenance of unification variables in error messages when possible2023-12-14T10:21:25ZRyan ScottProvide the provenance of unification variables in error messages when possibleConsider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:1...Consider the following code:
```hs
module Foo where
x :: Int
x = const 42 _
```
When compiles, this gives the following suggestion:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:4:14: error:
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
• In the second argument of ‘const’, namely ‘_’
In the expression: const 42 _
In an equation for ‘x’: x = const 42 _
• Relevant bindings include x :: Int (bound at Bug.hs:4:1)
Valid hole fits include
x :: Int (bound at Bug.hs:4:1)
otherwise :: Bool
(imported from ‘Prelude’ at Bug.hs:1:8-10
(and originally defined in ‘GHC.Base’))
False :: Bool
(imported from ‘Prelude’ at Bug.hs:1:8-10
(and originally defined in ‘GHC.Types’))
True :: Bool
(imported from ‘Prelude’ at Bug.hs:1:8-10
(and originally defined in ‘GHC.Types’))
lines :: String -> [String]
(imported from ‘Prelude’ at Bug.hs:1:8-10
(and originally defined in ‘base-4.12.0.0:Data.OldList’))
unlines :: [String] -> String
(imported from ‘Prelude’ at Bug.hs:1:8-10
(and originally defined in ‘base-4.12.0.0:Data.OldList’))
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
|
4 | x = const 42 _
| ^
```
One thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.
simonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 -> Int`. Let's report this! Something like:
```
• Found hole: _ :: b0
Where: ‘b0’ is an ambiguous type variable
Arising from an application of
(const 42 :: b0 -> Int)
In the expression: const 42 _
```
This would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | Tritlo |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Provide the provenance of unification variables in error messages when possible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nx :: Int\r\nx = const 42 _\r\n}}}\r\n\r\nWhen compiles, this gives the following suggestion:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:4:14: error:\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n • In the second argument of ‘const’, namely ‘_’\r\n In the expression: const 42 _\r\n In an equation for ‘x’: x = const 42 _\r\n • Relevant bindings include x :: Int (bound at Bug.hs:4:1)\r\n Valid hole fits include\r\n x :: Int (bound at Bug.hs:4:1)\r\n otherwise :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:8-10\r\n (and originally defined in ‘GHC.Base’))\r\n False :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:8-10\r\n (and originally defined in ‘GHC.Types’))\r\n True :: Bool\r\n (imported from ‘Prelude’ at Bug.hs:1:8-10\r\n (and originally defined in ‘GHC.Types’))\r\n lines :: String -> [String]\r\n (imported from ‘Prelude’ at Bug.hs:1:8-10\r\n (and originally defined in ‘base-4.12.0.0:Data.OldList’))\r\n unlines :: [String] -> String\r\n (imported from ‘Prelude’ at Bug.hs:1:8-10\r\n (and originally defined in ‘base-4.12.0.0:Data.OldList’))\r\n (Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)\r\n |\r\n4 | x = const 42 _\r\n | ^\r\n}}}\r\n\r\nOne thing that's rather ugly about this is the use of the type `b0`. What exactly //is// `b0` anyway? The only hint that the error message gives is that it's an ambiguous type variable. But that's not terribly helpful to figure out where `b0` arises from. Ambiguous type variables like this one arise quite frequently when writing Haskell code, and it can often take some sleuthing to figure out why they pop up.\r\n\r\nsimonpj had one suggestion for making ambiguous type variables less confusing: report their provenance whenever possible. There is one notable example of a situation where it's simple to explain from where exactly in the source code a unification variable originates: function applications. In particular, the program above applies the function `const 42` to `_`, which means that the type of `const 42` is instantiated to be `b0 -> Int`. Let's report this! Something like:\r\n\r\n{{{\r\n • Found hole: _ :: b0\r\n Where: ‘b0’ is an ambiguous type variable\r\n Arising from an application of\r\n (const 42 :: b0 -> Int)\r\n In the expression: const 42 _\r\n}}}\r\n\r\nThis would go a long way to clearing up what GHC is thinking when it reports these ambiguous type variable errors. While we can't easily report the provenance of //every// ambiguous type variables, those arising from function applications are quite doable. We might be able to reuse the `CtOrigin` machinery (or take heavy inspiration from it) to accomplish this feat.","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15677Valid hole fits and GADT type variable names2021-09-07T15:56:45ZRyan ScottValid hole fits and GADT type variable namesConsider the following code:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data HList :: [...Consider the following code:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data HList :: [Type] -> Type where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x:xs)
foo :: HList a -> HList a
foo HNil = HNil
foo (HCons (b :: bType) bs) = HCons _ bs
```
Here is the suggestion that the typed hole in `foo` provides:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
Bug.hs:16:37: error:
• Found hole: _ :: x
Where: ‘x’ is a rigid type variable bound by
a pattern with constructor:
HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
in an equation for ‘foo’
at Bug.hs:16:6-26
• In the first argument of ‘HCons’, namely ‘_’
In the expression: HCons _ bs
In an equation for ‘foo’: foo (HCons (b :: bType) bs) = HCons _ bs
• Relevant bindings include
bs :: HList xs (bound at Bug.hs:16:25)
b :: x (bound at Bug.hs:16:13)
foo :: HList a -> HList a (bound at Bug.hs:15:1)
Constraints include a ~ (x : xs) (from Bug.hs:16:6-26)
Valid hole fits include b :: x (bound at Bug.hs:16:13)
|
16 | foo (HCons (b :: bType) bs) = HCons _ bs
| ^
```
One thing immediately stands out here: the hole has type `x`, but `x` appears no where in the definition of `foo`! I had expected this suggestion to mention `bType`, since I went through the effort of declaring `b` to have that type through a pattern signature, but GHC instead uses types from the definition of the `HCons` constructor itself. This seems less than ideal, since one would expect GHC to only ever mention types that are lexically in scope at a particular definition site.
One thing which complicates this idea is that there can be multiple in-scope type variables that all refer to the same type. For instance, if I define this function:
```hs
bar :: HList a -> HList a -> HList a
bar HNil HNil = HNil
bar (HCons (b :: bType) bs) (HCons (c :: cType) cs) = HCons _ bs
```
What should the suggested type of the hole be: `bType`, or `cType`? Either choice is equally valid. After talking with Tritlo and simonpj about this, we came to the consensus that we should just pick one of the type variables to report at the top of the error message:
```
• Found hole: _ :: bType
```
And then later in the message, include any type variable synonyms that have been brought into scope (via pattern signatures or otherwise). I imagine this might look something like:
```
• Type variable synonyms include
`cType` equals `bType`
```
This is quite similar to an existing feature of valid hole fits where we report `Constraints include`. (Indeed, we briefly considered just reporting these type variable synonyms as explicit equality constraints, but doing so would be somewhat misleading, since that's not how pattern signatures actually work in practice.)
One implementation challenge is to figure out how to construct a mapping from `x` to `bType`. One place where inspiration can be drawn from is the `ATyVar` constructor of `TcTyThing`:
```hs
data TcTyThing
= ...
| ATyVar Name TcTyVar -- The type variable to which the lexically scoped type
-- variable is bound. We only need the Name
-- for error-message purposes; it is the corresponding
-- Name in the domain of the envt
```
`ATyVar` already stores a "reverse mapping" of sorts to give better a more accurate `Name` in the event that it is pretty-printed, which is quite similar to what we need to do with `x` and `bType`.
<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 | Tritlo |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Valid hole fits and GADT type variable names","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["GADTs","TypedHoles,"],"differentials":[],"test_case":"","architecture":"","cc":["Tritlo"],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ndata HList :: [Type] -> Type where\r\n HNil :: HList '[]\r\n HCons :: x -> HList xs -> HList (x:xs)\r\n\r\nfoo :: HList a -> HList a\r\nfoo HNil = HNil\r\nfoo (HCons (b :: bType) bs) = HCons _ bs\r\n}}}\r\n\r\nHere is the suggestion that the typed hole in `foo` provides:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Foo ( Bug.hs, Bug.o )\r\n\r\nBug.hs:16:37: error:\r\n • Found hole: _ :: x\r\n Where: ‘x’ is a rigid type variable bound by\r\n a pattern with constructor:\r\n HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),\r\n in an equation for ‘foo’\r\n at Bug.hs:16:6-26\r\n • In the first argument of ‘HCons’, namely ‘_’\r\n In the expression: HCons _ bs\r\n In an equation for ‘foo’: foo (HCons (b :: bType) bs) = HCons _ bs\r\n • Relevant bindings include\r\n bs :: HList xs (bound at Bug.hs:16:25)\r\n b :: x (bound at Bug.hs:16:13)\r\n foo :: HList a -> HList a (bound at Bug.hs:15:1)\r\n Constraints include a ~ (x : xs) (from Bug.hs:16:6-26)\r\n Valid hole fits include b :: x (bound at Bug.hs:16:13)\r\n |\r\n16 | foo (HCons (b :: bType) bs) = HCons _ bs\r\n | ^\r\n}}}\r\n\r\nOne thing immediately stands out here: the hole has type `x`, but `x` appears no where in the definition of `foo`! I had expected this suggestion to mention `bType`, since I went through the effort of declaring `b` to have that type through a pattern signature, but GHC instead uses types from the definition of the `HCons` constructor itself. This seems less than ideal, since one would expect GHC to only ever mention types that are lexically in scope at a particular definition site.\r\n\r\nOne thing which complicates this idea is that there can be multiple in-scope type variables that all refer to the same type. For instance, if I define this function:\r\n\r\n{{{#!hs\r\nbar :: HList a -> HList a -> HList a\r\nbar HNil HNil = HNil\r\nbar (HCons (b :: bType) bs) (HCons (c :: cType) cs) = HCons _ bs\r\n}}}\r\n\r\nWhat should the suggested type of the hole be: `bType`, or `cType`? Either choice is equally valid. After talking with Tritlo and simonpj about this, we came to the consensus that we should just pick one of the type variables to report at the top of the error message:\r\n\r\n{{{\r\n • Found hole: _ :: bType\r\n}}}\r\n\r\nAnd then later in the message, include any type variable synonyms that have been brought into scope (via pattern signatures or otherwise). I imagine this might look something like:\r\n\r\n{{{\r\n • Type variable synonyms include\r\n `cType` equals `bType`\r\n}}}\r\n\r\nThis is quite similar to an existing feature of valid hole fits where we report `Constraints include`. (Indeed, we briefly considered just reporting these type variable synonyms as explicit equality constraints, but doing so would be somewhat misleading, since that's not how pattern signatures actually work in practice.)\r\n\r\nOne implementation challenge is to figure out how to construct a mapping from `x` to `bType`. One place where inspiration can be drawn from is the `ATyVar` constructor of `TcTyThing`:\r\n\r\n{{{#!hs\r\ndata TcTyThing\r\n = ...\r\n | ATyVar Name TcTyVar -- The type variable to which the lexically scoped type\r\n -- variable is bound. We only need the Name\r\n -- for error-message purposes; it is the corresponding\r\n -- Name in the domain of the envt\r\n}}}\r\n\r\n`ATyVar` already stores a \"reverse mapping\" of sorts to give better a more accurate `Name` in the event that it is pretty-printed, which is quite similar to what we need to do with `x` and `bType`.","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15621Error message involving type families points to wrong location2021-09-07T15:55:20ZRyan ScottError message involving type families points to wrong locationConsider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~:...Consider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
```
This doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a non-injective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
|
12 | a = Refl
| ^^^^
```
This claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.
Another interesting facet of this bug is that if you comment out `a`:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let {- a :: F Int :~: F Int
a = Refl -}
b :: F Int :~: F Bool
b = Refl
in ()
```
Then the error message will actually point to `b` this time:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a non-injective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()
|
15 | b = Refl
| ^^^^
```
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Error message involving type families points to wrong location","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let a :: F Int :~: F Int\r\n a = Refl\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThis doesn't typecheck, which isn't surprising, since `F Int` doesn't equal `F Bool` in the definition of `b`. What //is// surprising is where the error message points to:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Int\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a non-injective type family\r\n • In the expression: Refl\r\n In an equation for ‘a’: a = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n |\r\n12 | a = Refl\r\n | ^^^^\r\n}}}\r\n\r\nThis claims that the error message arises from the definition of `a`, which is completely wrong! As evidence, if you comment out `b`, then the program typechecks again.\r\n\r\nAnother interesting facet of this bug is that if you comment out `a`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Type.Equality\r\n\r\ntype family F a\r\n\r\nf :: ()\r\nf =\r\n let {- a :: F Int :~: F Int\r\n a = Refl -}\r\n\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n}}}\r\n\r\nThen the error message will actually point to `b` this time:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Bool :~: F Bool\r\n NB: ‘F’ is a non-injective type family\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n b :: F Int :~: F Bool\r\n b = Refl\r\n in ()\r\n |\r\n15 | b = Refl\r\n | ^^^^\r\n}}}\r\n\r\nThe use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of `F`.\r\n\r\nThis is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:11: error:\r\n • Couldn't match type ‘F Int’ with ‘F Bool’\r\n Expected type: F Int :~: F Bool\r\n Actual type: F Int :~: F Int\r\n NB: ‘F’ is a type function, and may not be injective\r\n • In the expression: Refl\r\n In an equation for ‘b’: b = Refl\r\n In the expression:\r\n let\r\n a :: F Int :~: F Int\r\n a = Refl\r\n b :: F Int :~: F Bool\r\n ....\r\n in ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15596When a type application cannot be applied to an identifier due to the absence...2021-09-07T15:54:40ZkindaroWhen a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!Consider this code:
```hs
{-# language TypeApplications #-}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Com...Consider this code:
```hs
{-# language TypeApplications #-}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 -> a0 -> a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer
|
6 | g = f @Integer
| ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{-# language TypeApplications #-}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 -> a0 -> a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n |\r\n6 | g = f @Integer\r\n | ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/15558Locally handling an empty constraint2019-10-23T15:55:46ZJohn EricsonLocally handling an empty constraintI need something like `\case {}` for constraints. See the code below. The `undefined` won't satisfy the type checker, nor is there anything total I found that would. The dead code warning also bubbled up out of the field incorrectly.
I ...I need something like `\case {}` for constraints. See the code below. The `undefined` won't satisfy the type checker, nor is there anything total I found that would. The dead code warning also bubbled up out of the field incorrectly.
I think this will require new language features tangentially related to Lambdas for `forall`. (Both `forall _.` and `=>` are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means.
```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Asdf where
import Data.Kind
import Data.Type.Equality
data Sing a where
X :: Sing Int
Y :: Sing [Bool]
data Foo a = Foo a (forall b. [b] :~: a -> b)
data Bar a = Bar a (forall b. [b] ~ a => b)
f, f' :: forall a. Sing a -> Foo a
f s = Foo a b
where
a :: a
a = case s of
X -> 0
Y -> []
b :: forall b. [b] :~: a -> b
b = case s of
X -> \case {}
Y -> \Refl -> False
f' = \case
X -> Foo 0 (\case {})
Y -> Foo [] (\Refl -> False)
g, g' :: forall a. Sing a -> Bar a
g s = Bar a b
where
a :: a
a = case s of
X -> 0
Y -> []
b :: forall b. [b] ~ a => b
b = case s of
Y -> False
g' = \case
X -> Bar 0 undefined -- can't make this happy
Y -> Bar [] False
```
⊥