GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-09-25T17:19:16Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/7668Location in -fdefer-type-errors2020-09-25T17:19:16ZKrzysztof GogolewskiLocation in -fdefer-type-errorsConsider
```
x :: Char
x = 'x' + 1
y :: Char
y = 'y' + 1
```
Run `ghci -fdefer-type-errors`:
```
*Main> x
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equa...Consider
```
x :: Char
x = 'x' + 1
y :: Char
y = 'y' + 1
```
Run `ghci -fdefer-type-errors`:
```
*Main> x
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equation for `y': y = 'y' + 1
(deferred type error)
*Main> y
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equation for `y': y = 'y' + 1
(deferred type error)
```
The first exception is wrong. It seems that the missing `Num Char` instance is filled with the same error message in all places where the constraint should be supplied.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.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":"Location in -fdefer-type-errors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n\r\n{{{\r\nx :: Char\r\nx = 'x' + 1\r\n\r\ny :: Char\r\ny = 'y' + 1\r\n}}}\r\n\r\nRun `ghci -fdefer-type-errors`:\r\n\r\n{{{\r\n*Main> x\r\n*** Exception: G.hs:5:9:\r\n No instance for (Num Char) arising from a use of `+'\r\n In the expression: 'y' + 1\r\n In an equation for `y': y = 'y' + 1\r\n(deferred type error)\r\n*Main> y\r\n*** Exception: G.hs:5:9:\r\n No instance for (Num Char) arising from a use of `+'\r\n In the expression: 'y' + 1\r\n In an equation for `y': y = 'y' + 1\r\n(deferred type error)\r\n}}}\r\n\r\nThe first exception is wrong. It seems that the missing `Num Char` instance is filled with the same error message in all places where the constraint should be supplied.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/24024Assertion failure with ghci -fdefer-type-errors2023-11-01T14:47:25ZKrzysztof GogolewskiAssertion failure with ghci -fdefer-type-errorsTo reproduce:
```
$ ./stage1/bin/ghc --interactive
GHCi, version 9.9.20230927: https://www.haskell.org/ghc/ :? for help
ghci> :set -fdefer-type-errors
ghci> :kind Int Int
panic! (the 'impossible' happened)
GHC version 9.9.20230927:
...To reproduce:
```
$ ./stage1/bin/ghc --interactive
GHCi, version 9.9.20230927: https://www.haskell.org/ghc/ :? for help
ghci> :set -fdefer-type-errors
ghci> :kind Int Int
panic! (the 'impossible' happened)
GHC version 9.9.20230927:
ASSERT failed!
{[W] co_aBU
= case typeError
@LiftedRep
@()
"<interactive>:1:1: error: [\ESC]8;;https://errors.haskell.org/messages/GHC-83865\ESC\\GHC-83865\ESC]8;;\ESC\\]\n\
\ \\226\\128\\162 Expected kind \\226\\128\\152* -> k0\\226\\128\\153, but \\226\\128\\152Int\\226\\128\\153 has kind \\226\\128\\152*\\226\\128\\153\n\
\ \\226\\128\\162 In the type \\226\\128\\152Int Int\\226\\128\\153\n\
\(deferred type error)"#
of {}}
Call stack:
CallStack (from HasCallStack):
massertPpr, called at compiler/GHC/Tc/Module.hs:2626:10 in ghc-9.9-inplace:GHC.Tc.Module
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:511:29 in ghc-9.9-inplace:GHC.Utils.Error
```
Even with assertions off we get a rather silly output
```
:set -fdefer-type-errors
ghci> :k Int Int
<interactive>:1:1: warning: [GHC-83865] [-Wdeferred-type-errors]
• Expected kind ‘* -> k0’, but ‘Int’ has kind ‘*’
• In the type ‘Int Int’
Int Int :: k
```9.8.2Krzysztof GogolewskiKrzysztof Gogolewskihttps://gitlab.haskell.org/ghc/ghc/-/issues/24026Core Lint error with -fdefer-type-errors and bad RULE2023-10-03T14:12:23ZKrzysztof GogolewskiCore Lint error with -fdefer-type-errors and bad RULETo reproduce:
```hs
module T24026 where
{-# RULES "f" forall (x :: Bool). f x = 0 #-}
f :: Int -> Int
f x = 0
```
```
$ ghc -dlint -fdefer-type-errors T24026
[1 of 1] Compiling T24026 ( T24026.hs, T24026.o )
*** Core Lint e...To reproduce:
```hs
module T24026 where
{-# RULES "f" forall (x :: Bool). f x = 0 #-}
f :: Int -> Int
f x = 0
```
```
$ ghc -dlint -fdefer-type-errors T24026
[1 of 1] Compiling T24026 ( T24026.hs, T24026.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
T24026.hs:6:1: warning:
The coercion variable co_awP :: Bool ~# Int
[LclId[CoVarId]]
is out of scope
In the RHS of f :: Int -> Int
In a rule attached to f :: Int -> Int
Substitution: <InScope = {}
IdSubst = []
TvSubst = []
CvSubst = []>
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "T24026"#)
f :: Int -> Int
[LclIdX,
RULES: "f" forall (x_awv :: Bool).
f (x_awv `cast` (Sub co_awP :: Bool ~R# Int))
= I# 0#]
f = \ (x_awu :: Int) -> I# 0#
end Rec }
````
The RULE has a type error, the coercion `Int ~ Bool` from `-fdefer-type-errors` is not bound.9.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/22642Allow signatures without a binding2023-07-20T16:15:02ZOleg GrenrusAllow signatures without a bindingIn other words so I can write
```haskell
someFancyFunction :: a -> (forall b. b -> c) -> (a -> b) -> c
```
currently GHC errors
```
Top.hs:3:1: error:
The type signature for ‘someFancyFunction’
lacks an accompanying binding
...In other words so I can write
```haskell
someFancyFunction :: a -> (forall b. b -> c) -> (a -> b) -> c
```
currently GHC errors
```
Top.hs:3:1: error:
The type signature for ‘someFancyFunction’
lacks an accompanying binding
|
3 | someFancyFunction :: a -> (forall b. b -> c) -> (a -> b) -> c
| ^^
```
Though one can simulate the behavior by compiling with `-fdefer-type-errors` and supplying some non-sense implementation:
```haskell
someFancyFunction :: a -> (forall b. b -> c) -> (a -> b) -> c
someFancyFunction = ()
```
An alternative is to write
```haskell
someFancyFunction :: a -> (forall b. b -> c) -> (a -> b) -> c
someFancyFunction x y z = someFancyFunction x y z
```
or
```haskell
someFancyFunction _x _y _z = undefined -- need to eta-expand because of rankN argument
```
But both of these are not great option: it's very easy to leave the "temporary" placeholders into the code base. GHC cannot help to find them. (it can with `-fdefer-type-errors` trick, but that feels roundabout - and does "too much" on the side).
I argue that very similar functionality already exists in GHC: missing type class members and missing record fields are filled by GHC. These issue warnings which can be turned into errors. Missing binding for a signature could also be a warning, which is an error by default. Or it could be a `-f..` flag.
I think it will be very useful for interactive development, so GHC don't error too early.9.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/24413Re-Enable `-fdefer-type-errors` and `-fdefer-out-of-scope-variables` in GHCi2024-02-15T15:43:46ZApoorv IngleRe-Enable `-fdefer-type-errors` and `-fdefer-out-of-scope-variables` in GHCi## Summary
GHCi has `-fdefer-type-errors` and `-fdefer-out-of-scope-variables` was disabled as an adhoc fix to avoid some serious issue #14963.
Now that the real issue is fixed by we should re-enable `-fdefer-type-errors` and `-fdefer-...## Summary
GHCi has `-fdefer-type-errors` and `-fdefer-out-of-scope-variables` was disabled as an adhoc fix to avoid some serious issue #14963.
Now that the real issue is fixed by we should re-enable `-fdefer-type-errors` and `-fdefer-out-of-scope-variables` in GHCi.
More info: https://gitlab.haskell.org/ghc/ghc/-/issues/14963#note_546391
## Steps to reproduce
Check #14963
## Expected behavior
Code snippet in #14963 shouldn't crash
## Environment
* GHC version used: HEADApoorv IngleApoorv Inglehttps://gitlab.haskell.org/ghc/ghc/-/issues/23258-fdefer-typed-holes will raise "(deferred type error)" exception, and that na...2023-06-10T12:20:55Zjwaldmann-fdefer-typed-holes will raise "(deferred type error)" exception, and that name looks wrongwith ghc-9.6.1,
```
:set -fdefer-typed-holes
ghci> x = [True,_] -- gives warning, as expected
ghci> print x
[True,*** Exception: <interactive>:11:11: error: [GHC-88464]
...
(deferred type error)
```
that last line looks wrong to me, s...with ghc-9.6.1,
```
:set -fdefer-typed-holes
ghci> x = [True,_] -- gives warning, as expected
ghci> print x
[True,*** Exception: <interactive>:11:11: error: [GHC-88464]
...
(deferred type error)
```
that last line looks wrong to me, since there is no type error. Documentation says "a hole ... will behave like undefined", and for that I would get no type error.https://gitlab.haskell.org/ghc/ghc/-/issues/23111Core Lint error with -fdefer-type-errors and kind error2023-03-14T15:16:29ZKrzysztof GogolewskiCore Lint error with -fdefer-type-errors and kind errorThe following program fails `ghc -dcore-lint -fdefer-type-errors`
```haskell
{-# LANGUAGE TypeFamilies #-}
module M where
import Data.Kind
type F :: Type
type family F
type G :: F
type family G
x :: G
x = ()
```
<details>
```haske...The following program fails `ghc -dcore-lint -fdefer-type-errors`
```haskell
{-# LANGUAGE TypeFamilies #-}
module M where
import Data.Kind
type F :: Type
type family F
type G :: F
type family G
x :: G
x = ()
```
<details>
```haskell
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
Non-CoVar has coercion type co_awK :: F ~# *
Substitution: <InScope = {}
IdSubst = []
TvSubst = []
CvSubst = []>
*** Offending Program ***
Rec {
co_awK :: F ~# *
[LclId[CoVarId]]
co_awK
= case typeError
@LiftedRep
@()
"M.hs:12:6: error: [GHC-83865]\n\
\ \\226\\128\\162 Expected a type, but \\226\\128\\152G\\226\\128\\153 has kind \\226\\128\\152F\\226\\128\\153\n\
\ \\226\\128\\162 In the type signature: x :: G\n\
\(deferred type error)"#
of wild_00 {
}
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
x :: (G |> co_awK)
[LclIdX]
x = case case typeError
@LiftedRep
@()
"M.hs:13:5: error: [GHC-18872]\n\
\ \\226\\128\\162 Couldn't match kind \\226\\128\\152F\\226\\128\\153 with \\226\\128\\152*\\226\\128\\153\n\
\ When matching types\n\
\ G :: F\n\
\ () :: *\n\
\ \\226\\128\\162 In the expression: ()\n\
\ In an equation for \\226\\128\\152x\\226\\128\\153: x = ()\n\
\(deferred type error)"#
of wild_00 {
}
of co_ayG
{ __DEFAULT ->
case case typeError
@LiftedRep
@()
"M.hs:13:5: error: [GHC-18872]\n\
\ \\226\\128\\162 Couldn't match kind \\226\\128\\152F\\226\\128\\153 with \\226\\128\\152*\\226\\128\\153\n\
\ When matching types\n\
\ G :: F\n\
\ () :: *\n\
\ \\226\\128\\162 In the expression: ()\n\
\ In an equation for \\226\\128\\152x\\226\\128\\153: x = ()\n\
\(deferred type error)"#
of wild_00 {
}
of co_ayH
{ __DEFAULT ->
()
`cast` (Sub (Sym (co_ayH
; Sym (GRefl nominal () (Sym co_ayG)))
; GRefl nominal G co_awK)
:: () ~R# (G |> co_awK))
}
}
end Rec }
```
</details>https://gitlab.haskell.org/ghc/ghc/-/issues/21692Static pointers + defer-type-errors Lint error2022-09-01T15:55:11ZKrzysztof GogolewskiStatic pointers + defer-type-errors Lint errorThis program fails Lint with `-fdefer-type-errors`:
```haskell
{-# LANGUAGE StaticPointers #-}
module T where
import GHC.StaticPtr
p :: StaticPtr Bool
p = static 'a'
```
```
*** Core Lint errors : in result of Desugar (before optimiz...This program fails Lint with `-fdefer-type-errors`:
```haskell
{-# LANGUAGE StaticPointers #-}
module T where
import GHC.StaticPtr
p :: StaticPtr Bool
p = static 'a'
```
```
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
Non-CoVar has coercion type co_avC :: Char ~# Bool
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
co_avC :: Char ~# Bool
[LclId[CoVarId]]
co_avC
= case typeError ...
```
If Lint is disabled, it fails with an assertion failure or a panic.
Related: #18467https://gitlab.haskell.org/ghc/ghc/-/issues/21024A deferred type error inferferes with the monomorphism restriction2022-06-09T14:31:57ZRichard Eisenbergrae@richarde.devA deferred type error inferferes with the monomorphism restrictionHere is a fairly simple program:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where
other = ['a', True]
x = 5
```
The monomorphism restriction is in effect, and note that the two definitions do not refer to each other.
GH...Here is a fairly simple program:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Bug where
other = ['a', True]
x = 5
```
The monomorphism restriction is in effect, and note that the two definitions do not refer to each other.
GHC embarrassingly infers the type `Any` for `x`, affected by the presence of the ill-typed `other`.https://gitlab.haskell.org/ghc/ghc/-/issues/20511Missing module imports could be defered with -fdefer-out-scope-variables?2021-10-19T15:06:03ZMatthew PickeringMissing module imports could be defered with -fdefer-out-scope-variables?If I write a module with a non-existent then you get an error such as:
```
A.hs:3:1: error:
Could not find module ‘FooBaz’
Use -v (or `:set -v` in ghci) to see a list of the files searched for.
|
3 | import FooBaz
| ^^^^^^^^...If I write a module with a non-existent then you get an error such as:
```
A.hs:3:1: error:
Could not find module ‘FooBaz’
Use -v (or `:set -v` in ghci) to see a list of the files searched for.
|
3 | import FooBaz
| ^^^^^^^^^^^^^
```
but if we turn on `-fdefer-out-of-scope-variables` then we might expect that we could continue and get more interesting diagnostics for the rest of the module. A missing module could be thought of as an out-of-scope variable.
One issue with this scheme is that identifiers which would come from this module would then be reported as out-of-scope which could cause additional confusion due to the cascading nature of deferred errors.
What do you think @wz1000 @monoidal ?https://gitlab.haskell.org/ghc/ghc/-/issues/20083Linear types and -fdefer-type-errors2024-02-09T00:47:35ZKrzysztof GogolewskiLinear types and -fdefer-type-errorsLinear types combined with `-fdefer-type-errors` show a poor error message.
```
ghci> :set -XLinearTypes
ghci> ap :: (a -> b) -> a %m -> b; ap f x = f x
<interactive>:2:35: error:
• Couldn't match type ‘m’ with ‘'Many’
aris...Linear types combined with `-fdefer-type-errors` show a poor error message.
```
ghci> :set -XLinearTypes
ghci> ap :: (a -> b) -> a %m -> b; ap f x = f x
<interactive>:2:35: error:
• Couldn't match type ‘m’ with ‘'Many’
arising from multiplicity of ‘x’
‘m’ is a rigid type variable bound by
the type signature for:
ap :: forall a b (m :: GHC.Types.Multiplicity).
(a -> b) -> a %m -> b
at <interactive>:2:1-27
• In an equation for ‘ap’: ap f x = f x
• Relevant bindings include
ap :: (a -> b) -> a %m -> b (bound at <interactive>:2:30)
ghci> :set -fdefer-type-errors
ghci> ap :: (a -> b) -> a %m -> b; ap f x = f x
<interactive>:4:30: error:
Multiplicity coercions are currently not supported (see GHC #19517)
<interactive>:4:30: error:
Multiplicity coercions are currently not supported (see GHC #19517)
```
The error message is technically correct, but `-fdefer-type-errors` downgrades the type mismatch to a warning. The warning is not shown, while it contains important information.
Until #19517 is done, when `-fdefer-type-errors` is on, we should compile multiplicity coercions to runtime errors and convert the error to a warning.
Also make the message more user-friendly.https://gitlab.haskell.org/ghc/ghc/-/issues/19966Out-of-scope variables not deferred with type constructors2021-06-11T21:00:38ZKrzysztof GogolewskiOut-of-scope variables not deferred with type constructorsIn HEAD, `-fdefer-out-of-scope-variables` can no longer defer an out-of-scope identifier if it exists on the type level.
```
ghci> :set -fdefer-out-of-scope-variables
ghci> x = I
<interactive>:2:5: warning: [-Wdeferred-out-of-scope-va...In HEAD, `-fdefer-out-of-scope-variables` can no longer defer an out-of-scope identifier if it exists on the type level.
```
ghci> :set -fdefer-out-of-scope-variables
ghci> x = I
<interactive>:2:5: warning: [-Wdeferred-out-of-scope-variables]
Data constructor not in scope: I
ghci> x = IO
<interactive>:3:5: error:
• Illegal term-level use of the type constructor ‘IO’
imported from ‘Prelude’ (and originally defined in ‘GHC.Types’)
• In the expression: IO
In an equation for ‘x’: x = IO
```
In 9.0, `x = IO` behaves the same as `x = I`.
With Dependent Haskell we might ultimately allow `x = IO` to mean the type constructor, but the current situation is a bit inconsistent.
Low priority. Related: #17102.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/18636RebindableSyntax cannot defer-out-of-scope-variables2021-02-16T21:02:59ZRichard Eisenbergrae@richarde.devRebindableSyntax cannot defer-out-of-scope-variablesWhen I say
```hs
{-# LANGUAGE RebindableSyntax #-}
{-# OPTIONS_GHC -fdefer-out-of-scope-variables #-}
module Bug where
foo = 5
```
I get
```
Bug.hs:6:7: error: Not in scope: ‘fromInteger’
```
But I told GHC to defer such errors!
N...When I say
```hs
{-# LANGUAGE RebindableSyntax #-}
{-# OPTIONS_GHC -fdefer-out-of-scope-variables #-}
module Bug where
foo = 5
```
I get
```
Bug.hs:6:7: error: Not in scope: ‘fromInteger’
```
But I told GHC to defer such errors!
Nobody is really asking for this (I was just trying to abuse GHC for fun), but I think it should be very very easy to implement.https://gitlab.haskell.org/ghc/ghc/-/issues/17102-fdefer-out-of-scope-variables should also defer ambiguous occurrences2021-10-14T09:23:15ZChris Smith-fdefer-out-of-scope-variables should also defer ambiguous occurrences## Motivation
Use of `-fdefer-out-of-scope-variables` indicates that a user wants to keep trying to run code even if the variable names cannot be resolved. But there's one case where GHC doesn't live up to that intent.
import Prel...## Motivation
Use of `-fdefer-out-of-scope-variables` indicates that a user wants to keep trying to run code even if the variable names cannot be resolved. But there's one case where GHC doesn't live up to that intent.
import Prelude
head = "^-^"
main = print head
GHC says:
$ ghc -fdefer-out-of-scope-variables Test.hs
[1 of 1] Compiling Main ( Test.hs, Test.o )
Test.hs:3:14: error:
Ambiguous occurrence ‘head’
It could refer to either ‘Prelude.head’,
imported from ‘Prelude’ at Test.hs:1:1-14
(and originally defined in ‘GHC.List’)
or ‘Main.head’, defined at Test.hs:2:1
and fails to load the module
## Proposal
I believe this should successfully load the module, but fail at runtime because `head` couldn't be resolved.https://gitlab.haskell.org/ghc/ghc/-/issues/14722Error message points to wrong location2021-08-31T13:33:47ZIcelandjackError message points to wrong locationThis rightly fails, but I have an issue with the error message. I think points to the visible type application eagerly.. rather than the type annotation `(f_xx :: ())`.
```hs
{-# Language RankNTypes, PolyKinds, GADTs, TypeApplications, ...This rightly fails, but I have an issue with the error message. I think points to the visible type application eagerly.. rather than the type annotation `(f_xx :: ())`.
```hs
{-# Language RankNTypes, PolyKinds, GADTs, TypeApplications, ScopedTypeVariables #-}
import Data.Kind
newtype Limit :: (k -> Type) -> Type where
Limit :: (forall xx. f xx) -> Limit f
foo :: forall f a. Limit f -> f a
foo (Limit (f_xx :: ())) = f_xx @a
```
gives
```
$ ghci -ignore-dot-ghci /tmp/Test.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Test.hs, interpreted )
/tmp/Test.hs:9:28: error:
• Cannot apply expression of type ‘()’
to a visible type argument ‘a’
• In the expression: f_xx @a
In an equation for ‘foo’: foo (Limit (f_xx :: ())) = f_xx @a
|
9 | foo (Limit (f_xx :: ())) = f_xx @a
| ^^^^^^^
Failed, no modules loaded.
Prelude>
```
I would have expected:
```
/tmp/Test.hs:9:13: error:
• Couldn't match expected type ‘()’ with actual type ‘f xx0’
• When checking that the pattern signature: ()
fits the type of its context: forall (xx :: k1). f xx
In the pattern: f_xx :: ()
In the pattern: Limit (f_xx :: ())
• Relevant bindings include
foo :: Limit f -> f a (bound at /tmp/Test.hs:9:1)
```
Thoughts
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.5 |
| 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":"Error message points to wrong location","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"This rightly fails, but I have an issue with the error message. I think points to the visible type application eagerly.. rather than the type annotation `(f_xx :: ())`.\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes, PolyKinds, GADTs, TypeApplications, ScopedTypeVariables #-}\r\n\r\nimport Data.Kind\r\n\r\nnewtype Limit :: (k -> Type) -> Type where\r\n Limit :: (forall xx. f xx) -> Limit f\r\n\r\nfoo :: forall f a. Limit f -> f a\r\nfoo (Limit (f_xx :: ())) = f_xx @a\r\n}}}\r\n\r\ngives \r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci /tmp/Test.hs \r\nGHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Test.hs, interpreted )\r\n\r\n/tmp/Test.hs:9:28: error:\r\n • Cannot apply expression of type ‘()’\r\n to a visible type argument ‘a’\r\n • In the expression: f_xx @a\r\n In an equation for ‘foo’: foo (Limit (f_xx :: ())) = f_xx @a\r\n |\r\n9 | foo (Limit (f_xx :: ())) = f_xx @a\r\n | ^^^^^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nI would have expected:\r\n\r\n{{{\r\n/tmp/Test.hs:9:13: error:\r\n • Couldn't match expected type ‘()’ with actual type ‘f xx0’\r\n • When checking that the pattern signature: ()\r\n fits the type of its context: forall (xx :: k1). f xx\r\n In the pattern: f_xx :: ()\r\n In the pattern: Limit (f_xx :: ())\r\n • Relevant bindings include\r\n foo :: Limit f -> f a (bound at /tmp/Test.hs:9:1)\r\n}}}\r\n\r\nThoughts","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14370improve documentation of -fdefer-typed-holes for naked expressions in ghci2023-04-13T23:16:33ZBertram Felgenhauerimprove documentation of -fdefer-typed-holes for naked expressions in ghciConsider the following ghci session.
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -fdefer-typed-holes -Wno-typed-holes
Prelude> :set -fdefer-out-of-scope-variables -Wno-deferred-out-of-scope-variables
...Consider the following ghci session.
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -fdefer-typed-holes -Wno-typed-holes
Prelude> :set -fdefer-out-of-scope-variables -Wno-deferred-out-of-scope-variables
Prelude> let x = [_]; y = [r]
Prelude> (length x, length y)
(1,1)
Prelude> length [_]
<interactive>:4:9: error:
• Found hole: _ :: a0
Where: ‘a0’ is an ambiguous type variable
• In the expression: _
In the first argument of ‘length’, namely ‘[_]’
In the expression: length [_]
• Relevant bindings include it :: Int (bound at <interactive>:4:1)
Prelude> length [r]
1
```
Why does the `length [_]` expression produce a type error immediately instead of being deferred?
\~\~(I've asked the same question in #14367 but this looks like a real bug.)\~\~
The documentation can be improved here, see \[\#[ticket:14370\#comment:144137](https://gitlab.haskell.org//ghc/ghc/issues/14370#note_144137) comment 2\]https://gitlab.haskell.org/ghc/ghc/-/issues/11197Overeager deferred type errors2021-08-12T16:45:46ZRichard Eisenbergrae@richarde.devOvereager deferred type errorsWith `TypeInType`, the solver now works in terms of unlifted equality. The only place this matters is in deferred type errors, which now are more eager than they were before. For example:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
mod...With `TypeInType`, the solver now works in terms of unlifted equality. The only place this matters is in deferred type errors, which now are more eager than they were before. For example:
```
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Main where
main = do
putStrLn "Hi there."
putStrLn True
```
This used to print
```
Hi there.
Defer: Defer.hs:7:12: error:
...
```
Now it prints
```
Defer: Defer.hs:7:12: error:
...
```
No more `Hi there.`.
Thinking about Core, this change should be expected. GHC puts all evidence bindings for `main` at the top, and with unlifted equality in the solver, these bindings now contain `case typeError ... of ...`, which forces the type error eagerly. Previously, there was a lazy binding for a lifted equality witness, unpacked only at the last moment by magic in the desugarer, thus the lazier warning.
Simon has proposed customizing the !FloatIn pass to deal with this scenario. I do believe this would work nicely, but I have not yet implemented it.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.11 |
| 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":"Overeager deferred type errors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"With `TypeInType`, the solver now works in terms of unlifted equality. The only place this matters is in deferred type errors, which now are more eager than they were before. For example:\r\n\r\n{{{\r\n{-# OPTIONS_GHC -fdefer-type-errors #-}\r\n\r\nmodule Main where\r\n\r\nmain = do\r\n putStrLn \"Hi there.\"\r\n putStrLn True\r\n}}}\r\n\r\nThis used to print\r\n\r\n{{{\r\nHi there.\r\nDefer: Defer.hs:7:12: error:\r\n ...\r\n}}}\r\n\r\nNow it prints\r\n\r\n{{{\r\nDefer: Defer.hs:7:12: error:\r\n ...\r\n}}}\r\n\r\nNo more `Hi there.`.\r\n\r\nThinking about Core, this change should be expected. GHC puts all evidence bindings for `main` at the top, and with unlifted equality in the solver, these bindings now contain `case typeError ... of ...`, which forces the type error eagerly. Previously, there was a lazy binding for a lifted equality witness, unpacked only at the last moment by magic in the desugarer, thus the lazier warning.\r\n\r\nSimon has proposed customizing the !FloatIn pass to deal with this scenario. I do believe this would work nicely, but I have not yet implemented it.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev